{-# OPTIONS --without-K --safe #-}
open import Categories.Category

module CatTheory.Morphism.Properties {o ℓ e} (𝒞 : Category o ℓ e) where

open Category 𝒞
open HomReasoning

open import Categories.Morphism 𝒞
open import Categories.Morphism.Reasoning 𝒞
open import Function using (_$_)

import Categories.Morphism.Properties as Mₚ
module Cheat! = Mₚ 𝒞

private
  variable
    A B C D : Obj
    f g h i : A ⇒ B

Iso-∘ : Iso f g → Iso h i → Iso (f ∘ h) (i ∘ g)
Iso-∘ {f = f} {g = g} {h = h} {i = i} iso₁ iso₂ = record
  { isoˡ = begin
    (i ∘ g) ∘ f ∘ h ≈⟨ cancelInner iso₁.isoˡ ⟩
    i ∘ h           ≈⟨ iso₂.isoˡ ⟩
    id              ∎
  ; isoʳ = begin
    (f ∘ h) ∘ i ∘ g ≈⟨ cancelInner iso₂.isoʳ ⟩
    f ∘ g           ≈⟨ iso₁.isoʳ ⟩
    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!

Iso⇒Retract : Iso f g → g RetractOf f
Iso⇒Retract iso = isoˡ
  where open Iso iso

Retract⇒Mono : g RetractOf f → Mono f
Retract⇒Mono {g = g} {f = f} g∘f≈id h₁ h₂ f∘h₁≈f∘h₂ = begin
  h₁           ≈˘⟨ cancelˡ g∘f≈id ⟩
  g ∘ (f ∘ h₁) ≈⟨  refl⟩∘⟨ f∘h₁≈f∘h₂ ⟩
  g ∘ (f ∘ h₂) ≈⟨  cancelˡ g∘f≈id ⟩
  h₂           ∎

Mono∘ : Mono f → Mono g → Mono (f ∘ g)
Mono∘ {f = f} {g = g} f-mono g-mono h₁ h₂ f∘g∘h₁≈f∘g∘h₂ =
  g-mono h₁ h₂ $ f-mono (g ∘ h₁) (g ∘ h₂) $ sym-assoc ○ f∘g∘h₁≈f∘g∘h₂ ○ assoc