Refresher.agda

module Refresher where

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + n = n
succ n + m = succ (n + m)

data _≡_ {A : Set} : A → A → Set where
  refl : ∀ {x} → x ≡ x

eq-sym : {A : Set}{x y : A} → x ≡ y → y ≡ x
eq-sym refl = refl

eq-trans : {A : Set}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
eq-trans refl refl = refl

cong : {A B : Set}{x y : A} → (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

assoc : (x y z : ℕ) → (x + (y + z)) ≡ ((x + y) + z)
assoc zero y z = refl
assoc (succ x) y z = cong succ (assoc x y z)

add-zero : (x : ℕ) → (x + zero) ≡ x
add-zero zero = refl
add-zero (succ x) = cong succ (add-zero x)

record Monoid : Set₁ where
  field
    C : Set
    comp : C → C → C
    comp-assoc : (x y z : C) → comp x (comp y z) ≡ comp (comp x y) z
    id : C
    id-left : (x : C) → comp x id ≡ x
    id-right : (x : C) → comp id x ≡ x
open Monoid

nat-monoid : Monoid
nat-monoid = record
  { C = ℕ ;
    comp = _+_ ;
    comp-assoc = assoc ;
    id = zero ;
    id-left = add-zero ;
    id-right = λ x → refl }

record MonoidMorphism (M₁ M₂ : Monoid) : Set where
  field
    fun : C M₁ → C M₂
    fun-comp : (x y : C M₁) → fun (comp M₁ x y) ≡ comp M₂ (fun x) (fun y)
open MonoidMorphism

data List (A : Set) : Set where
  [] : List A
  _∷_ : A → List A → List A

_++_ : {A : Set} → List A → List A → List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

append-assoc : {A : Set}(xs ys zs : List A) → (xs ++ (ys ++ zs)) ≡ ((xs ++ ys) ++ zs)
append-assoc [] ys zs = refl
append-assoc (x ∷ xs) ys zs = cong (_∷_ x) (append-assoc xs ys zs)

append-zero : {A : Set}(xs : List A) → (xs ++ []) ≡ xs
append-zero [] = refl
append-zero (x ∷ xs) = cong (_∷_ x) (append-zero xs)

list-monoid : Set → Monoid
list-monoid X = record
  { C = List X ;
    comp = _++_ ;
    comp-assoc = append-assoc ;
    id = [] ;
    id-left = append-zero ;
    id-right = λ x → refl }

length : {A : Set} → List A → ℕ
length [] = zero
length (x ∷ xs) = succ (length xs)

append-length : {A : Set}(xs ys : List A) → length (xs ++ ys) ≡ (length xs + length ys)
append-length [] ys = refl
append-length (x ∷ xs) ys = cong succ (append-length xs ys)

length-morphism : (A : Set) → MonoidMorphism (list-monoid A) nat-monoid
length-morphism A = record
  { fun = length ;
    fun-comp = append-length }

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj1 : A
    proj2 : B proj1

_∧_ : Set → Set → Set
A ∧ B = Σ A (λ x → B)
    
single-id : (m : Monoid)(x : C m) → ((y : C m) → (comp m x y ≡ y) ∧ (comp m y x ≡ y)) → x ≡ id m
single-id m e e-id with e-id (id m)
... | p1 , p2 = eq-trans (eq-sym (id-right m e)) p2

surj : {A B : Set}(f : A → B) → Set
surj {A} {B} f = (y : B) → Σ A (λ x → f x ≡ y)

m-id-l1 : (m1 m2 : Monoid)(f : MonoidMorphism m1 m2) → surj (fun f) → (y : C m2) → comp m2 (fun f (id m1)) y ≡ y
m-id-l1 m1 m2 f sur y with sur y
m-id-l1 m1 m2 f sur .(fun f x) | x , refl with fun-comp f (id m1) x
... | prf1 = eq-trans (eq-sym prf1) (cong (fun f) (id-right m1 x))

m-id-l2 : (m1 m2 : Monoid)(f : MonoidMorphism m1 m2) → surj (fun f) → (y : C m2) → comp m2 y (fun f (id m1)) ≡ y
m-id-l2 m1 m2 f sur y with sur y
m-id-l2 m1 m2 f sur .(fun f x) | x , refl with fun-comp f x (id m1)
... | prf1 = eq-trans (eq-sym prf1) (cong (fun f) (id-left m1 x))

morphism-id : (m₁ m₂ : Monoid)(f : MonoidMorphism m₁ m₂) → surj (fun f) → fun f (id m₁) ≡ id m₂
morphism-id m1 m2 f sur = single-id m2 (fun f (id m1)) (λ y → m-id-l1 m1 m2 f sur y , m-id-l2 m1 m2 f sur y)