The category of Heyting algebras.
Equations
Instances For
Construct a bundled HeytAlg
from a HeytingAlgebra
.
Instances For
Equations
- HeytAlg.instInhabited = { default := HeytAlg.of PUnit.{?u.3 + 1} }
Equations
- One or more equations did not get rendered due to their size.
Equations
instance
HeytAlg.instHeytingHomClassHomαHeytingAlgebra
{X Y : HeytAlg}
:
HeytingHomClass (X ⟶ Y) ↑X ↑Y
Equations
- One or more equations did not get rendered due to their size.
@[simp]
@[simp]