Homotopy Type Theory
Category theory

Here we collect articles about doing category theory in HoTT. This is based off of the HoTT Book.

Definitions

Groupoids

• pregroupoid?
• setoid
• groupoid
• set

Homotopy precategories

• quiver
• directed graph
• H-magmoid
• H-spaceoid
• homotopy precategory
• concrete homotopy precategory
• family of objects in a concrete homotopy precategory
• SEPS

Morphisms

• isomorphism in a precategory
• epimorphism in a precategory?
• monomorphism in a precategory?

Categories

• precategory
• category
• equivalence of precategories
• weak equivalence of precategories
• isomorphism of precategories?
• opposite precategory
• product precategory

Functors

• functor
• natural transformation
• functor precategory
• left adjoint
• faithful functor
• full functor
• split essentially surjective
• essentially surjective
• hom functor
• representable functor

Limits and colimits

• product?
• coproduct?
• equaliser?
• directed colimit?

Dagger morphisms

• unitary isomorphism in a dagger precategory
• dagger epimorphism in a dagger precategory
• dagger monomorphism in a dagger precategory

Dagger categories

• dagger precategory
• dagger category
• monoidal dagger category
• braided monoidal dagger category
• symmetric monoidal dagger category
• cartesian monoidal dagger category
• cocartesian monoidal dagger category
• semiadditive dagger category
• finitely complete dagger category?
• finitely cocomplete dagger category?
• compact closed dagger category

Order theory

• preorder
• directed type
• net
• poset
• join-semilattice
• meet-semilattice
• omega-complete poset
• directed-complete poset
• partial function classifier
• Sierpinski space
• continuous poset?
• lattice
• distributive lattice
• sigma-complete lattice
• sigma-frame
• suplattice
• frame
• Heyting algebra
• Boolean algebra?
• monotonic function
• monotonic function preorder?
• sigma-continuous function?
• opposite preorder
• antitonic function
• posite?
• lower type
• upper type
• ideal?
• filter
• enriched poset
• order
• strict order
• dense strict order
• quasiorder?
• strict lower type?
• strict upper type?
• Dedekind cut
• Dedekind complete dense strict order?

2-posets

• 2-preorder
• 2-poset
• locally Heyting-algebraic 2-poset

dagger 2-posets

• dagger 2-preorder
• dagger 2-poset
• semiadditive dagger 2-poset
• unital dagger 2-poset
• tabular dagger 2-poset
• division dagger 2-poset
• power dagger 2-poset
• cartesian dagger 2-poset
• conjunctive dagger 2-poset
• coherent dagger 2-poset
• geometric dagger 2-poset
• Heyting dagger 2-poset
• Boolean dagger 2-poset
• elementarily topical dagger 2-poset
• Boolean topical dagger 2-poset
• W-topical dagger 2-poset
• well-pointed dagger 2-poset
• choice dagger 2-poset
• 2-poset of partial maps
• category of maps
• category of monic maps
• ETCR
• Categorical SEAR

Dagger morphisms in dagger 2-posets

• onto dagger morphism in a dagger 2-poset
• functional dagger morphism in a dagger 2-poset
• entire dagger morphism in a dagger 2-poset
• one-to-one dagger morphism in a dagger 2-poset
• map in a dagger 2-poset
• monic map in a dagger 2-poset
• epic map in a dagger 2-poset?

Concrete categories

• concrete precategory
• concrete category
• family of objects in a concrete precategory
• category of partial functions in a set
• ETCS with elements
• HilbR
• Rel
• SEAR

Theorems

• Rezk completion
• Yoneda lemma

References

• HoTT Book
• Univalent categories and the Rezk completion