Homotopy Type Theory locally Heyting-algebraic 2-poset > history (Rev #2, changes)

Contents

Definition

A 2-poset $C$ is locally Heyting-algebraic if for every object $A:Ob(C)$ and $B:Ob(C)$, the hom-object $Hom(A,B)$ is a Heyting algebra.

Examples

The 2-poset of sets and relations is locally Heyting-algebraic.

See also

• 2-poset

• Heyting algebra