This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.
Equivalences of arrows
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