{-# OPTIONS --without-K --safe #-}
 
open import Categories.Category
 
-- Reasoning facilities about morphism equivalences (not necessarily 'squares')
 
module Categories.Morphism.Reasoning {o ℓ e} (C : Category o ℓ e) where
 
-- some items are defined in sub-modules
open import Categories.Morphism.Reasoning.Core C public
open import Categories.Morphism.Reasoning.Iso C public
 
open Category C
open Definitions C
open HomReasoning
 
-- create a commutative square from an equivalence
toSquare : ∀ {A B} {f g : A ⇒ B} → f ≈ g → CommutativeSquare f id id g
toSquare {_} {_} {f} {g} f≈g = begin
      id ∘ f   ≈⟨ identityˡ ⟩
      f        ≈⟨ f≈g ⟩
      g        ≈˘⟨ identityʳ ⟩
      g ∘ id   ∎