Functors between set-magmoids
Content created by Fredrik Bakke.
Created on 2023-11-01.
Last modified on 2023-11-01.
module category-theory.functors-set-magmoids where
Imports
open import category-theory.maps-set-magmoids open import category-theory.set-magmoids open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.equivalences open import foundation.function-types open import foundation.homotopies open import foundation.identity-types open import foundation.iterated-dependent-product-types open import foundation.propositions open import foundation.subtypes open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels
Idea
A functor between set-magmoids is a family of maps on the hom-sets that preserve the composition operation.
These objects serve as our starting point in the study of stucture-preserving maps of categories. Indeed, categories form a subtype of set-magmoids, although functors of set-magmoids do not automatically preserve identity-morphisms.
Definitions
The predicate of being a functor of set-magmoids
module _ {l1 l2 l3 l4 : Level} (A : Set-Magmoid l1 l2) (B : Set-Magmoid l3 l4) (F₀ : obj-Set-Magmoid A → obj-Set-Magmoid B) (F₁ : {x y : obj-Set-Magmoid A} → hom-Set-Magmoid A x y → hom-Set-Magmoid B (F₀ x) (F₀ y)) where preserves-comp-hom-Set-Magmoid : UU (l1 ⊔ l2 ⊔ l4) preserves-comp-hom-Set-Magmoid = {x y z : obj-Set-Magmoid A} (g : hom-Set-Magmoid A y z) (f : hom-Set-Magmoid A x y) → F₁ (comp-hom-Set-Magmoid A g f) ＝ comp-hom-Set-Magmoid B (F₁ g) (F₁ f) is-prop-preserves-comp-hom-Set-Magmoid : is-prop preserves-comp-hom-Set-Magmoid is-prop-preserves-comp-hom-Set-Magmoid = is-prop-iterated-implicit-Π 3 ( λ x y z → is-prop-iterated-Π 2 ( λ g f → is-set-hom-Set-Magmoid B (F₀ x) (F₀ z) ( F₁ (comp-hom-Set-Magmoid A g f)) ( comp-hom-Set-Magmoid B (F₁ g) (F₁ f)))) preserves-comp-hom-prop-Set-Magmoid : Prop (l1 ⊔ l2 ⊔ l4) pr1 preserves-comp-hom-prop-Set-Magmoid = preserves-comp-hom-Set-Magmoid pr2 preserves-comp-hom-prop-Set-Magmoid = is-prop-preserves-comp-hom-Set-Magmoid
The predicate on maps of set-magmoids of being a functor
module _ {l1 l2 l3 l4 : Level} (A : Set-Magmoid l1 l2) (B : Set-Magmoid l3 l4) (F : map-Set-Magmoid A B) where preserves-comp-hom-prop-map-Set-Magmoid : Prop (l1 ⊔ l2 ⊔ l4) preserves-comp-hom-prop-map-Set-Magmoid = preserves-comp-hom-prop-Set-Magmoid A B ( obj-map-Set-Magmoid A B F) ( hom-map-Set-Magmoid A B F) preserves-comp-hom-map-Set-Magmoid : UU (l1 ⊔ l2 ⊔ l4) preserves-comp-hom-map-Set-Magmoid = type-Prop preserves-comp-hom-prop-map-Set-Magmoid is-prop-preserves-comp-hom-map-Set-Magmoid : is-prop preserves-comp-hom-map-Set-Magmoid is-prop-preserves-comp-hom-map-Set-Magmoid = is-prop-type-Prop preserves-comp-hom-prop-map-Set-Magmoid
The type of functors between set-magmoids
module _ {l1 l2 l3 l4 : Level} (A : Set-Magmoid l1 l2) (B : Set-Magmoid l3 l4) where functor-Set-Magmoid : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) functor-Set-Magmoid = Σ ( obj-Set-Magmoid A → obj-Set-Magmoid B) ( λ F₀ → Σ ( {x y : obj-Set-Magmoid A} → hom-Set-Magmoid A x y → hom-Set-Magmoid B (F₀ x) (F₀ y)) ( preserves-comp-hom-Set-Magmoid A B F₀)) module _ {l1 l2 l3 l4 : Level} (A : Set-Magmoid l1 l2) (B : Set-Magmoid l3 l4) (F : functor-Set-Magmoid A B) where obj-functor-Set-Magmoid : obj-Set-Magmoid A → obj-Set-Magmoid B obj-functor-Set-Magmoid = pr1 F hom-functor-Set-Magmoid : {x y : obj-Set-Magmoid A} → (f : hom-Set-Magmoid A x y) → hom-Set-Magmoid B ( obj-functor-Set-Magmoid x) ( obj-functor-Set-Magmoid y) hom-functor-Set-Magmoid = pr1 (pr2 F) map-functor-Set-Magmoid : map-Set-Magmoid A B pr1 map-functor-Set-Magmoid = obj-functor-Set-Magmoid pr2 map-functor-Set-Magmoid = hom-functor-Set-Magmoid preserves-comp-functor-Set-Magmoid : {x y z : obj-Set-Magmoid A} (g : hom-Set-Magmoid A y z) (f : hom-Set-Magmoid A x y) → ( hom-functor-Set-Magmoid ( comp-hom-Set-Magmoid A g f)) ＝ ( comp-hom-Set-Magmoid B ( hom-functor-Set-Magmoid g) ( hom-functor-Set-Magmoid f)) preserves-comp-functor-Set-Magmoid = pr2 (pr2 F)
The identity functor on a set-magmoid
module _ {l1 l2 : Level} (A : Set-Magmoid l1 l2) where id-functor-Set-Magmoid : functor-Set-Magmoid A A pr1 id-functor-Set-Magmoid = id pr1 (pr2 id-functor-Set-Magmoid) = id pr2 (pr2 id-functor-Set-Magmoid) g f = refl
Composition of functors on set-magmoids
Any two compatible functors can be composed to a new functor.
module _ {l1 l2 l3 l4 l5 l6 : Level} (A : Set-Magmoid l1 l2) (B : Set-Magmoid l3 l4) (C : Set-Magmoid l5 l6) (G : functor-Set-Magmoid B C) (F : functor-Set-Magmoid A B) where obj-comp-functor-Set-Magmoid : obj-Set-Magmoid A → obj-Set-Magmoid C obj-comp-functor-Set-Magmoid = obj-functor-Set-Magmoid B C G ∘ obj-functor-Set-Magmoid A B F hom-comp-functor-Set-Magmoid : {x y : obj-Set-Magmoid A} → hom-Set-Magmoid A x y → hom-Set-Magmoid C ( obj-comp-functor-Set-Magmoid x) ( obj-comp-functor-Set-Magmoid y) hom-comp-functor-Set-Magmoid = hom-functor-Set-Magmoid B C G ∘ hom-functor-Set-Magmoid A B F map-comp-functor-Set-Magmoid : map-Set-Magmoid A C pr1 map-comp-functor-Set-Magmoid = obj-comp-functor-Set-Magmoid pr2 map-comp-functor-Set-Magmoid = hom-comp-functor-Set-Magmoid preserves-comp-comp-functor-Set-Magmoid : preserves-comp-hom-Set-Magmoid A C obj-comp-functor-Set-Magmoid hom-comp-functor-Set-Magmoid preserves-comp-comp-functor-Set-Magmoid g f = ( ap ( hom-functor-Set-Magmoid B C G) ( preserves-comp-functor-Set-Magmoid A B F g f)) ∙ ( preserves-comp-functor-Set-Magmoid B C G ( hom-functor-Set-Magmoid A B F g) ( hom-functor-Set-Magmoid A B F f)) comp-functor-Set-Magmoid : functor-Set-Magmoid A C pr1 comp-functor-Set-Magmoid = obj-comp-functor-Set-Magmoid pr1 (pr2 comp-functor-Set-Magmoid) = hom-functor-Set-Magmoid B C G ∘ hom-functor-Set-Magmoid A B F pr2 (pr2 comp-functor-Set-Magmoid) = preserves-comp-comp-functor-Set-Magmoid
Properties
Extensionality of functors between set-magmoids
Equality of functors is equality of underlying maps
module _ {l1 l2 l3 l4 : Level} (A : Set-Magmoid l1 l2) (B : Set-Magmoid l3 l4) (F G : functor-Set-Magmoid A B) where equiv-eq-map-eq-functor-Set-Magmoid : (F ＝ G) ≃ (map-functor-Set-Magmoid A B F ＝ map-functor-Set-Magmoid A B G) equiv-eq-map-eq-functor-Set-Magmoid = equiv-ap-emb ( comp-emb ( emb-subtype ( preserves-comp-hom-prop-map-Set-Magmoid A B)) ( emb-equiv ( inv-associative-Σ ( obj-Set-Magmoid A → obj-Set-Magmoid B) ( λ F₀ → { x y : obj-Set-Magmoid A} → hom-Set-Magmoid A x y → hom-Set-Magmoid B (F₀ x) (F₀ y)) ( preserves-comp-hom-map-Set-Magmoid A B)))) eq-map-eq-functor-Set-Magmoid : F ＝ G → map-functor-Set-Magmoid A B F ＝ map-functor-Set-Magmoid A B G eq-map-eq-functor-Set-Magmoid = map-equiv equiv-eq-map-eq-functor-Set-Magmoid eq-eq-map-functor-Set-Magmoid : map-functor-Set-Magmoid A B F ＝ map-functor-Set-Magmoid A B G → F ＝ G eq-eq-map-functor-Set-Magmoid = map-inv-equiv equiv-eq-map-eq-functor-Set-Magmoid is-section-eq-eq-map-functor-Set-Magmoid : eq-map-eq-functor-Set-Magmoid ∘ eq-eq-map-functor-Set-Magmoid ~ id is-section-eq-eq-map-functor-Set-Magmoid = is-section-map-inv-equiv equiv-eq-map-eq-functor-Set-Magmoid is-retraction-eq-eq-map-functor-Set-Magmoid : eq-eq-map-functor-Set-Magmoid ∘ eq-map-eq-functor-Set-Magmoid ~ id is-retraction-eq-eq-map-functor-Set-Magmoid = is-retraction-map-inv-equiv equiv-eq-map-eq-functor-Set-Magmoid
Categorical laws for functor composition
Unit laws for functor composition
module _ {l1 l2 l3 l4 : Level} (A : Set-Magmoid l1 l2) (B : Set-Magmoid l3 l4) (F : functor-Set-Magmoid A B) where left-unit-law-comp-functor-Set-Magmoid : comp-functor-Set-Magmoid A B B (id-functor-Set-Magmoid B) F ＝ F left-unit-law-comp-functor-Set-Magmoid = eq-eq-map-functor-Set-Magmoid A B _ _ refl right-unit-law-comp-functor-Set-Magmoid : comp-functor-Set-Magmoid A A B F (id-functor-Set-Magmoid A) ＝ F right-unit-law-comp-functor-Set-Magmoid = refl
Associativity of functor composition
module _ {l1 l1' l2 l2' l3 l3' l4 l4' : Level} (A : Set-Magmoid l1 l1') (B : Set-Magmoid l2 l2') (C : Set-Magmoid l3 l3') (D : Set-Magmoid l4 l4') (F : functor-Set-Magmoid A B) (G : functor-Set-Magmoid B C) (H : functor-Set-Magmoid C D) where associative-comp-functor-Set-Magmoid : comp-functor-Set-Magmoid A B D (comp-functor-Set-Magmoid B C D H G) F ＝ comp-functor-Set-Magmoid A C D H (comp-functor-Set-Magmoid A B C G F) associative-comp-functor-Set-Magmoid = eq-eq-map-functor-Set-Magmoid A D _ _ refl
Mac Lane pentagon for functor composition
(I(GH))F ---- I((GH)F)
/ \
/ \
((IH)G)F I(H(GF))
\ /
\ /
(IH)(GF)
The proof remains to be formalized.
module _
{l1 l1' l2 l2' l3 l3' l4 l4' : Level}
(A : Set-Magmoid l1 l1')
(B : Set-Magmoid l2 l2')
(C : Set-Magmoid l3 l3')
(D : Set-Magmoid l4 l4')
(E : Set-Magmoid l4 l4')
(F : functor-Set-Magmoid A B)
(G : functor-Set-Magmoid B C)
(H : functor-Set-Magmoid C D)
(I : functor-Set-Magmoid D E)
where
mac-lane-pentagon-comp-functor-Set-Magmoid :
coherence-pentagon-identifications
{ x =
comp-functor-Set-Magmoid A B E
( comp-functor-Set-Magmoid B D E I
( comp-functor-Set-Magmoid B C D H G))
( F)}
{ comp-functor-Set-Magmoid A D E I
( comp-functor-Set-Magmoid A B D
( comp-functor-Set-Magmoid B C D H G)
( F))}
{ comp-functor-Set-Magmoid A B E
( comp-functor-Set-Magmoid B C E
( comp-functor-Set-Magmoid C D E I H)
( G))
( F)}
{ comp-functor-Set-Magmoid A D E
( I)
( comp-functor-Set-Magmoid A C D
( H)
( comp-functor-Set-Magmoid A B C G F))}
{ comp-functor-Set-Magmoid A C E
( comp-functor-Set-Magmoid C D E I H)
( comp-functor-Set-Magmoid A B C G F)}
( associative-comp-functor-Set-Magmoid A B D E
( F) (comp-functor-Set-Magmoid B C D H G) (I))
( ap
( λ p → comp-functor-Set-Magmoid A B E p F)
( inv (associative-comp-functor-Set-Magmoid B C D E G H I)))
( ap
( λ p → comp-functor-Set-Magmoid A D E I p)
( associative-comp-functor-Set-Magmoid A B C D F G H))
( associative-comp-functor-Set-Magmoid A B C E
( F) (G) (comp-functor-Set-Magmoid C D E I H))
( inv
( associative-comp-functor-Set-Magmoid A C D E
(comp-functor-Set-Magmoid A B C G F) H I))
mac-lane-pentagon-comp-functor-Set-Magmoid = {!!}
Recent changes
- 2023-11-01. Fredrik Bakke. Fun with functors (#886).