Showing changes from revision #6 to #7:
Added | Removed | Changed
The concept if functor is the evident concept of homomorphisms between categories.
Let and be precategories . A Informally, afunctor consists of
In terms of formal Coq-code this reads as follows (e.g. Ahrens-Kapulkin-Shulman 13, functors_transformations.v):
Definition functor_data (C C' : precategory_ob_mor) := total2 (
fun F : ob C -> ob C' =>
forall a b : ob C, a --> b -> F a --> F b).
Definition functor_on_objects {C C' : precategory_ob_mor}
(F : functor_data C C') : ob C -> ob C' := pr1 F.
Coercion functor_on_objects : functor_data >-> Funclass.
Definition functor_on_morphisms {C C' : precategory_ob_mor} (F : functor_data C C')
{ a b : ob C} : a --> b -> F a --> F b := pr2 F a b.
Local Notation "# F" := (functor_on_morphisms F)(at level 3).
Definition is_functor {C C' : precategory_data} (F : functor_data C C') :=
dirprod (forall a : ob C, #F (identity a) == identity (F a))
(forall a b c : ob C, forall f : a --> b, forall g : b --> c,
#F (f ;; g) == #F f ;; #F g).
Lemma isaprop_is_functor (C C' : precategory_data)
(F : functor_data C C'): isaprop (is_functor F).
Proof.
apply isofhleveldirprod.
apply impred; intro a.
apply (pr2 (_ --> _)).
repeat (apply impred; intro).
apply (pr2 (_ --> _)).
Qed.
Definition functor (C C' : precategory) := total2 (
fun F : functor_data C C' => is_functor F).
By induction on identity, a functor also preserves (See precategory).
For functors and , their composite is given by
Composition of functors is associative .
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.
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 12:37:58 by Urs Schreiber. See the history of this page for a list of all contributions to it.