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

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.Reasoning 𝒞

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₂