The definition of functor in homotopy type theory is a straightforward translation of the ordinary one. However, the notion of univalent category? allows us to construct some such functors that in classical mathematics would require either the axiom of choice or the use of anafunctors.
Let $A$ and $B$ be precategories. Informally, a functor $F : A \to B$ consists of
Formally, the type of functors from $A$ to $B$ is
A formal definition in Coq? can be found in Ahrens-Kapulkin-Shulman 13.
By induction on identity, a functor also preserves $idtoiso$ (See precategory).
For functors $F:A\to B$ and $G:B \to C$, their composite $G \circ F : A \to C$ is given by
Composition of functors is associative $H(G F)=(H G)F$.
Proof: Since composition of functions is associative, this follows immediately for the actions on objects and on homs. And since hom-sets are sets, the rest of the data is automatic. $\square$
Lemma 9.2.9 is coherent, i.e. the following pentagon of equalities commutes:
Category theory natural transformation full functor faithful functor
Benedikt Ahrens, Chris Kapulkin, Michael Shulman, section 4 of Univalent categories and the Rezk completion, Mathematical Structures in Computer Science 25.5 (2015): 1010-1039 (arXiv:1303.0584)
Univalent Foundations Project, section 9.2 of Homotopy Type Theory – Univalent Foundations of Mathematics, IAS 2013
Coq? code formalizing the concept of functors includes the following:
Revision on September 7, 2018 at 14:03:31 by Mike Shulman. See the history of this page for a list of all contributions to it.