open import 1Lab.Prelude hiding (_∘_ ; id ; _β†ͺ_)

open import Cat.Solver
open import Cat.Base

module Cat.Morphism {o h} (C : Precategory o h) where

MorphismsπŸ”—

This module defines the three most important classes of morphisms that can be found in a category: monomorphisms, epimorphisms, and isomorphisms.

MonosπŸ”—

A morphism is said to be monic when it is left-cancellable. A monomorphism from AA to BB, written Aβ†ͺBA \mono B, is a monic morphism.

is-monic : Hom a b β†’ Type _
is-monic {a = a} f = βˆ€ {c} β†’ (g h : Hom c a) β†’ f ∘ g ≑ f ∘ h β†’ g ≑ h

is-monic-is-prop : βˆ€ {a b} (f : Hom a b) β†’ is-prop (is-monic f)
is-monic-is-prop f x y i {c} g h p = Hom-set _ _ _ _ (x g h p) (y g h p) i

record _β†ͺ_ (a b : Ob) : Type (o βŠ” h) where
  field
    mor   : Hom a b
    monic : is-monic mor

open _β†ͺ_ public

Conversely, a morphism is said to be epic when it is right-cancellable. An epimorphism from AA to BB, written A↠BA \epi B, is an epic morphism.

EpisπŸ”—

is-epic : Hom a b β†’ Type _
is-epic {b = b} f = βˆ€ {c} β†’ (g h : Hom b c) β†’ g ∘ f ≑ h ∘ f β†’ g ≑ h

is-epic-is-prop : βˆ€ {a b} (f : Hom a b) β†’ is-prop (is-epic f)
is-epic-is-prop f x y i {c} g h p = Hom-set _ _ _ _ (x g h p) (y g h p) i

record _β† _ (a b : Ob) : Type (o βŠ” h) where
  field
    mor  : Hom a b
    epic : is-epic mor

open _β† _ public

IsosπŸ”—

Maps f:Aβ†’Bf : A \to B and g:Bβ†’Ag : B \to A are inverses when we have f∘gf \circ g and g∘fg \circ f both equal to the identity. A map f:Aβ†’Bf : A \to B is invertible (or is an isomorphism) when there exists a gg for which ff and gg are inverses. An isomorphism Aβ‰…BA \cong B is a choice of map Aβ†’BA \to B, together with a specified inverse.

record Inverses (f : Hom a b) (g : Hom b a) : Type h where
  field
    invl : f ∘ g ≑ id
    invr : g ∘ f ≑ id

open Inverses

record is-invertible (f : Hom a b) : Type h where
  field
    inv : Hom b a
    inverses : Inverses f inv

  open Inverses inverses public

  op : is-invertible inv
  op .inv = f
  op .inverses .Inverses.invl = invr inverses
  op .inverses .Inverses.invr = invl inverses

record _β‰…_ (a b : Ob) : Type h where
  field
    to       : Hom a b
    from     : Hom b a
    inverses : Inverses to from

  open Inverses inverses public

open _β‰…_ public

A given map is invertible in at most one way: If you have f:A→Bf : A \to B with two inverses g:B→Ag : B \to A and h:B→Ah : B \to A, then not only are g=hg = h equal, but the witnesses of these equalities are irrelevant.

Inverses-are-prop : βˆ€ {f : Hom a b} {g : Hom b a} β†’ is-prop (Inverses f g)
Inverses-are-prop x y i .Inverses.invl = Hom-set _ _ _ _ (x .invl) (y .invl) i
Inverses-are-prop x y i .Inverses.invr = Hom-set _ _ _ _ (x .invr) (y .invr) i

is-invertible-is-prop : βˆ€ {f : Hom a b} β†’ is-prop (is-invertible f)
is-invertible-is-prop {a = a} {b = b} {f = f} g h = p where
  module g = is-invertible g
  module h = is-invertible h

  g≑h : g.inv ≑ h.inv
  g≑h =
    g.inv             β‰‘βŸ¨ sym (idr _) βˆ™ apβ‚‚ _∘_ refl (sym h.invl) βŸ©β‰‘
    g.inv ∘ f ∘ h.inv β‰‘βŸ¨ assoc _ _ _ Β·Β· apβ‚‚ _∘_ g.invr refl Β·Β· idl _ βŸ©β‰‘
    h.inv             ∎

  p : g ≑ h
  p i .is-invertible.inv = g≑h i
  p i .is-invertible.inverses =
    is-propβ†’pathp (Ξ» i β†’ Inverses-are-prop {g = g≑h i}) g.inverses h.inverses i

We note that the identity morphism is always iso, and that isos compose:

id-iso : a β‰… a
id-iso .to = id
id-iso .from = id
id-iso .inverses .invl = idl id
id-iso .inverses .invr = idl id

Isomorphism = _β‰…_

Inverses-∘ : {f : Hom a b} {f⁻¹ : Hom b a} {g : Hom b c} {g⁻¹ : Hom c b}
           β†’ Inverses f f⁻¹ β†’ Inverses g g⁻¹ β†’ Inverses (g ∘ f) (f⁻¹ ∘ g⁻¹)
Inverses-∘ {f = f} {f⁻¹} {g} {g⁻¹} finv ginv = record { invl = l ; invr = r } where
  module finv = Inverses finv
  module ginv = Inverses ginv

  abstract
    l : (g ∘ f) ∘ f⁻¹ ∘ g⁻¹ ≑ id
    l = (g ∘ f) ∘ f⁻¹ ∘ g⁻¹ β‰‘βŸ¨ cat! C βŸ©β‰‘
        g ∘ (f ∘ f⁻¹) ∘ g⁻¹ β‰‘βŸ¨ (Ξ» i β†’ g ∘ finv.invl i ∘ g⁻¹) βŸ©β‰‘
        g ∘ id ∘ g⁻¹        β‰‘βŸ¨ cat! C βŸ©β‰‘
        g ∘ g⁻¹             β‰‘βŸ¨ ginv.invl βŸ©β‰‘
        id                  ∎

    r : (f⁻¹ ∘ g⁻¹) ∘ g ∘ f ≑ id
    r = (f⁻¹ ∘ g⁻¹) ∘ g ∘ f β‰‘βŸ¨ cat! C βŸ©β‰‘
        f⁻¹ ∘ (g⁻¹ ∘ g) ∘ f β‰‘βŸ¨ (Ξ» i β†’ f⁻¹ ∘ ginv.invr i ∘ f) βŸ©β‰‘
        f⁻¹ ∘ id ∘ f        β‰‘βŸ¨ cat! C βŸ©β‰‘
        f⁻¹ ∘ f             β‰‘βŸ¨ finv.invr βŸ©β‰‘
        id                  ∎

_∘Iso_ : a β‰… b β†’ b β‰… c β†’ a β‰… c
(f ∘Iso g) .to = g .to ∘ f .to
(f ∘Iso g) .from = f .from ∘ g .from
(f ∘Iso g) .inverses = Inverses-∘ (f .inverses) (g .inverses)

_Iso⁻¹ : a β‰… b β†’ b β‰… a
(f Iso⁻¹) .to = f .from
(f Iso⁻¹) .from = f .to
(f Iso⁻¹) .inverses .invl = f .inverses .invr
(f Iso⁻¹) .inverses .invr = f .inverses .invl

We also note that invertible morphisms are both epic and monic.

invertible→monic : is-invertible f → is-monic f
invertible→monic {f = f} invert g h p =
  g             β‰‘Λ˜βŸ¨ idl g βŸ©β‰‘Λ˜
  id ∘ g        β‰‘Λ˜βŸ¨ ap (_∘ g) (is-invertible.invr invert) βŸ©β‰‘Λ˜
  (inv ∘ f) ∘ g β‰‘Λ˜βŸ¨ assoc inv f g βŸ©β‰‘Λ˜
  inv ∘ (f ∘ g) β‰‘βŸ¨ ap (inv ∘_) p βŸ©β‰‘
  inv ∘ (f ∘ h) β‰‘βŸ¨ assoc inv f h βŸ©β‰‘
  (inv ∘ f) ∘ h β‰‘βŸ¨ ap (_∘ h) (is-invertible.invr invert) βŸ©β‰‘
  id ∘ h        β‰‘βŸ¨ idl h βŸ©β‰‘
  h ∎
  where
    open is-invertible invert

invertible→epic : is-invertible f → is-epic f
invertible→epic {f = f} invert g h p =
  g             β‰‘Λ˜βŸ¨ idr g βŸ©β‰‘Λ˜
  g ∘ id        β‰‘Λ˜βŸ¨ ap (g ∘_) (is-invertible.invl invert) βŸ©β‰‘Λ˜
  g ∘ (f ∘ inv) β‰‘βŸ¨ assoc g f inv βŸ©β‰‘
  (g ∘ f) ∘ inv β‰‘βŸ¨ ap (_∘ inv) p βŸ©β‰‘
  (h ∘ f) ∘ inv β‰‘Λ˜βŸ¨ assoc h f inv βŸ©β‰‘Λ˜
  h ∘ (f ∘ inv) β‰‘βŸ¨ ap (h  ∘_) (is-invertible.invl invert) βŸ©β‰‘
  h ∘ id        β‰‘βŸ¨ idr h βŸ©β‰‘
  h ∎
  where
    open is-invertible invert