{-# OPTIONS --without-K --safe #-}

open import Categories.Category

module Categories.Morphism.IsoEquiv {o β„“ e} (π’ž : Category o β„“ e) where

open import Level
open import Function using (flip; _on_)
open import Relation.Binary hiding (_β‡’_)
import Relation.Binary.Construct.On as On

open import Categories.Morphism π’ž

open Category π’ž

private
  variable
    A B C : Obj

-- Two lemmas to set things up: if they exist, inverses are unique.

to-unique : βˆ€ {f₁ fβ‚‚ : A β‡’ B} {g₁ gβ‚‚} β†’
            Iso f₁ g₁ β†’ Iso fβ‚‚ gβ‚‚ β†’ f₁ β‰ˆ fβ‚‚ β†’ g₁ β‰ˆ gβ‚‚
to-unique {_} {_} {f₁} {fβ‚‚} {g₁} {gβ‚‚} iso₁ isoβ‚‚ hyp = begin
                 g₁   β‰ˆΛ˜βŸ¨ identityΛ‘ ⟩
     id        ∘ g₁   β‰ˆΛ˜βŸ¨ ∘-resp-β‰ˆΛ‘ Isoβ‚‚.isoΛ‘ ⟩
    (gβ‚‚ ∘  fβ‚‚) ∘ g₁   β‰ˆΛ˜βŸ¨ ∘-resp-β‰ˆΛ‘ (∘-resp-β‰ˆΚ³ hyp) ⟩
    (gβ‚‚ ∘  f₁) ∘ g₁   β‰ˆβŸ¨ assoc ⟩
     gβ‚‚ ∘ (f₁  ∘ g₁)  β‰ˆβŸ¨ ∘-resp-β‰ˆΚ³ Iso₁.isoΚ³ ⟩
     gβ‚‚ ∘  id         β‰ˆβŸ¨ identityΚ³ ⟩
     gβ‚‚               ∎
  where
    open HomReasoning
    module Iso₁ = Iso iso₁
    module Isoβ‚‚ = Iso isoβ‚‚

from-unique : βˆ€ {f₁ fβ‚‚ : A β‡’ B} {g₁ gβ‚‚} β†’
              Iso f₁ g₁ β†’ Iso fβ‚‚ gβ‚‚ β†’ g₁ β‰ˆ gβ‚‚ β†’ f₁ β‰ˆ fβ‚‚
from-unique iso₁ isoβ‚‚ hyp = to-unique iso₁⁻¹ iso₂⁻¹ hyp
  where
    iso₁⁻¹ = record { isoΛ‘ = Iso.isoΚ³ iso₁  ; isoΚ³ = Iso.isoΛ‘ iso₁ }
    iso₂⁻¹ = record { isoΛ‘ = Iso.isoΚ³ isoβ‚‚  ; isoΚ³ = Iso.isoΛ‘ isoβ‚‚ }

-- Equality of isomorphisms is just equality of the underlying morphism(s).
--
-- Only one equation needs to be given; the equation in the other
-- direction holds automatically (by the above lemmas).
--
-- The reason for wrapping the underlying equality in a record at all
-- is that this helps unification.  Concretely, it allows Agda to
-- infer the isos |i| and |j| being related in function applications
-- where only the equation |i ≃ j| is passed as an explicit argument.

infix 4 _≃_
record _≃_ (i j : A β‰… B) : Set e where
  constructor ⌞_⌟
  open _β‰…_
  field from-β‰ˆ : from i β‰ˆ from j

  to-β‰ˆ : to i β‰ˆ to j
  to-β‰ˆ = to-unique (iso i) (iso j) from-β‰ˆ

open _≃_

module _ {A B : Obj} where
  open Equiv

  ≃-refl : Reflexive (_≃_ {A} {B})
  ≃-refl = ⌞ refl ⌟

  ≃-sym : Symmetric (_≃_ {A} {B})
  ≃-sym = Ξ» where ⌞ eq ⌟          β†’ ⌞ sym eq ⌟

  ≃-trans : Transitive (_≃_ {A} {B})
  ≃-trans = Ξ» where ⌞ eq₁ ⌟ ⌞ eqβ‚‚ ⌟ β†’ ⌞ trans eq₁ eqβ‚‚ ⌟

  ≃-isEquivalence : IsEquivalence (_≃_ {A} {B})
  ≃-isEquivalence = record
    { refl  = ≃-refl
    ; sym   = ≃-sym
    ; trans = ≃-trans
    }

≃-setoid : βˆ€ {A B : Obj} β†’ Setoid _ _
≃-setoid {A} {B} = record
  { Carrier       = A β‰… B
  ; _β‰ˆ_           = _≃_
  ; isEquivalence = ≃-isEquivalence
  }

----------------------------------------------------------------------

-- An alternative, more direct notion of equality on isomorphisms that
-- involves no wrapping/unwrapping.

infix 4 _≃′_
_≃′_ : Rel (A β‰… B) e
_≃′_ = _β‰ˆ_ on _β‰…_.from

≃′-isEquivalence : IsEquivalence (_≃′_ {A} {B})
≃′-isEquivalence = On.isEquivalence _β‰…_.from equiv

≃′-setoid : βˆ€ {A B : Obj} β†’ Setoid _ _
≃′-setoid {A} {B} = record
  { Carrier       = A β‰… B
  ; _β‰ˆ_           = _≃′_
  ; isEquivalence = ≃′-isEquivalence
  }

-- The two notions of equality are equivalent

≃⇒≃′ : βˆ€ {i j : A β‰… B} β†’ i ≃ j β†’ i ≃′ j
≃⇒≃′ eq = from-β‰ˆ eq

≃′⇒≃ : βˆ€ {i j : A β‰… B} β†’ i ≃′ j β†’ i ≃ j
≃′⇒≃ {_} {_} {i} {j} eq = ⌞ eq ⌟