Proofs for inducing monoids from categories

CatToMon.agda

module CatToMon where

open import Data.Product
open import Data.Sum
open import Data.Unit
open import Data.Empty
open import Level
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable
open import Relation.Binary
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality.Core
open import Relation.Nullary using (¬_; Dec; yes; no)


record Monoid : Set₁ where
  field Carrier : Set
        unit : Carrier
        _⊕_ : Carrier -> Carrier -> Carrier
        assoc : {x y z : Carrier} -> (x ⊕ (y ⊕ z)) ≡ ((x ⊕ y) ⊕ z)
        unit-left : {x : Carrier} -> (unit ⊕ x) ≡ x
        unit-right : {x : Carrier} -> (x ⊕ unit) ≡ x

open Monoid

record Category {l : Level} : Set (Level.suc l) where
  field obj : Set l
        arr : (src : obj) -> (trg : obj) -> Set l

        -- Decideable equality on objects
        eq : Decidable {A = obj} _≡_ 
        -- composition in the left-to-right form
        _$_ : {a b c : obj} (f : arr a b) -> (g : arr b c) -> arr a c
        id  : (a : obj) -> arr a a

        -- Properties of composition/identity
        comp-assoc : {a b c d : obj} (f : arr a b) (g : arr b c) (h : arr c d) -> (f $ (g $ h)) ≡ ((f $ g) $ h)
        id-right : {a b : obj} {f : arr a b} -> (f $ (id b)) ≡ f
        id-left : {a b : obj} {f : arr a b} -> ((id a) $ f) ≡ f 

open Category

data Completion (C : Category) : Set where
  Bottom : Completion C
  Top    : Completion C
  Morph  : (x : obj C) -> (y : obj C) -> (arr C x y) -> Completion C


plus : {C : Category} -> Completion C -> Completion C -> Completion C
plus Bottom x = Bottom
plus x Bottom = Bottom
plus Top x    = x
plus x   Top  = x
plus {c} (Morph u v f) (Morph w x g) with (eq c v w)
plus {c} (Morph u v f) (Morph .v x g) | yes refl = Morph u x (_$_ c f g)
plus {c} (Morph u v _) (Morph w x _)  | no ¬refl = Bottom


decEqReflex : {A : Set} {_≟_ : Decidable {A = A} _≡_} -> {x : A} -> (x ≟ x) ≡ yes refl
decEqReflex {s} {_≟_} {x = x} with x ≟ x
decEqReflex | yes refl = refl
decEqReflex | no q = ⊥-elim (q refl)


nonMorphd : {c : Category} {u v w x : obj c} {f : arr c u v} {g : arr c w x}
          -> (¬ (v ≡ w))
          -> plus {c} (Morph u v f) (Morph w x g) ≡ Bottom
nonMorphd {c} {u} {v} {w} {x} notEq with eq c v w 
nonMorphd notEq | yes p      = ⊥-elim (notEq p)
nonMorphd notEq | no ¬notEq  = refl



unitR : {c : Category} {x : Completion c} -> plus {c} x Top ≡ x
unitR {x = Bottom}      = refl
unitR {x = Top}         = refl
unitR {x = Morph _ _ _} = refl

unitL : {c : Category} {x : Completion c} -> plus {c} Top x ≡ x
unitL {x = Bottom}      = refl
unitL {x = Top}         = refl
unitL {x = Morph _ _ _} = refl

absorbR : {c : Category} {x : Completion c} -> plus {c} x Bottom ≡ Bottom
absorbR {x = Bottom}      = refl
absorbR {x = Top}         = refl
absorbR {x = Morph _ _ _} = refl

absorbL : {c : Category} {x : Completion c} -> plus {c} Bottom x ≡ Bottom
absorbL {x = Bottom}      = refl
absorbL {x = Top}         = refl
absorbL {x = Morph _ _ _} = refl


associativity : {c : Category} {x y z : Completion c}
            -> plus {c} x (plus {c} y z) ≡ plus {c} (plus {c} x y) z
            
associativity {c} {x = Top} {y} {z}
  rewrite (unitL {c} {x = plus {c} y z})
        | (unitL {c} {x = y})
    = refl
associativity {c} {x} {Top} {z}
  rewrite unitL {c} {x = z}
        | unitR {c} {x = x}
    = refl
associativity {c} {x} {y} {Top}
  rewrite unitR {c} {x = y}
        | unitR {c} {x = plus {c} x y}
    = refl
associativity {x = Bottom} {y} {z} = refl
associativity {c} {x = x} {Bottom} {z}
  rewrite absorbL {c} {x = z}
        | absorbR {c} {x = x}
    = refl
associativity {c} {x = x} {y} {Bottom}
  rewrite absorbR {c} {x = y}
        | absorbR {c} {x = x}
        | absorbR {c} {x = plus {c} x y}
    = refl
    
associativity {c} {x = Morph u v f} {Morph w x g} {Morph y z h}
  with eq c v w | eq c x y
associativity {c} {Morph u v f} {Morph .v x g} {Morph .x z h} | yes refl | yes refl
  rewrite decEqReflex {obj c} {eq c} {v}
        | decEqReflex {obj c} {eq c} {x}
        | comp-assoc c {u} {v} {x} {z} f g h
  = refl

associativity {c} {Morph u v f} {Morph .v x g} {Morph y z h} | yes refl | no q
  rewrite nonMorphd {c} {u} {x} {y} {z} {_$_ c f g} {h} q
  = refl
  
associativity {c} {Morph u v f} {Morph w x g} {Morph .x z h} | no q | yes refl
  rewrite nonMorphd {c} {u} {v} {w} {z} {f} {_$_ c g h} q
  = refl
  
associativity {c} {Morph u v f} {Morph w x g} {Morph y z h} | no q1 | no q2 = refl


cToM : Category -> Monoid
cToM p = record
              { Carrier    = Completion p
              ; unit       = Top
              ; _⊕_        = plus
              ; assoc      = λ {x} {y} {z} → associativity {p} {x} {y} {z}
              ; unit-left  = unitL
              ; unit-right = unitR
              }


record MonoFunctor {l : Level} (c d : Category {l}) : Set (suc l) where
  field F : obj c -> obj d
        Ff : {a b : obj c} -> (arr c a b) -> arr d (F a) (F b)
        Feq : {a b : obj c} -> a ≡ b -> (F a) ≡ (F b)
        Feqi : {a b : obj c} -> (F a) ≡ (F b) -> a ≡ b 

        compAssoc : {x y z : obj c} -> (f : arr c x y) -> (g : arr c y z) ->
                    Ff (_$_ c f g) ≡ _$_ d (Ff f) (Ff g)
        compUnit : {a : obj c} ->
                   Ff (id c a) ≡ id d (F a)

open MonoFunctor


record MonoidMorphism (m n : Monoid) : Set₁ where
  field G : Carrier m -> Carrier n
        Gp : {a b : Carrier m} -> G (_⊕_ m a b) ≡ _⊕_ n (G a) (G b)
        Gu : G (unit m) ≡ unit n

open MonoidMorphism

objMap : {c d : Category} -> (MonoFunctor c d) -> (Carrier (cToM c) -> Carrier (cToM d))
objMap func Bottom = Bottom
objMap func Top = Top
objMap func (Morph x y f) = Morph (F func x) (F func y) (Ff func f)


monoidHomoAssoc : {c d : Category} -> (func : MonoFunctor c d)
                  {a b : Carrier (cToM c)}
               -> (objMap func) (_⊕_ (cToM c) a b) ≡ _⊕_ (cToM d) (objMap func a) (objMap func b)
monoidHomoAssoc func {Bottom} {Bottom} = refl
monoidHomoAssoc func {Bottom} {Top} = refl
monoidHomoAssoc func {Bottom} {Morph x y x₁} = refl
monoidHomoAssoc func {Top} {Bottom} = refl
monoidHomoAssoc func {Top} {Top} = refl
monoidHomoAssoc func {Top} {Morph x y x₁} = refl
monoidHomoAssoc func {Morph x y x₁} {Bottom} = refl
monoidHomoAssoc func {Morph x y x₁} {Top} = refl
monoidHomoAssoc {c} {d} func {Morph x y f} {Morph w z g}
   with eq c y w 
monoidHomoAssoc {c} {d} func {Morph x y f} {Morph .y z g} | yes refl 
     rewrite compAssoc func {x} {y} {z} f g | decEqReflex {obj d} {eq d} {F func y} = refl

-- This case requires that inequality is preserved, but this condition does not
-- come from the pre-order morphism
monoidHomoAssoc {c} {d} func {Morph x y f} {Morph w z g} | no np
     rewrite nonMorphd {d} {F func x} {F func y} {F func w} {F func z}
                        {Ff func f} {Ff func g} (λ p → np (Feqi func p)) = refl


monoFToMmorph : {c d : Category} -> MonoFunctor c d -> MonoidMorphism (cToM c) (cToM d)
monoFToMmorph {p} {q} preM =
  record {
    G = objMap preM
  ; Gp = λ {a} {b} -> monoidHomoAssoc {p} {q} preM {a} {b}
  ; Gu = refl
  }