# Equivalences of arrows

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2024-01-25.

module foundation.equivalences-arrows where

Imports
open import foundation.cartesian-morphisms-arrows
open import foundation.commuting-squares-of-maps
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.homotopies
open import foundation.morphisms-arrows
open import foundation.span-diagrams
open import foundation.spans
open import foundation.universe-levels

open import foundation-core.propositions


## Idea

An equivalence of arrows from a function f : A → B to a function g : X → Y is a morphism of arrows

        i
A -----> X
|   ≃    |
f |        | g
∨   ≃    ∨
B -----> Y
j


in which i and j are equivalences.

## Definitions

### The predicate of being an equivalence of arrows

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(f : A → B) (g : X → Y) (h : hom-arrow f g)
where

is-equiv-prop-hom-arrow : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
is-equiv-prop-hom-arrow =
product-Prop
( is-equiv-Prop (map-domain-hom-arrow f g h))
( is-equiv-Prop (map-codomain-hom-arrow f g h))

is-equiv-hom-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
is-equiv-hom-arrow =
type-Prop is-equiv-prop-hom-arrow

is-prop-is-equiv-hom-arrow : is-prop is-equiv-hom-arrow
is-prop-is-equiv-hom-arrow = is-prop-type-Prop is-equiv-prop-hom-arrow

is-equiv-map-domain-is-equiv-hom-arrow :
is-equiv-hom-arrow → is-equiv (map-domain-hom-arrow f g h)
is-equiv-map-domain-is-equiv-hom-arrow = pr1

is-equiv-map-codomain-is-equiv-hom-arrow :
is-equiv-hom-arrow → is-equiv (map-codomain-hom-arrow f g h)
is-equiv-map-codomain-is-equiv-hom-arrow = pr2


### Equivalences of arrows

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(f : A → B) (g : X → Y)
where

coherence-equiv-arrow : (A ≃ X) → (B ≃ Y) → UU (l1 ⊔ l4)
coherence-equiv-arrow i j =
coherence-hom-arrow f g (map-equiv i) (map-equiv j)

equiv-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
equiv-arrow =
Σ (A ≃ X) (λ i → Σ (B ≃ Y) (coherence-equiv-arrow i))

module _
(e : equiv-arrow)
where

equiv-domain-equiv-arrow : A ≃ X
equiv-domain-equiv-arrow = pr1 e

map-domain-equiv-arrow : A → X
map-domain-equiv-arrow = map-equiv equiv-domain-equiv-arrow

is-equiv-map-domain-equiv-arrow : is-equiv map-domain-equiv-arrow
is-equiv-map-domain-equiv-arrow =
is-equiv-map-equiv equiv-domain-equiv-arrow

equiv-codomain-equiv-arrow : B ≃ Y
equiv-codomain-equiv-arrow = pr1 (pr2 e)

map-codomain-equiv-arrow : B → Y
map-codomain-equiv-arrow = map-equiv equiv-codomain-equiv-arrow

is-equiv-map-codomain-equiv-arrow : is-equiv map-codomain-equiv-arrow
is-equiv-map-codomain-equiv-arrow =
is-equiv-map-equiv equiv-codomain-equiv-arrow

coh-equiv-arrow :
coherence-equiv-arrow
( equiv-domain-equiv-arrow)
( equiv-codomain-equiv-arrow)
coh-equiv-arrow = pr2 (pr2 e)

hom-equiv-arrow : hom-arrow f g
pr1 hom-equiv-arrow = map-domain-equiv-arrow
pr1 (pr2 hom-equiv-arrow) = map-codomain-equiv-arrow
pr2 (pr2 hom-equiv-arrow) = coh-equiv-arrow

is-equiv-equiv-arrow : is-equiv-hom-arrow f g hom-equiv-arrow
pr1 is-equiv-equiv-arrow = is-equiv-map-domain-equiv-arrow
pr2 is-equiv-equiv-arrow = is-equiv-map-codomain-equiv-arrow

span-equiv-arrow :
span l1 B X
span-equiv-arrow =
span-hom-arrow f g hom-equiv-arrow

span-diagram-equiv-arrow : span-diagram l2 l3 l1
pr1 span-diagram-equiv-arrow = B
pr1 (pr2 span-diagram-equiv-arrow) = X
pr2 (pr2 span-diagram-equiv-arrow) = span-equiv-arrow


### The identity equivalence of arrows

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
where

id-equiv-arrow : equiv-arrow f f
pr1 id-equiv-arrow = id-equiv
pr1 (pr2 id-equiv-arrow) = id-equiv
pr2 (pr2 id-equiv-arrow) = refl-htpy


### Composition of equivalences of arrows

module _
{l1 l2 l3 l4 l5 l6 : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6}
(f : A → B) (g : X → Y) (h : U → V)
(b : equiv-arrow g h) (a : equiv-arrow f g)
where

equiv-domain-comp-equiv-arrow : A ≃ U
equiv-domain-comp-equiv-arrow =
equiv-domain-equiv-arrow g h b ∘e equiv-domain-equiv-arrow f g a

map-domain-comp-equiv-arrow : A → U
map-domain-comp-equiv-arrow = map-equiv equiv-domain-comp-equiv-arrow

equiv-codomain-comp-equiv-arrow : B ≃ V
equiv-codomain-comp-equiv-arrow =
equiv-codomain-equiv-arrow g h b ∘e equiv-codomain-equiv-arrow f g a

map-codomain-comp-equiv-arrow : B → V
map-codomain-comp-equiv-arrow = map-equiv equiv-codomain-comp-equiv-arrow

coh-comp-equiv-arrow :
coherence-equiv-arrow f h
( equiv-domain-comp-equiv-arrow)
( equiv-codomain-comp-equiv-arrow)
coh-comp-equiv-arrow =
coh-comp-hom-arrow f g h
( hom-equiv-arrow g h b)
( hom-equiv-arrow f g a)

comp-equiv-arrow : equiv-arrow f h
pr1 comp-equiv-arrow = equiv-domain-comp-equiv-arrow
pr1 (pr2 comp-equiv-arrow) = equiv-codomain-comp-equiv-arrow
pr2 (pr2 comp-equiv-arrow) = coh-comp-equiv-arrow

hom-comp-equiv-arrow : hom-arrow f h
hom-comp-equiv-arrow = hom-equiv-arrow f h comp-equiv-arrow


### Inverses of equivalences of arrows

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(f : A → B) (g : X → Y) (α : equiv-arrow f g)
where

equiv-domain-inv-equiv-arrow : X ≃ A
equiv-domain-inv-equiv-arrow = inv-equiv (equiv-domain-equiv-arrow f g α)

map-domain-inv-equiv-arrow : X → A
map-domain-inv-equiv-arrow = map-equiv equiv-domain-inv-equiv-arrow

equiv-codomain-inv-equiv-arrow : Y ≃ B
equiv-codomain-inv-equiv-arrow = inv-equiv (equiv-codomain-equiv-arrow f g α)

map-codomain-inv-equiv-arrow : Y → B
map-codomain-inv-equiv-arrow = map-equiv equiv-codomain-inv-equiv-arrow

coh-inv-equiv-arrow :
coherence-equiv-arrow g f
( equiv-domain-inv-equiv-arrow)
( equiv-codomain-inv-equiv-arrow)
coh-inv-equiv-arrow =
horizontal-inv-equiv-coherence-square-maps
( equiv-domain-equiv-arrow f g α)
( f)
( g)
( equiv-codomain-equiv-arrow f g α)
( coh-equiv-arrow f g α)

inv-equiv-arrow : equiv-arrow g f
pr1 inv-equiv-arrow = equiv-domain-inv-equiv-arrow
pr1 (pr2 inv-equiv-arrow) = equiv-codomain-inv-equiv-arrow
pr2 (pr2 inv-equiv-arrow) = coh-inv-equiv-arrow

hom-inv-equiv-arrow : hom-arrow g f
hom-inv-equiv-arrow = hom-equiv-arrow g f inv-equiv-arrow

is-equiv-inv-equiv-arrow : is-equiv-hom-arrow g f hom-inv-equiv-arrow
is-equiv-inv-equiv-arrow = is-equiv-equiv-arrow g f inv-equiv-arrow


### If a map is equivalent to an equivalence, then it is an equivalence

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(f : A → B) (g : X → Y) (α : equiv-arrow f g)
where

is-equiv-source-is-equiv-target-equiv-arrow : is-equiv g → is-equiv f
is-equiv-source-is-equiv-target-equiv-arrow =
is-equiv-left-is-equiv-right-square
( f)
( g)
( map-domain-equiv-arrow f g α)
( map-codomain-equiv-arrow f g α)
( coh-equiv-arrow f g α)
( is-equiv-map-domain-equiv-arrow f g α)
( is-equiv-map-codomain-equiv-arrow f g α)

is-equiv-target-is-equiv-source-equiv-arrow : is-equiv f → is-equiv g
is-equiv-target-is-equiv-source-equiv-arrow =
is-equiv-right-is-equiv-left-square
( f)
( g)
( map-domain-equiv-arrow f g α)
( map-codomain-equiv-arrow f g α)
( coh-equiv-arrow f g α)
( is-equiv-map-domain-equiv-arrow f g α)
( is-equiv-map-codomain-equiv-arrow f g α)


### Equivalences of arrows are cartesian

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(f : A → B) (g : X → Y) (α : equiv-arrow f g)
where

is-cartesian-equiv-arrow :
is-cartesian-hom-arrow f g (hom-equiv-arrow f g α)
is-cartesian-equiv-arrow =
is-pullback-is-equiv-horizontal-maps
( map-codomain-equiv-arrow f g α)
( g)
( cone-hom-arrow f g (hom-equiv-arrow f g α))
( is-equiv-map-codomain-equiv-arrow f g α)
( is-equiv-map-domain-equiv-arrow f g α)

cartesian-hom-equiv-arrow : cartesian-hom-arrow f g
pr1 cartesian-hom-equiv-arrow = hom-equiv-arrow f g α
pr2 cartesian-hom-equiv-arrow = is-cartesian-equiv-arrow