Added proof of iso from section and retraction

src/Categories/Morphism/Properties.agda

@@ -150,3 +150,59 @@ _∘↠_ : B ↠ C → A ↠ B → A ↠ C
 f ∘↠ g = record { mor = mor f ∘ mor g ; epi = Epi-∘ (epi f) (epi g) }
   where
     open _↠_
+
+--------------------------------------------------------------------------------
+-- Isomorphism from a section and a retraction
+
+EpicRetract⇒Iso : ∀ {X Y} {f : Y ⇒ X} {r : X ⇒ Y} → 
+                   r RetractOf f → Epi f → Iso f r
+EpicRetract⇒Iso {f = f} {r} rf≈id epi = record { 
+  isoˡ = rf≈id ; 
+  isoʳ = epi (f ∘ r) id (begin
+    (f ∘ r) ∘ f ≈⟨ pullʳ rf≈id ⟩
+    f ∘ id      ≈⟨ id-comm ⟩
+    id ∘ f ∎) }
+
+MonicSection⇒Iso : ∀ {X Y} {f : Y ⇒ X} {s : X ⇒ Y} → 
+                   s SectionOf f → Mono f → Iso f s
+MonicSection⇒Iso {f = f} {s} fs≈id mono = record { 
+  isoˡ = mono (s ∘ f) id (begin 
+    f ∘ (s ∘ f) ≈⟨ pullˡ fs≈id ⟩
+    id ∘ f      ≈⟨ id-comm-sym ⟩
+    f ∘ id ∎) ; 
+  isoʳ = fs≈id }
+
+≈-SectionRetraction : ∀ {X Y} {f : Y ⇒ X} {s r : X ⇒ Y} → 
+                      s SectionOf f → r RetractOf f → s ≈ r
+≈-SectionRetraction {f = f} {s} {r} fs≈id rf≈id = begin
+  s           ≈⟨ insertˡ rf≈id ⟩
+  r ∘ (f ∘ s) ≈⟨ elimʳ fs≈id ⟩
+  r ∎
+
+SectionRetraction⇒Isoˡ : ∀ {X Y} {f : Y ⇒ X} {s r : X ⇒ Y} → 
+                         s SectionOf f → r RetractOf f → Iso f s
+SectionRetraction⇒Isoˡ {f = f} {s} {r} fs≈id rf≈id = record { 
+  isoˡ = begin
+    s ∘ f ≈⟨ ≈-SectionRetraction fs≈id rf≈id ⟩∘⟨refl ⟩
+    r ∘ f ≈⟨ rf≈id ⟩
+    id ∎ ; 
+  isoʳ = fs≈id }
+
+SectionRetraction⇒Isoʳ : ∀ {X Y} {f : Y ⇒ X} {s r : X ⇒ Y} → 
+                         s SectionOf f → r RetractOf f → Iso f r
+SectionRetraction⇒Isoʳ {f = f} {s} {r} fs≈id rf≈id = record { 
+  isoˡ = rf≈id ; 
+  isoʳ = begin
+    f ∘ r ≈⟨ refl⟩∘⟨ ⟺ (≈-SectionRetraction fs≈id rf≈id) ⟩
+    f ∘ s ≈⟨ fs≈id ⟩
+    id ∎ }
+
+
+
+
+
+
+
+
+
+