module Cat.Morphism {o h} (C : Precategory o h) where
Morphisms🔗
This module defines the three most important classes of morphisms that can be found in a category: monomorphisms, epimorphisms, and isomorphisms.
Monos🔗
A morphism is said to be monic when it is left-cancellable. A monomorphism from to written is a monic morphism.
is-monic : Hom a b → Type _ is-monic {a = a} f = ∀ {c} → (g h : Hom c a) → f ∘ g ≡ f ∘ h → g ≡ h is-monic-is-prop : ∀ {a b} (f : Hom a b) → is-prop (is-monic f) is-monic-is-prop f x y i {c} g h p = Hom-set _ _ _ _ (x g h p) (y g h p) i record _↪_ (a b : Ob) : Type (o ⊔ h) where constructor make-mono field mor : Hom a b monic : is-monic mor open _↪_ public
Conversely, a morphism is said to be epic when it is right-cancellable. An epimorphism from to written is an epic morphism.
Epis🔗
is-epic : Hom a b → Type _ is-epic {b = b} f = ∀ {c} → (g h : Hom b c) → g ∘ f ≡ h ∘ f → g ≡ h is-epic-is-prop : ∀ {a b} (f : Hom a b) → is-prop (is-epic f) is-epic-is-prop f x y i {c} g h p = Hom-set _ _ _ _ (x g h p) (y g h p) i record _↠_ (a b : Ob) : Type (o ⊔ h) where constructor make-epi field mor : Hom a b epic : is-epic mor open _↠_ public
The identity morphism is monic and epic.
id-monic : ∀ {a} → is-monic (id {a}) id-monic g h p = sym (idl _) ∙∙ p ∙∙ idl _ id-epic : ∀ {a} → is-epic (id {a}) id-epic g h p = sym (idr _) ∙∙ p ∙∙ idr _
Both monos and epis are closed under composition.
∘-is-monic : ∀ {a b c} {f : Hom b c} {g : Hom a b} → is-monic f → is-monic g → is-monic (f ∘ g) ∘-is-monic fm gm a b α = gm _ _ (fm _ _ (assoc _ _ _ ∙∙ α ∙∙ sym (assoc _ _ _))) ∘-is-epic : ∀ {a b c} {f : Hom b c} {g : Hom a b} → is-epic f → is-epic g → is-epic (f ∘ g) ∘-is-epic fe ge a b α = fe _ _ (ge _ _ (sym (assoc _ _ _) ∙∙ α ∙∙ (assoc _ _ _))) _∘Mono_ : ∀ {a b c} → b ↪ c → a ↪ b → a ↪ c (f ∘Mono g) .mor = f .mor ∘ g .mor (f ∘Mono g) .monic = ∘-is-monic (f .monic) (g .monic) _∘Epi_ : ∀ {a b c} → b ↠ c → a ↠ b → a ↠ c (f ∘Epi g) .mor = f .mor ∘ g .mor (f ∘Epi g) .epic = ∘-is-epic (f .epic) (g .epic)
If is monic, then must also be monic.
monic-cancell : ∀ {a b c} {f : Hom b c} {g : Hom a b} → is-monic (f ∘ g) → is-monic g monic-cancell {f = f} fg-monic h h' p = fg-monic h h' $ sym (assoc _ _ _) ∙∙ ap (f ∘_) p ∙∙ assoc _ _ _
Dually, if is epic, then must also be epic.
epic-cancelr : ∀ {a b c} {f : Hom b c} {g : Hom a b} → is-epic (f ∘ g) → is-epic f epic-cancelr {g = g} fg-epic h h' p = fg-epic h h' $ assoc _ _ _ ∙∙ ap (_∘ g) p ∙∙ sym (assoc _ _ _)
Postcomposition with a mono is an embedding.
monic-postcomp-embedding : ∀ {a b c} {f : Hom b c} → is-monic f → is-embedding {A = Hom a b} (f ∘_) monic-postcomp-embedding monic = injective→is-embedding (Hom-set _ _) _ (monic _ _)
Likewise, precomposition with an epi is an embedding.
epic-precomp-embedding : ∀ {a b c} {f : Hom a b} → is-epic f → is-embedding {A = Hom b c} (_∘ f) epic-precomp-embedding epic = injective→is-embedding (Hom-set _ _) _ (epic _ _)
subst-is-monic : ∀ {a b} {f g : Hom a b} → f ≡ g → is-monic f → is-monic g subst-is-monic f=g f-monic h i p = f-monic h i (ap (_∘ h) f=g ∙∙ p ∙∙ ap (_∘ i) (sym f=g)) subst-is-epic : ∀ {a b} {f g : Hom a b} → f ≡ g → is-epic f → is-epic g subst-is-epic f=g f-epic h i p = f-epic h i (ap (h ∘_) f=g ∙∙ p ∙∙ ap (i ∘_) (sym f=g))
Sections🔗
A morphism is a section of another morphism when The intuition for this name is that picks out a cross-section of from For instance, could map animals to their species; a section of this map would have to pick out a canonical representative of each species from the set of all animals.
_section-of_ : (s : Hom b a) (r : Hom a b) → Type _ s section-of r = r ∘ s ≡ id section-of-is-prop : ∀ {s : Hom b a} {r : Hom a b} → is-prop (s section-of r) section-of-is-prop = Hom-set _ _ _ _ record has-section (r : Hom a b) : Type h where constructor make-section field section : Hom b a is-section : section section-of r open has-section public
The identity map has a section (namely, itself), and the composite of maps with sections also has a section.
id-has-section : ∀ {a} → has-section (id {a}) id-has-section .section = id id-has-section .is-section = idl _ section-of-∘ : ∀ {a b c} {f : Hom c b} {g : Hom b c} {h : Hom b a} {i : Hom a b} → f section-of g → h section-of i → (h ∘ f) section-of (g ∘ i) section-of-∘ {f = f} {g = g} {h = h} {i = i} fg-sect hi-sect = (g ∘ i) ∘ h ∘ f ≡⟨ cat! C ⟩≡ g ∘ (i ∘ h) ∘ f ≡⟨ ap (λ ϕ → g ∘ ϕ ∘ f) hi-sect ⟩≡ g ∘ id ∘ f ≡⟨ ap (g ∘_) (idl _) ⟩≡ g ∘ f ≡⟨ fg-sect ⟩≡ id ∎ section-∘ : ∀ {a b c} {f : Hom b c} {g : Hom a b} → has-section f → has-section g → has-section (f ∘ g) section-∘ f-sect g-sect .section = g-sect .section ∘ f-sect .section section-∘ {f = f} {g = g} f-sect g-sect .is-section = section-of-∘ (f-sect .is-section) (g-sect .is-section)
Moreover, if has a section, then so does
section-cancell : ∀ {a b c} {f : Hom b c} {g : Hom a b} → has-section (f ∘ g) → has-section f section-cancell {g = g} s .section = g ∘ s .section section-cancell {g = g} s .is-section = assoc _ _ _ ∙ s .is-section
If has a section, then is epic.
has-section→epic : ∀ {a b} {f : Hom a b} → has-section f → is-epic f has-section→epic {f = f} f-sect g h p = g ≡˘⟨ idr _ ⟩≡˘ g ∘ id ≡˘⟨ ap (g ∘_) (f-sect .is-section) ⟩≡˘ g ∘ f ∘ f-sect .section ≡⟨ assoc _ _ _ ⟩≡ (g ∘ f) ∘ f-sect .section ≡⟨ ap (_∘ f-sect .section) p ⟩≡ (h ∘ f) ∘ f-sect .section ≡˘⟨ assoc _ _ _ ⟩≡˘ h ∘ f ∘ f-sect .section ≡⟨ ap (h ∘_) (f-sect .is-section) ⟩≡ h ∘ id ≡⟨ idr _ ⟩≡ h ∎
has-section-precomp-embedding : ∀ {a b c} {f : Hom a b} → has-section f → is-embedding {A = Hom b c} (_∘ f) has-section-precomp-embedding f-section = epic-precomp-embedding (has-section→epic f-section)
subst-section : ∀ {a b} {f g : Hom a b} → f ≡ g → has-section f → has-section g subst-section p s .section = s .section subst-section p s .is-section = ap₂ _∘_ (sym p) refl ∙ s .is-section
Retracts🔗
A morphism is a retract of another morphism when Note that this is the same equation involved in the definition of a section; retracts and sections always come in pairs. If sections solve a sort of “curation problem” where we are asked to pick out canonical representatives, then retracts solve a sort of “classification problem”.
_retract-of_ : (r : Hom a b) (s : Hom b a) → Type _ r retract-of s = r ∘ s ≡ id retract-of-is-prop : ∀ {s : Hom b a} {r : Hom a b} → is-prop (r retract-of s) retract-of-is-prop = Hom-set _ _ _ _ record has-retract (s : Hom b a) : Type h where constructor make-retract field retract : Hom a b is-retract : retract retract-of s open has-retract public
The identity map has a retract (namely, itself), and the composite of maps with retracts also has a retract.
id-has-retract : ∀ {a} → has-retract (id {a}) id-has-retract .retract = id id-has-retract .is-retract = idl _ retract-of-∘ : ∀ {a b c} {f : Hom c b} {g : Hom b c} {h : Hom b a} {i : Hom a b} → f retract-of g → h retract-of i → (h ∘ f) retract-of (g ∘ i) retract-of-∘ fg-ret hi-ret = section-of-∘ hi-ret fg-ret retract-∘ : ∀ {a b c} {f : Hom b c} {g : Hom a b} → has-retract f → has-retract g → has-retract (f ∘ g) retract-∘ f-ret g-ret .retract = g-ret .retract ∘ f-ret .retract retract-∘ f-ret g-ret .is-retract = retract-of-∘ (f-ret .is-retract) (g-ret .is-retract)
If has a retract, then so does
retract-cancelr : ∀ {a b c} {f : Hom b c} {g : Hom a b} → has-retract (f ∘ g) → has-retract g retract-cancelr {f = f} r .retract = r .retract ∘ f retract-cancelr {f = f} r .is-retract = sym (assoc _ _ _) ∙ r .is-retract
If has a retract, then is monic.
has-retract→monic : ∀ {a b} {f : Hom a b} → has-retract f → is-monic f has-retract→monic {f = f} f-ret g h p = g ≡˘⟨ idl _ ⟩≡˘ id ∘ g ≡˘⟨ ap (_∘ g) (f-ret .is-retract) ⟩≡˘ (f-ret .retract ∘ f) ∘ g ≡˘⟨ assoc _ _ _ ⟩≡˘ f-ret .retract ∘ (f ∘ g) ≡⟨ ap (f-ret .retract ∘_) p ⟩≡ f-ret .retract ∘ f ∘ h ≡⟨ assoc _ _ _ ⟩≡ (f-ret .retract ∘ f) ∘ h ≡⟨ ap (_∘ h) (f-ret .is-retract) ⟩≡ id ∘ h ≡⟨ idl _ ⟩≡ h ∎
has-retract-postcomp-embedding : ∀ {a b c} {f : Hom b c} → has-retract f → is-embedding {A = Hom a b} (f ∘_) has-retract-postcomp-embedding f-retract = monic-postcomp-embedding (has-retract→monic f-retract)
A section that is also epic is a retract.
section-of+epic→retract-of : ∀ {a b} {s : Hom b a} {r : Hom a b} → s section-of r → is-epic s → s retract-of r section-of+epic→retract-of {s = s} {r = r} sect epic = epic (s ∘ r) id $ (s ∘ r) ∘ s ≡˘⟨ assoc s r s ⟩≡˘ s ∘ (r ∘ s) ≡⟨ ap (s ∘_) sect ⟩≡ s ∘ id ≡⟨ idr _ ⟩≡ s ≡˘⟨ idl _ ⟩≡˘ id ∘ s ∎
Dually, a retract that is also monic is a section.
retract-of+monic→section-of : ∀ {a b} {s : Hom b a} {r : Hom a b} → r retract-of s → is-monic r → r section-of s retract-of+monic→section-of {s = s} {r = r} ret monic = monic (s ∘ r) id $ r ∘ s ∘ r ≡⟨ assoc r s r ⟩≡ (r ∘ s) ∘ r ≡⟨ ap (_∘ r) ret ⟩≡ id ∘ r ≡⟨ idl _ ⟩≡ r ≡˘⟨ idr _ ⟩≡˘ r ∘ id ∎
has-retract+epic→has-section : ∀ {a b} {f : Hom a b} → has-retract f → is-epic f → has-section f has-retract+epic→has-section ret epic .section = ret .retract has-retract+epic→has-section ret epic .is-section = section-of+epic→retract-of (ret .is-retract) epic has-section+monic→has-retract : ∀ {a b} {f : Hom a b} → has-section f → is-monic f → has-retract f has-section+monic→has-retract sect monic .retract = sect .section has-section+monic→has-retract sect monic .is-retract = retract-of+monic→section-of (sect .is-section) monic
Split monomorphisms🔗
A morphism is a split monomorphism if it merely has a retract.
is-split-monic : Hom a b → Type _ is-split-monic f = ∥ has-retract f ∥
Every split mono is a mono, as being monic is a proposition.
split-monic→mono : is-split-monic f → is-monic f split-monic→mono = rec! has-retract→monic
Split epimorphisms🔗
Dually, a morphism is a split epimorphism if it merely has a section.
is-split-epic : Hom a b → Type _ is-split-epic f = ∥ has-section f ∥
Like split monos, every split epimorphism is an epimorphism.
split-epic→epic : is-split-epic f → is-epic f split-epic→epic = rec! has-section→epic
Isos🔗
Maps and are inverses when we have and both equal to the identity. A map is invertible (or is an isomorphism) when there exists a for which and are inverses. An isomorphism is a choice of map together with a specified inverse.
record Inverses (f : Hom a b) (g : Hom b a) : Type h where field invl : f ∘ g ≡ id invr : g ∘ f ≡ id open Inverses record is-invertible (f : Hom a b) : Type h where field inv : Hom b a inverses : Inverses f inv open Inverses inverses public op : is-invertible inv op = record { inv = f ; inverses = record { invl = invr inverses ; invr = invl inverses }} record _≅_ (a b : Ob) : Type h where field to : Hom a b from : Hom b a inverses : Inverses to from open Inverses inverses public
A given map is invertible in at most one way: If you have with two inverses and then not only are equal, but the witnesses of these equalities are irrelevant.
Inverses-are-prop : ∀ {f : Hom a b} {g : Hom b a} → is-prop (Inverses f g) Inverses-are-prop x y i .Inverses.invl = Hom-set _ _ _ _ (x .invl) (y .invl) i Inverses-are-prop x y i .Inverses.invr = Hom-set _ _ _ _ (x .invr) (y .invr) i is-invertible-is-prop : ∀ {f : Hom a b} → is-prop (is-invertible f) is-invertible-is-prop {a = a} {b = b} {f = f} g h = p where module g = is-invertible g module h = is-invertible h g≡h : g.inv ≡ h.inv g≡h = g.inv ≡⟨ sym (idr _) ∙ ap₂ _∘_ refl (sym h.invl) ⟩≡ g.inv ∘ f ∘ h.inv ≡⟨ assoc _ _ _ ∙∙ ap₂ _∘_ g.invr refl ∙∙ idl _ ⟩≡ h.inv ∎ p : g ≡ h p i .is-invertible.inv = g≡h i p i .is-invertible.inverses = is-prop→pathp (λ i → Inverses-are-prop {g = g≡h i}) g.inverses h.inverses i
We note that the identity morphism is always iso, and that isos compose:
id-invertible : ∀ {a} → is-invertible (id {a}) id-invertible .is-invertible.inv = id id-invertible .is-invertible.inverses .invl = idl id id-invertible .is-invertible.inverses .invr = idl id id-iso : a ≅ a id-iso .to = id id-iso .from = id id-iso .inverses .invl = idl id id-iso .inverses .invr = idl id Isomorphism = _≅_ Inverses-∘ : {a b c : Ob} {f : Hom b c} {f⁻¹ : Hom c b} {g : Hom a b} {g⁻¹ : Hom b a} → Inverses f f⁻¹ → Inverses g g⁻¹ → Inverses (f ∘ g) (g⁻¹ ∘ f⁻¹) Inverses-∘ {f = f} {f⁻¹} {g} {g⁻¹} finv ginv = record { invl = l ; invr = r } where module finv = Inverses finv module ginv = Inverses ginv abstract l : (f ∘ g) ∘ g⁻¹ ∘ f⁻¹ ≡ id l = (f ∘ g) ∘ g⁻¹ ∘ f⁻¹ ≡⟨ cat! C ⟩≡ f ∘ (g ∘ g⁻¹) ∘ f⁻¹ ≡⟨ (λ i → f ∘ ginv.invl i ∘ f⁻¹) ⟩≡ f ∘ id ∘ f⁻¹ ≡⟨ cat! C ⟩≡ f ∘ f⁻¹ ≡⟨ finv.invl ⟩≡ id ∎ r : (g⁻¹ ∘ f⁻¹) ∘ f ∘ g ≡ id r = (g⁻¹ ∘ f⁻¹) ∘ f ∘ g ≡⟨ cat! C ⟩≡ g⁻¹ ∘ (f⁻¹ ∘ f) ∘ g ≡⟨ (λ i → g⁻¹ ∘ finv.invr i ∘ g) ⟩≡ g⁻¹ ∘ id ∘ g ≡⟨ cat! C ⟩≡ g⁻¹ ∘ g ≡⟨ ginv.invr ⟩≡ id ∎ _∘Iso_ : ∀ {a b c : Ob} → b ≅ c → a ≅ b → a ≅ c (f ∘Iso g) .to = f .to ∘ g .to (f ∘Iso g) .from = g .from ∘ f .from (f ∘Iso g) .inverses = Inverses-∘ (f .inverses) (g .inverses) _∙Iso_ : ∀ {a b c : Ob} → a ≅ b → b ≅ c → a ≅ c f ∙Iso g = g ∘Iso f infixr 40 _∘Iso_ _∙Iso_ infixr 41 _Iso⁻¹ invertible-∘ : ∀ {f : Hom b c} {g : Hom a b} → is-invertible f → is-invertible g → is-invertible (f ∘ g) invertible-∘ f-inv g-inv = record { inv = g-inv.inv ∘ f-inv.inv ; inverses = Inverses-∘ f-inv.inverses g-inv.inverses } where module f-inv = is-invertible f-inv module g-inv = is-invertible g-inv _invertible⁻¹ : ∀ {f : Hom a b} → (f-inv : is-invertible f) → is-invertible (is-invertible.inv f-inv) _invertible⁻¹ {f = f} f-inv .is-invertible.inv = f _invertible⁻¹ f-inv .is-invertible.inverses .invl = is-invertible.invr f-inv _invertible⁻¹ f-inv .is-invertible.inverses .invr = is-invertible.invl f-inv _Iso⁻¹ : a ≅ b → b ≅ a (f Iso⁻¹) .to = f .from (f Iso⁻¹) .from = f .to (f Iso⁻¹) .inverses .invl = f .inverses .invr (f Iso⁻¹) .inverses .invr = f .inverses .invl
make-inverses : {f : Hom a b} {g : Hom b a} → f ∘ g ≡ id → g ∘ f ≡ id → Inverses f g make-inverses p q .invl = p make-inverses p q .invr = q make-invertible : {f : Hom a b} → (g : Hom b a) → f ∘ g ≡ id → g ∘ f ≡ id → is-invertible f make-invertible g p q .is-invertible.inv = g make-invertible g p q .is-invertible.inverses .invl = p make-invertible g p q .is-invertible.inverses .invr = q make-iso : (f : Hom a b) (g : Hom b a) → f ∘ g ≡ id → g ∘ f ≡ id → a ≅ b {-# INLINE make-iso #-} make-iso f g p q = record { to = f ; from = g ; inverses = record { invl = p ; invr = q }} make-iso! : ∀ {ℓr ℓs} (f : Hom a b) (g : Hom b a) → ⦃ r : Extensional (Hom a a) ℓr ⦄ ⦃ s : Extensional (Hom b b) ℓs ⦄ → Pathᵉ s (f ∘ g) id → Pathᵉ r (g ∘ f) id → a ≅ b {-# INLINE make-iso! #-} make-iso! f g p q = record { to = f ; from = g ; inverses = record { invl = ext p ; invr = ext q }} inverses→invertible : ∀ {f : Hom a b} {g : Hom b a} → Inverses f g → is-invertible f inverses→invertible x .is-invertible.inv = _ inverses→invertible x .is-invertible.inverses = x involution→invertible : (f : Hom a a) → f ∘ f ≡ id → is-invertible f involution→invertible f inv = make-invertible f inv inv involution→iso : (f : Hom a a) → f ∘ f ≡ id → a ≅ a involution→iso f inv = make-iso f f inv inv _≅⟨_⟩_ : ∀ (x : Ob) {y z} → x ≅ y → y ≅ z → x ≅ z x ≅⟨ p ⟩≅ q = q ∘Iso p _≅˘⟨_⟩_ : ∀ (x : Ob) {y z} → y ≅ x → y ≅ z → x ≅ z x ≅˘⟨ p ⟩≅˘ q = q ∘Iso p Iso⁻¹ _≅∎ : (x : Ob) → x ≅ x x ≅∎ = id-iso infixr 2 _≅⟨_⟩_ _≅˘⟨_⟩_ infix 3 _≅∎ invertible→iso : (f : Hom a b) → is-invertible f → a ≅ b invertible→iso f x = record { to = f ; from = x .is-invertible.inv ; inverses = x .is-invertible.inverses } is-invertible-inverse : {f : Hom a b} (g : is-invertible f) → is-invertible (g .is-invertible.inv) is-invertible-inverse g = record { inv = _ ; inverses = record { invl = invr g ; invr = invl g } } where open Inverses (g .is-invertible.inverses) iso→invertible : (i : a ≅ b) → is-invertible (i ._≅_.to) iso→invertible i = record { inv = i ._≅_.from ; inverses = i ._≅_.inverses } private ≅-pathp-internal : (p : a ≡ c) (q : b ≡ d) → {f : a ≅ b} {g : c ≅ d} → PathP (λ i → Hom (p i) (q i)) (f ._≅_.to) (g ._≅_.to) → PathP (λ i → Hom (q i) (p i)) (f ._≅_.from) (g ._≅_.from) → PathP (λ i → p i ≅ q i) f g ≅-pathp-internal p q r s i .to = r i ≅-pathp-internal p q r s i .from = s i ≅-pathp-internal p q {f} {g} r s i .inverses = is-prop→pathp (λ j → Inverses-are-prop {f = r j} {g = s j}) (f .inverses) (g .inverses) i
The following lemma is useful when we have a commutative diagram of morphisms which are all known to be isomorphisms, which we want to “flip around” by way of inversion. For example, given all the morphisms in
are isomorphisms, we can use inverse-unique to get an
equality
This is used, for example, in opposite
monoidal category to invert the triangle and pentagon
identities.
abstract inverse-unique : {x y : Ob} (p : x ≡ y) {b d : Ob} (q : b ≡ d) (f : x ≅ b) (g : y ≅ d) → PathP (λ i → Hom (p i) (q i)) (f .to) (g .to) → PathP (λ i → Hom (q i) (p i)) (f .from) (g .from)
We prove this by J'-induction
on the simpler case where
and
definitionally.
inverse-unique₀ : {x b : Ob} (f g : x ≅ b) → f .to ≡ g .to → f .from ≡ g .from inverse-unique₀ {x} {b} f g r = f .from ≡˘⟨ ap (f .from ∘_) (g .invl) ∙ idr _ ⟩≡˘ f .from ∘ g .to ∘ g .from ≡⟨ assoc _ _ _ ⟩≡ (f .from ∘ g .to) ∘ g .from ≡⟨ ap (_∘ g .from) (ap (f .from ∘_) (sym r) ∙ f .invr) ∙ idl _ ⟩≡ g .from ∎
Definition of inverse-unique
by induction.
inverse-unique = J' (λ a c p → ∀ {b d} (q : b ≡ d) (f : a ≅ b) (g : c ≅ d) → PathP (λ i → Hom (p i) (q i)) (f .to) (g .to) → PathP (λ i → Hom (q i) (p i)) (f .from) (g .from)) λ x → J' (λ b d q → (f : x ≅ b) (g : x ≅ d) → PathP (λ i → Hom x (q i)) (f .to) (g .to) → PathP (λ i → Hom (q i) x) (f .from) (g .from)) λ y → inverse-unique₀
This may in turn be used to characterize paths between isomorphisms:
≅-pathp : (p : a ≡ c) (q : b ≡ d) {f : a ≅ b} {g : c ≅ d} → PathP (λ i → Hom (p i) (q i)) (f ._≅_.to) (g ._≅_.to) → PathP (λ i → p i ≅ q i) f g ≅-pathp p q {f = f} {g = g} r = ≅-pathp-internal p q r (inverse-unique p q f g r)
Alternate characterizations to ≅-pathp.
≅-pathp-from : (p : a ≡ c) (q : b ≡ d) {f : a ≅ b} {g : c ≅ d} → PathP (λ i → Hom (q i) (p i)) (f ._≅_.from) (g ._≅_.from) → PathP (λ i → p i ≅ q i) f g ≅-pathp-from p q {f = f} {g = g} r = ≅-pathp-internal p q (inverse-unique q p (f Iso⁻¹) (g Iso⁻¹) r) r ≅-path : {f g : a ≅ b} → f ._≅_.to ≡ g ._≅_.to → f ≡ g ≅-path = ≅-pathp refl refl ≅-path-from : {f g : a ≅ b} → f ._≅_.from ≡ g ._≅_.from → f ≡ g ≅-path-from = ≅-pathp-from refl refl
≅-is-contr : (∀ {a b} → is-contr (Hom a b)) → is-contr (a ≅ b) ≅-is-contr hom-contr .centre = make-iso (hom-contr .centre) (hom-contr .centre) (is-contr→is-prop hom-contr _ _) (is-contr→is-prop hom-contr _ _) ≅-is-contr hom-contr .paths f = ≅-path (hom-contr .paths (f .to)) iso≃is-invertible : ∀ {a b} → (a ≅ b) ≃ (Σ[ f ∈ Hom a b ] is-invertible f) iso≃is-invertible .fst f .fst = f .to iso≃is-invertible .fst f .snd = iso→invertible f iso≃is-invertible .snd .is-eqv (f , f-inv) .centre = strict-fibres (uncurry invertible→iso) (f , f-inv) .fst iso≃is-invertible .snd .is-eqv (f , f-inv) .paths = strict-fibres (uncurry invertible→iso) (f , f-inv) .snd ≅-is-prop : (∀ {a b} → is-prop (Hom a b)) → is-prop (a ≅ b) ≅-is-prop hom-prop f g = ≅-path (hom-prop (f .to) (g .to)) ↪-pathp : {a : I → Ob} {b : I → Ob} {f : a i0 ↪ b i0} {g : a i1 ↪ b i1} → PathP (λ i → Hom (a i) (b i)) (f .mor) (g .mor) → PathP (λ i → a i ↪ b i) f g ↪-pathp {a = a} {b} {f} {g} pa = go where go : PathP (λ i → a i ↪ b i) f g go i .mor = pa i go i .monic {c = c} = is-prop→pathp (λ i → Π-is-hlevel {A = Hom c (a i)} 1 λ g → Π-is-hlevel {A = Hom c (a i)} 1 λ h → fun-is-hlevel {A = pa i ∘ g ≡ pa i ∘ h} 1 (Hom-set c (a i) g h)) (f .monic) (g .monic) i ↠-pathp : {a : I → Ob} {b : I → Ob} {f : a i0 ↠ b i0} {g : a i1 ↠ b i1} → PathP (λ i → Hom (a i) (b i)) (f .mor) (g .mor) → PathP (λ i → a i ↠ b i) f g ↠-pathp {a = a} {b} {f} {g} pa = go where go : PathP (λ i → a i ↠ b i) f g go i .mor = pa i go i .epic {c = c} = is-prop→pathp (λ i → Π-is-hlevel {A = Hom (b i) c} 1 λ g → Π-is-hlevel {A = Hom (b i) c} 1 λ h → fun-is-hlevel {A = g ∘ pa i ≡ h ∘ pa i} 1 (Hom-set (b i) c g h)) (f .epic) (g .epic) i subst-is-invertible : ∀ {x y} {f g : Hom x y} → f ≡ g → is-invertible f → is-invertible g subst-is-invertible f=g f-inv = make-invertible f.inv (ap (_∘ f.inv) (sym f=g) ∙ f.invl) (ap (f.inv ∘_) (sym f=g) ∙ f.invr) where module f = is-invertible f-inv
Isomorphisms enjoy a 2-out-of-3 property: if any 2 of and are isomorphisms, then so is the third.
inverses-cancell : ∀ {f : Hom b c} {g : Hom a b} {g⁻¹ : Hom b a} {fg⁻¹ : Hom c a} → Inverses g g⁻¹ → Inverses (f ∘ g) fg⁻¹ → Inverses f (g ∘ fg⁻¹) inverses-cancelr : ∀ {f : Hom b c} {f⁻¹ : Hom c b} {g : Hom a b} {fg⁻¹ : Hom c a} → Inverses f f⁻¹ → Inverses (f ∘ g) fg⁻¹ → Inverses g (fg⁻¹ ∘ f) invertible-cancell : ∀ {f : Hom b c} {g : Hom a b} → is-invertible g → is-invertible (f ∘ g) → is-invertible f invertible-cancelr : ∀ {f : Hom b c} {g : Hom a b} → is-invertible f → is-invertible (f ∘ g) → is-invertible g
We are early into our bootstrapping process for category theory, so the proofs of these lemmas are quite low-level, and thus omitted.
inverses-cancell g-inv fg-inv .invl = assoc _ _ _ ∙ fg-inv .invl inverses-cancell g-inv fg-inv .invr = sym (idr _) ∙ ap₂ _∘_ refl (sym (g-inv .invl)) ∙ assoc _ _ _ ∙ ap₂ _∘_ (sym (assoc _ _ _) ∙ sym (assoc _ _ _) ∙ ap₂ _∘_ refl (fg-inv .invr) ∙ idr _) refl ∙ g-inv .invl inverses-cancelr f-inv fg-inv .invl = sym (idl _) ∙ ap₂ _∘_ (sym (f-inv .invr)) refl ∙ sym (assoc _ _ _) ∙ ap₂ _∘_ refl (assoc _ _ _ ∙ assoc _ _ _ ∙ ap₂ _∘_ (fg-inv .invl) refl ∙ idl _) ∙ f-inv .invr inverses-cancelr f-inv fg-inv .invr = sym (assoc _ _ _) ∙ fg-inv .invr invertible-cancell g-inv fg-inv = inverses→invertible $ inverses-cancell (g-inv .is-invertible.inverses) (fg-inv .is-invertible.inverses) invertible-cancelr f-inv fg-inv = inverses→invertible $ inverses-cancelr (f-inv .is-invertible.inverses) (fg-inv .is-invertible.inverses)
We also note that invertible morphisms are both epic and monic.
invertible→monic : is-invertible f → is-monic f invertible→monic {f = f} invert g h p = g ≡˘⟨ idl g ⟩≡˘ id ∘ g ≡˘⟨ ap (_∘ g) (is-invertible.invr invert) ⟩≡˘ (inv ∘ f) ∘ g ≡˘⟨ assoc inv f g ⟩≡˘ inv ∘ (f ∘ g) ≡⟨ ap (inv ∘_) p ⟩≡ inv ∘ (f ∘ h) ≡⟨ assoc inv f h ⟩≡ (inv ∘ f) ∘ h ≡⟨ ap (_∘ h) (is-invertible.invr invert) ⟩≡ id ∘ h ≡⟨ idl h ⟩≡ h ∎ where open is-invertible invert invertible→epic : is-invertible f → is-epic f invertible→epic {f = f} invert g h p = g ≡˘⟨ idr g ⟩≡˘ g ∘ id ≡˘⟨ ap (g ∘_) (is-invertible.invl invert) ⟩≡˘ g ∘ (f ∘ inv) ≡⟨ assoc g f inv ⟩≡ (g ∘ f) ∘ inv ≡⟨ ap (_∘ inv) p ⟩≡ (h ∘ f) ∘ inv ≡˘⟨ assoc h f inv ⟩≡˘ h ∘ (f ∘ inv) ≡⟨ ap (h ∘_) (is-invertible.invl invert) ⟩≡ h ∘ id ≡⟨ idr h ⟩≡ h ∎ where open is-invertible invert iso→monic : (f : a ≅ b) → is-monic (f .to) iso→monic f = invertible→monic (iso→invertible f) iso→epic : (f : a ≅ b) → is-epic (f .to) iso→epic f = invertible→epic (iso→invertible f)
Furthermore, isomorphisms also yield section/retraction pairs.
inverses→to-has-section : ∀ {f : Hom a b} {g : Hom b a} → Inverses f g → has-section f inverses→to-has-section {g = g} inv .section = g inverses→to-has-section inv .is-section = Inverses.invl inv inverses→from-has-section : ∀ {f : Hom a b} {g : Hom b a} → Inverses f g → has-section g inverses→from-has-section {f = f} inv .section = f inverses→from-has-section inv .is-section = Inverses.invr inv inverses→to-has-retract : ∀ {f : Hom a b} {g : Hom b a} → Inverses f g → has-retract f inverses→to-has-retract {g = g} inv .retract = g inverses→to-has-retract inv .is-retract = Inverses.invr inv inverses→from-has-retract : ∀ {f : Hom a b} {g : Hom b a} → Inverses f g → has-retract g inverses→from-has-retract {f = f} inv .retract = f inverses→from-has-retract inv .is-retract = Inverses.invl inv
module _ {f : Hom a b} (f-inv : is-invertible f) where private module f = is-invertible f-inv invertible→to-has-section : has-section f invertible→to-has-section .section = f.inv invertible→to-has-section .is-section = f.invl invertible→to-has-retract : has-retract f invertible→to-has-retract .retract = f.inv invertible→to-has-retract .is-retract = f.invr invertible→to-split-monic : is-split-monic f invertible→to-split-monic = pure invertible→to-has-retract invertible→to-split-epic : is-split-epic f invertible→to-split-epic = pure invertible→to-has-section invertible→from-has-section : has-section f.inv invertible→from-has-section .section = f invertible→from-has-section .is-section = f.invr invertible→from-has-retract : has-retract f.inv invertible→from-has-retract .retract = f invertible→from-has-retract .is-retract = f.invl iso→to-has-section : (f : a ≅ b) → has-section (f .to) iso→to-has-section f .section = f .from iso→to-has-section f .is-section = f .invl iso→from-has-section : (f : a ≅ b) → has-section (f .from) iso→from-has-section f .section = f .to iso→from-has-section f .is-section = f .invr iso→to-has-retract : (f : a ≅ b) → has-retract (f .to) iso→to-has-retract f .retract = f .from iso→to-has-retract f .is-retract = f .invr iso→from-has-retract : (f : a ≅ b) → has-retract (f .from) iso→from-has-retract f .retract = f .to iso→from-has-retract f .is-retract = f .invl
Using our lemmas about section/retraction pairs from before, we can show that if is a monic retract, then is an iso.
retract-of+monic→inverses : ∀ {a b} {s : Hom b a} {r : Hom a b} → r retract-of s → is-monic r → Inverses r s retract-of+monic→inverses ret monic .invl = ret retract-of+monic→inverses ret monic .invr = retract-of+monic→section-of ret monic
We also have a dual result for sections and epis.
section-of+epic→inverses : ∀ {a b} {s : Hom b a} {r : Hom a b} → s retract-of r → is-epic r → Inverses r s section-of+epic→inverses sect epic .invl = section-of+epic→retract-of sect epic section-of+epic→inverses sect epic .invr = sect
has-retract+epic→invertible : ∀ {a b} {f : Hom a b} → has-retract f → is-epic f → is-invertible f has-retract+epic→invertible f-ret epic .is-invertible.inv = f-ret .retract has-retract+epic→invertible f-ret epic .is-invertible.inverses = section-of+epic→inverses (f-ret .is-retract) epic has-section+monic→invertible : ∀ {a b} {f : Hom a b} → has-section f → is-monic f → is-invertible f has-section+monic→invertible f-sect monic .is-invertible.inv = f-sect .section has-section+monic→invertible f-sect monic .is-invertible.inverses = retract-of+monic→inverses (f-sect .is-section) monic
In fact, the mere existence of a retract of an epimorphism suffices to show that is invertible, as invertibility itself is a proposition. Put another way, every morphism that is both a split mono and an epi is invertible.
split-monic+epic→invertible : is-split-monic f → is-epic f → is-invertible f split-monic+epic→invertible f-split-monic f-epic = ∥-∥-rec is-invertible-is-prop (λ r → has-retract+epic→invertible r f-epic) f-split-monic
A dual result holds for morphisms that are simultaneously split epic and monic.
split-epic+monic→invertible : is-split-epic f → is-monic f → is-invertible f
split-epic+monic→invertible f-split-epic f-monic = ∥-∥-rec is-invertible-is-prop (λ s → has-section+monic→invertible s f-monic) f-split-epic
Hom-sets between isomorphic objects are equivalent. Crucially, this allows us to use univalence to transport properties between hom-sets.
iso→hom-equiv : ∀ {a a' b b'} → a ≅ a' → b ≅ b' → Hom a b ≃ Hom a' b' iso→hom-equiv f g = Iso→Equiv $ (λ h → g .to ∘ h ∘ f .from) , iso (λ h → g .from ∘ h ∘ f .to ) (λ h → g .to ∘ (g .from ∘ h ∘ f .to) ∘ f .from ≡⟨ cat! C ⟩≡ (g .to ∘ g .from) ∘ h ∘ (f .to ∘ f .from) ≡⟨ ap₂ (λ l r → l ∘ h ∘ r) (g .invl) (f .invl) ⟩≡ id ∘ h ∘ id ≡⟨ cat! C ⟩≡ h ∎) (λ h → g .from ∘ (g .to ∘ h ∘ f .from) ∘ f .to ≡⟨ cat! C ⟩≡ (g .from ∘ g .to) ∘ h ∘ (f .from ∘ f .to) ≡⟨ ap₂ (λ l r → l ∘ h ∘ r) (g .invr) (f .invr) ⟩≡ id ∘ h ∘ id ≡⟨ cat! C ⟩≡ h ∎)
-- Optimized versions of Iso→Hom-equiv which yield nicer results -- if only one isomorphism is needed. dom-iso→hom-equiv : ∀ {a a' b} → a ≅ a' → Hom a b ≃ Hom a' b dom-iso→hom-equiv f .fst h = h ∘ f .from dom-iso→hom-equiv f .snd = is-iso→is-equiv record { from = _∘ f .to ; rinv = λ h → (h ∘ f .to) ∘ f .from ≡⟨ sym (assoc _ _ _) ⟩≡ h ∘ (f .to ∘ f .from) ≡⟨ ap (h ∘_) (f .invl) ⟩≡ h ∘ id ≡⟨ idr _ ⟩≡ h ∎ ; linv = λ h → (h ∘ f .from) ∘ f .to ≡⟨ sym (assoc _ _ _) ⟩≡ h ∘ (f .from ∘ f .to) ≡⟨ ap (h ∘_) (f .invr) ⟩≡ h ∘ id ≡⟨ idr _ ⟩≡ h ∎ } cod-iso→hom-equiv : ∀ {a b b'} → b ≅ b' → Hom a b ≃ Hom a b' cod-iso→hom-equiv f .fst h = f .to ∘ h cod-iso→hom-equiv f .snd = is-iso→is-equiv record { from = f .from ∘_ ; rinv = λ h → f .to ∘ f .from ∘ h ≡⟨ assoc _ _ _ ⟩≡ (f .to ∘ f .from) ∘ h ≡⟨ ap (_∘ h) (f .invl) ⟩≡ id ∘ h ≡⟨ idl _ ⟩≡ h ∎ ; linv = λ h → f .from ∘ f .to ∘ h ≡⟨ assoc _ _ _ ⟩≡ (f .from ∘ f .to) ∘ h ≡⟨ ap (_∘ h) (f .invr) ⟩≡ id ∘ h ≡⟨ idl _ ⟩≡ h ∎ }
If is invertible, then both pre and post-composition with are equivalences.
invertible-precomp-equiv : ∀ {a b c} {f : Hom a b} → is-invertible f → is-equiv {A = Hom b c} (_∘ f) invertible-precomp-equiv {f = f} f-inv = is-iso→is-equiv $ iso (λ h → h ∘ f-inv.inv) (λ h → sym (assoc _ _ _) ∙∙ ap (h ∘_) f-inv.invr ∙∙ idr h) (λ h → sym (assoc _ _ _) ∙∙ ap (h ∘_) f-inv.invl ∙∙ idr h) where module f-inv = is-invertible f-inv invertible-postcomp-equiv : ∀ {a b c} {f : Hom b c} → is-invertible f → is-equiv {A = Hom a b} (f ∘_) invertible-postcomp-equiv {f = f} f-inv = is-iso→is-equiv $ iso (λ h → f-inv.inv ∘ h) (λ h → assoc _ _ _ ∙∙ ap (_∘ h) f-inv.invl ∙∙ idl h) (λ h → assoc _ _ _ ∙∙ ap (_∘ h) f-inv.invr ∙∙ idl h) where module f-inv = is-invertible f-inv