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

{-
  Properties and definitions regarding Morphisms of a category:
  - Monomorphism
  - Epimorphism
  - Isomorphism
  - (object) equivalence ('spelled' _β‰…_ ). Exported as the module β‰…
-}
open import Categories.Category.Core

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

open import Level
open import Relation.Binary hiding (_β‡’_)

open import Categories.Morphism.Reasoning.Core π’ž

open Category π’ž

private
  variable
    A B C : Obj

Mono : βˆ€ (f : A β‡’ B) β†’ Set (o βŠ” β„“ βŠ” e)
Mono {A = A} f = βˆ€ {C} β†’ (g₁ gβ‚‚ : C β‡’ A) β†’ f ∘ g₁ β‰ˆ f ∘ gβ‚‚ β†’ g₁ β‰ˆ gβ‚‚

JointMono : {ΞΉ : Level} (I : Set ΞΉ) (B : I β†’ Obj) β†’ ((i : I) β†’ A β‡’ B i) β†’ Set (o βŠ” β„“ βŠ” e βŠ” ΞΉ)
JointMono {A} I B f = βˆ€ {C} β†’ (g₁ gβ‚‚ : C β‡’ A) β†’ ((i : I) β†’ f i ∘ g₁ β‰ˆ f i ∘ gβ‚‚) β†’ g₁ β‰ˆ gβ‚‚

record _↣_ (A B : Obj) : Set (o βŠ” β„“ βŠ” e) where
  field
    mor  : A β‡’ B
    mono : Mono mor

Epi : βˆ€ (f : A β‡’ B) β†’ Set (o βŠ” β„“ βŠ” e)
Epi {B = B} f = βˆ€ {C} β†’ (g₁ gβ‚‚ : B β‡’ C) β†’ g₁ ∘ f β‰ˆ gβ‚‚ ∘ f β†’ g₁ β‰ˆ gβ‚‚

JointEpi : (I : Set) (A : I β†’ Obj) β†’ ((i : I) β†’ A i β‡’ B) β†’ Set (o βŠ” β„“ βŠ” e)
JointEpi {B} I A f = βˆ€ {C} β†’ (g₁ gβ‚‚ : B β‡’ C) β†’ ((i : I) β†’ g₁ ∘ f i β‰ˆ gβ‚‚ ∘ f i) β†’ g₁ β‰ˆ gβ‚‚

record _β† _ (A B : Obj) : Set (o βŠ” β„“ βŠ” e) where
  field
    mor : A β‡’ B
    epi : Epi mor

_SectionOf_ : (g : B β‡’ A) (f : A β‡’ B) β†’ Set e
g SectionOf f = f ∘ g β‰ˆ id

_RetractOf_ : (g : B β‡’ A) (f : A β‡’ B) β†’ Set e
g RetractOf f = g ∘ f β‰ˆ id

record Retract (X U : Obj) : Set (β„“ βŠ” e) where
  field
    section : X β‡’ U
    retract : U β‡’ X
    is-retract : retract ∘ section β‰ˆ id

record Iso (from : A β‡’ B) (to : B β‡’ A) : Set e where
  field
    isoΛ‘ : to ∘ from β‰ˆ id
    isoΚ³ : from ∘ to β‰ˆ id

-- We often say that a morphism "is an iso" if there exists some inverse to it.
-- This does buck the naming convention we use somewhat, but it lines up
-- better with the literature.
record IsIso (from : A β‡’ B) : Set (β„“ βŠ” e) where
  field
    inv : B β‡’ A
    iso : Iso from inv 

  open Iso iso public

infix 4 _β‰…_
record _β‰…_ (A B : Obj) : Set (β„“ βŠ” e) where
  field
    from : A β‡’ B
    to   : B β‡’ A
    iso  : Iso from to

  open Iso iso public

-- don't pollute the name space too much
private
  β‰…-refl : Reflexive _β‰…_
  β‰…-refl = record
    { from = id
    ; to   = id
    ; iso  = record
      { isoΛ‘ = identityΒ²
      ; isoΚ³ = identityΒ²
      }
    }

  β‰…-sym : Symmetric _β‰…_
  ≅-sym A≅B = record
    { from = to
    ; to   = from
    ; iso  = record
      { isoΛ‘ = isoΚ³
      ; isoΚ³ = isoΛ‘
      }
    }
    where open _≅_ A≅B

  β‰…-trans : Transitive _β‰…_
  ≅-trans A≅B B≅C = record
    { from = from Bβ‰…C ∘ from Aβ‰…B
    ; to   = to Aβ‰…B ∘ to Bβ‰…C
    ; iso  = record
      { isoΛ‘ = begin
        (to Aβ‰…B ∘ to Bβ‰…C) ∘ from Bβ‰…C ∘ from Aβ‰…B β‰ˆβŸ¨ cancelInner (isoΛ‘ Bβ‰…C) ⟩
        to Aβ‰…B ∘ from Aβ‰…B                       β‰ˆβŸ¨  isoΛ‘ Aβ‰…B  ⟩
        id                                      ∎
      ; isoΚ³ = begin
        (from Bβ‰…C ∘ from Aβ‰…B) ∘ to Aβ‰…B ∘ to Bβ‰…C β‰ˆβŸ¨ cancelInner (isoΚ³ Aβ‰…B) ⟩
        from Bβ‰…C ∘ to Bβ‰…C                       β‰ˆβŸ¨ isoΚ³ Bβ‰…C ⟩
        id                                      ∎
      }
    }
    where open _β‰…_
          open HomReasoning
          open Equiv

β‰…-isEquivalence : IsEquivalence _β‰…_
β‰…-isEquivalence = record
  { refl  = β‰…-refl
  ; sym   = β‰…-sym
  ; trans = β‰…-trans
  }

-- But make accessing it easy:
module β‰… = IsEquivalence β‰…-isEquivalence

β‰…-setoid : Setoid _ _
β‰…-setoid = record
  { Carrier       = Obj
  ; _β‰ˆ_           = _β‰…_
  ; isEquivalence = β‰…-isEquivalence
  }