In basics: cubical methods (heterogeneous equality, globe_over, path_over, square), polynomials (polynomial), general facts (general).
In bicategories.bicategory: definition (bicategory, strict), equivalences in bicategories (equivalence), examples (the bicategory of 1-types, every 2-type is a bicategory, the bicategory of categories, full sub bicategory, opposite bicategory)
In bicategories.lax_functor: definition (lax_functor), examples (a map between 2-types gives a lax functor)
In bicategoriese.lax_transformation: definition (lax_transformation)
In setoid: basic definitions (setoid), properties of the quotient (squot_properties), squot is an adjuction (setoid_adjunction)
In groupoid.grpd_bicategory: definition of groupoids, proof that it is a bicategory, several constructions, laws of groupoids
In groupoid.path_groupoid: every 1-type gives a groupoid via the path space, every type gives a groupoid by truncating the path space.
In groupoid.groupoid_quotient: definition of groupoid quotient (gquot), recursion principles (gquot_principles), functoriality (gquot_functor), in properties the encode-decode proof, it commutes with + and * and general properties are given
Known to compile with the HoTT library version d79a5b50196a0c101eb192830620cabe2eaa1781.
Compilation:
coq_makefile -f _CoqProject -o Makefilemake