Homotopy Type Theory functor > history (Rev #8, changes)

Showing changes from revision #7 to #8: Added | ~~Removed~~ | ~~Chan~~ged

Idea
Definition
Properties
See also
References

Idea

The ~~concept~~ definition if offunctor in homotopy type theory is a straightforward translation of the ~~evident~~ ordinary ~~concept~~ one. However, the notion of~~homomorphisms~~univalent category? ~~between~~ allows us to construct some such functors that in classical mathematics would require either the ~~categories~~ axiom of choice or the use of anafunctors.

Definition

Let $A$ and $B$ be precategories. Informally, a functor $F : A \to B$ consists of

A function $F_0 : A_0 \to B_0$
For each $a,b:A$ , a function $F_{a,b}:hom_A(a,b) \to hom_B(F a,F b)$ , generally also denoted $F$ .
For each $a:A$ , we have $F(1_a)=1_{F a}$ .
For each $a,b,c: A$ and $f:hom_A(a,b)$ amd $g:hom_A(b,c)$ , we have

F(g \circ f) = F g \circ F f

In Formally, ~~terms~~ the type of ~~formal~~ functors from~~Coq~~ $A$ ~~-code~~ ~~this~~ to ~~reads~~ as ~~follows~~ ~~(e.g.Ahrens-Kapulkin-Shulman 13~~ $B$ , is~~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).

Func(A,B) \coloneqq \sum_{F_0:A_0\to B_0} \sum_{F:\prod_{a,b:A} hom_A(a,b) \to \hom_B(F a,F b)} \Big(\prod_{a:A} F(1_a) = 1_{F a}\Big) \times \Big( \prod_{a,b,c:A} \prod_{f:\hom_A(a,b)} \prod_{g:\hom_A(b,c)} F(g \circ f) = F g \circ F f\Big)

A formal definition in Coq? can be found in Ahrens-Kapulkin-Shulman 13.

Properties

By induction on identity, a functor also preserves $idtoiso$ (See precategory).

Composition of functors

For functors $F:A\to B$ and $G:B \to C$ , their composite $G \circ F : A \to C$ is given by

The composite $(G_0 \circ F_0): A_0 \to C_0$
For each $a,b:A$ , the composite
$(G_{F a, F b} \circ F_{a,b}):hom_A(a,b)\to hom_C(G F a, G F b)$

Lemma 9.2.9

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.10

Lemma 9.2.9 is coherent, i.e. the following pentagon of equalities commutes:

\array{ && (K H)(G F) \\ & \nearrow && \searrow \\ ((K H) G) F && && K (H (G F)) \\ \downarrow && && \uparrow \\ (K(H G)) F && \longrightarrow && K( (H G) F) }

References

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~~Coq? code formalizing the concept of functors includes the following:

functors_transformations.v

category: category theory

Revision on September 7, 2018 at 18:03:31 by Mike Shulman. See the history of this page for a list of all contributions to it.