I: 2: b: show isomorphisms decomposeI-2-c

1 files changed, 27 insertions, 2 deletions

diff --git a/src/CatTheory/Morphism/Properties.agda b/src/CatTheory/Morphism/Properties.agda
index d0a6e7b..e268a6e 100644
--- a/src/CatTheory/Morphism/Properties.agda
+++ b/src/CatTheory/Morphism/Properties.agda
@@ -6,9 +6,12 @@ module CatTheory.Morphism.Properties {o ℓ e} (𝒞 : Category o ℓ e) where
 open Category 𝒞
 open HomReasoning
 
-import Categories.Morphism as M
-open M 𝒞
+open import Categories.Morphism 𝒞
 open import Categories.Morphism.Reasoning 𝒞
+open import Function using (_$_)
+
+import Categories.Morphism.Properties as Mₚ
+module Cheat! = Mₚ 𝒞
 
 private
   variable
@@ -27,3 +30,25 @@ Iso-∘ {f = f} {g = g} {h = h} {i = i} iso₁ iso₂ = record
     id              ∎
   }
   where module iso₁ = Iso iso₁; module iso₂ = Iso iso₂
+
+Iso-invˡ : g RetractOf f → Iso (f ∘ h) (i ∘ g) → Iso h i
+Iso-invˡ {g = g} {f = f} {h = h} {i = i} g∘f≈id iso = record
+  { isoˡ = begin
+    i ∘ h             ≈⟨ intro-center g∘f≈id ⟩
+    i ∘ (g ∘ f) ∘ h   ≈⟨ refl⟩∘⟨ assoc ⟩
+    i ∘ g ∘ f ∘ h     ≈⟨ sym-assoc ⟩
+    (i ∘ g) ∘ (f ∘ h) ≈⟨ isoˡ ⟩
+    id                ∎
+  ; isoʳ = begin
+    h ∘ i                     ≈⟨ intro-last g∘f≈id ⟩
+    h ∘ (i ∘ g) ∘ f           ≈⟨ intro-first g∘f≈id ⟩
+    g ∘ (f ∘ h) ∘ (i ∘ g) ∘ f ≈⟨ sym-assoc ⟩
+    (g ∘ f ∘ h) ∘ (i ∘ g) ∘ f ≈⟨ cancelInner isoʳ ⟩
+    g ∘ f                     ≈⟨ g∘f≈id ⟩
+    id                        ∎
+  }
+  where open Iso iso
+
+Iso-invʳ : i SectionOf h → Iso (f ∘ h) (i ∘ g) → Iso f g
+Iso-invʳ h∘i≈id iso = Iso-swap $ Iso-invˡ h∘i≈id $ Iso-swap iso
+  where open Cheat!