# Maps between set-magmoids

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-11-01.

module category-theory.maps-set-magmoids where

Imports
open import category-theory.set-magmoids

open import foundation.action-on-identifications-functions
open import foundation.commuting-pentagons-of-identifications
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.universe-levels


## Idea

A map from a set-magmoid C to a set magmoid D consists of:

• a map F₀ : C → D on objects, and
• a map F₁ : hom x y → hom (F₀ x) (F₀ y) on morphisms.

## Definitions

### Maps between set-magmoids

module _
{l1 l2 l3 l4 : Level}
(C : Set-Magmoid l1 l2)
(D : Set-Magmoid l3 l4)
where

map-Set-Magmoid : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
map-Set-Magmoid =
Σ ( obj-Set-Magmoid C → obj-Set-Magmoid D)
( λ F₀ →
{x y : obj-Set-Magmoid C} →
hom-Set-Magmoid C x y →
hom-Set-Magmoid D (F₀ x) (F₀ y))

obj-map-Set-Magmoid :
(F : map-Set-Magmoid) → obj-Set-Magmoid C → obj-Set-Magmoid D
obj-map-Set-Magmoid = pr1

hom-map-Set-Magmoid :
(F : map-Set-Magmoid) {x y : obj-Set-Magmoid C} →
hom-Set-Magmoid C x y →
hom-Set-Magmoid D (obj-map-Set-Magmoid F x) (obj-map-Set-Magmoid F y)
hom-map-Set-Magmoid = pr2


### The identity map on a set-magmoid

module _
{l1 l2 : Level} (A : Set-Magmoid l1 l2)
where

id-map-Set-Magmoid : map-Set-Magmoid A A
pr1 id-map-Set-Magmoid = id
pr2 id-map-Set-Magmoid = id


### Composition of maps on set-magmoids

Any two compatible maps can be composed to a new map.

module _
{l1 l2 l3 l4 l5 l6 : Level}
(A : Set-Magmoid l1 l2)
(B : Set-Magmoid l3 l4)
(C : Set-Magmoid l5 l6)
(G : map-Set-Magmoid B C)
(F : map-Set-Magmoid A B)
where

obj-comp-map-Set-Magmoid : obj-Set-Magmoid A → obj-Set-Magmoid C
obj-comp-map-Set-Magmoid =
obj-map-Set-Magmoid B C G ∘ obj-map-Set-Magmoid A B F

hom-comp-map-Set-Magmoid :
{x y : obj-Set-Magmoid A} →
hom-Set-Magmoid A x y →
hom-Set-Magmoid C (obj-comp-map-Set-Magmoid x) (obj-comp-map-Set-Magmoid y)
hom-comp-map-Set-Magmoid =
hom-map-Set-Magmoid B C G ∘ hom-map-Set-Magmoid A B F

comp-map-Set-Magmoid : map-Set-Magmoid A C
pr1 comp-map-Set-Magmoid = obj-comp-map-Set-Magmoid
pr2 comp-map-Set-Magmoid = hom-comp-map-Set-Magmoid


## Properties

### Categorical laws for map composition

#### Unit laws for map composition

module _
{l1 l2 l3 l4 : Level}
(A : Set-Magmoid l1 l2) (B : Set-Magmoid l3 l4)
(F : map-Set-Magmoid A B)
where

left-unit-law-comp-map-Set-Magmoid :
comp-map-Set-Magmoid A B B (id-map-Set-Magmoid B) F ＝ F
left-unit-law-comp-map-Set-Magmoid = refl

right-unit-law-comp-map-Set-Magmoid :
comp-map-Set-Magmoid A A B F (id-map-Set-Magmoid A) ＝ F
right-unit-law-comp-map-Set-Magmoid = refl


#### Associativity of map 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 : map-Set-Magmoid A B)
(G : map-Set-Magmoid B C)
(H : map-Set-Magmoid C D)
where

associative-comp-map-Set-Magmoid :
comp-map-Set-Magmoid A B D (comp-map-Set-Magmoid B C D H G) F ＝
comp-map-Set-Magmoid A C D H (comp-map-Set-Magmoid A B C G F)
associative-comp-map-Set-Magmoid = refl


#### Mac Lane pentagon for map composition

The Mac Lane pentagon is a higher coherence of the associator for map composition. Since map composition is strictly associative, the Mac Lane pentagon also follows by reflexivity.

    (I(GH))F ---- I((GH)F)
/        \
/          \
((IH)G)F          I(H(GF))
\        /
\    /
(IH)(GF)

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 : map-Set-Magmoid A B)
(G : map-Set-Magmoid B C)
(H : map-Set-Magmoid C D)
(I : map-Set-Magmoid D E)
where

mac-lane-pentagon-comp-map-Set-Magmoid :
coherence-pentagon-identifications
{ x =
comp-map-Set-Magmoid A B E
( comp-map-Set-Magmoid B D E I
( comp-map-Set-Magmoid B C D H G))
( F)}
{ comp-map-Set-Magmoid A D E I
( comp-map-Set-Magmoid A B D
( comp-map-Set-Magmoid B C D H G)
( F))}
{ comp-map-Set-Magmoid A B E
( comp-map-Set-Magmoid B C E
( comp-map-Set-Magmoid C D E I H)
( G))
( F)}
{ comp-map-Set-Magmoid A D E
( I)
( comp-map-Set-Magmoid A C D
( H)
( comp-map-Set-Magmoid A B C G F))}
{ comp-map-Set-Magmoid A C E
( comp-map-Set-Magmoid C D E I H)
( comp-map-Set-Magmoid A B C G F)}
( associative-comp-map-Set-Magmoid A B D E
( F) (comp-map-Set-Magmoid B C D H G) (I))
( ap
( λ p → comp-map-Set-Magmoid A B E p F)
( inv (associative-comp-map-Set-Magmoid B C D E G H I)))
( ap
( λ p → comp-map-Set-Magmoid A D E I p)
( associative-comp-map-Set-Magmoid A B C D F G H))
( associative-comp-map-Set-Magmoid A B C E
( F) (G) (comp-map-Set-Magmoid C D E I H))
( inv
( associative-comp-map-Set-Magmoid A C D E
(comp-map-Set-Magmoid A B C G F) H I))
mac-lane-pentagon-comp-map-Set-Magmoid = refl