open import Cat.Allegory.Base
open import Cat.Prelude

import Cat.Reasoning

module Cat.Allegory.Reasoning {o β β'} (A : Allegory o β β') where

open Allegory A public
open Cat.Reasoning (A .Allegory.cat)
hiding (module HLevel-instance ; Ob ; Hom ; Hom-set ; id ; idl ; idr ; assoc ; _β_ ; Mor ; HomβMor ; Mor-path)
public


# Combinators for allegoriesπ

For reasoning about morphisms in allegories, the first thing we need is a convenient syntax for piecing together long arguments by transitivity. The following operators allow us to interweave throwing in an inequality, and rewriting by an equality:

private variable
w x y z : Ob
a b c d f f' g g' h i : Hom x y

_β€β¨_β©_ : β (f : Hom x y) β f β€ g β g β€ h β f β€ h
_=β¨_β©_ : β (f : Hom x y) β f β‘ g β g β€ h β f β€ h
_=Λβ¨_β©_ : β (f : Hom x y) β g β‘ f β g β€ h β f β€ h
_β€β    : β (f : Hom x y) β f β€ f

f β€β¨ p β©β€ q = β€-trans p q
f =β¨ p β©= q = subst (_β€ _) (sym p) q
f =Λβ¨ p β©=Λ q = subst (_β€ _) p q
f β€β = β€-refl

infixr 40 _β_ _βΆ_
infixr 2 _=β¨_β©_ _=Λβ¨_β©_ _β€β¨_β©_
infix  3 _β€β


Additionally, we have whiskering operations, derived from the horizontal composition operation by holding one of the operands constant:

_βΆ_ : (f : Hom x y) β g β€ h β f β g β€ f β h
_β_ : f β€ g β (h : Hom x y) β f β h β€ g β h

f βΆ g = β€-refl β g
g β f = g β β€-refl


A few lemmas about the meet operation are also in order. It, unsurprisingly, behaves like the binary operation of a meet-semilattice: We have that $f \le g$ is equivalently $f = f \cap g$, and $f \cap g$ is a commutative, associative idempotent binary operation, which preserves ordering in both of its arguments.

β©-pres-r     : g β€ g' β f β© g β€ f β© g'
β©-pres-l     : f β€ f' β f β© g β€ f' β© g
β©-pres     : f β€ f' β g β€ g' β f β© g β€ f' β© g'
β©-distribl   : f β (g β© h) β€ (f β g) β© (f β h)
β©-distribr   : (g β© h) β f β€ (g β f) β© (h β f)
β©-distrib   : (f β© g) β (h β© i) β€ (f β h β© g β h) β© (f β i β© g β i)
β©-assoc      : (f β© g) β© h β‘ f β© (g β© h)
β©-comm       : f β© g β‘ g β© f
β©-idempotent : f β© f β‘ f

β©-pres-r w = β©-univ β©-le-l (β€-trans β©-le-r w)
β©-pres-l w = β©-univ (β€-trans β©-le-l w) β©-le-r
β©-pres w v = β©-univ (β€-trans β©-le-l w) (β€-trans β©-le-r v)
β©-distribl = β©-univ (_ βΆ β©-le-l) (_ βΆ β©-le-r)
β©-distribr = β©-univ (β©-le-l β _) (β©-le-r β _)
β©-distrib = β€-trans β©-distribl (β©-pres β©-distribr β©-distribr)
β©-assoc = β€-antisym
(β©-univ (β€-trans β©-le-l β©-le-l)
(β©-univ (β€-trans β©-le-l β©-le-r) β©-le-r))
(β©-univ (β©-univ β©-le-l (β€-trans β©-le-r β©-le-l))
(β€-trans β©-le-r β©-le-r))
β©-comm = β€-antisym (β©-univ β©-le-r β©-le-l) (β©-univ β©-le-r β©-le-l)
β©-idempotent = β€-antisym β©-le-l (β©-univ β€-refl β€-refl)

modular'
: β {x y z} (f : Hom x y) (g : Hom y z) (h : Hom x z)
β (g β f) β© h β€ (g β© (h β f β )) β f
modular' f g h =
(g β f) β© h                     =Λβ¨ dual _ β©=Λ
β ((g β f) β© h) β  β β            =β¨ ap! (dual-β© A) β©=
(β (g β f) β  β β© h β ) β          =β¨ ap! dual-β β©=
β ((f β  β g β ) β© h β ) β β        β€β¨ dual-β€ (modular (g β ) (f β ) (h β )) β©β€
(f β  β (g β  β© (f β  β  β h β ))) β  =β¨ dual-β β©=
(g β  β© (f β  β  β h β )) β  β f β  β  =β¨ apβ _β_ (dual-β© A) (dual f) β©=
(g β  β  β© (f β  β  β h β ) β ) β f   =β¨ apβ _β_ (apβ _β©_ (dual g) (ap _β  (apβ _β_ (dual f) refl) Β·Β· dual-β Β·Β· ap (_β f β ) (dual h))) refl β©=
(g β© h β f β ) β f               β€β


## Identitiesπ

abstract
β€-eliml : f β€ id β f β g β€ g
β€-eliml {f = f} {g = g} w =
f β g  β€β¨ w β g β©β€
id β g =β¨ idl _ β©=
g β€β

β€-elimr : g β€ id β f β g β€ f
β€-elimr {g = g} {f = f} w =
f β g  β€β¨ f βΆ w β©β€
f β id =β¨ idr _ β©=
f β€β

β€-introl : id β€ f β g β€ f β g
β€-introl {f = f} {g = g} w =
g      =β¨ sym (idl _) β©=
id β g β€β¨ w β g β©β€
f β g  β€β

β€-intror : id β€ g β f β€ f β g
β€-intror {g = g} {f = f} w =
f      =β¨ sym (idr _) β©=
f β id β€β¨ f βΆ w β©β€
f β g  β€β


## Associationsπ

  β€-pushl : a β€ b β c β a β f β€ b β c β f
β€-pushl {a = a} {b = b} {c = c} {f = f} w =
a β f       β€β¨ w β f β©β€
(b β c) β f =β¨ sym (assoc b c f) β©=
b β c β f   β€β

β€-pushr : a β€ b β c β f β a β€ (f β b) β c
β€-pushr {a = a} {b = b} {c = c} {f = f}  w =
f β a       β€β¨ f βΆ w β©β€
f β b β c   =β¨ assoc f b c β©=
(f β b) β c β€β

β€-pulll : a β b β€ c β a β b β f β€ c β f
β€-pulll {a = a} {b = b} {c = c} {f = f} w =
a β b β f   =β¨ assoc a b f β©=
(a β b) β f β€β¨ w β f β©β€
c β f       β€β

β€-pullr : a β b β€ c β (f β a) β b β€ f β c
β€-pullr {a = a} {b = b} {c = c} {f = f} w =
(f β a) β b   =β¨ sym (assoc f a b) β©=
f β a β b     β€β¨ f βΆ w β©β€
f β c         β€β

β€-extendl : a β b β€ c β d β a β b β f β€ c β d β f
β€-extendl {a = a} {b = b} {c = c} {d = d} {f = f} w =
a β b β f   β€β¨ β€-pulll w β©β€
(c β d) β f =β¨ sym (assoc c d f) β©=
c β d β f   β€β

β€-extendr : a β b β€ c β d β (f β a) β b β€ (f β c) β d
β€-extendr {a = a} {b = b} {c = c} {d = d} {f = f} w =
(f β a) β b β€β¨ β€-pullr w β©β€
f β c β d   =β¨ assoc f c d β©=
(f β c) β d β€β

β€-pull-inner : a β b β€ c β (f β a) β (b β g) β€ f β c β g
β€-pull-inner w = β€-pullr (β€-pulll w)

β€-pull-outer : a β b β€ f β c β d β€ g β a β (b β c) β d β€ f β g
β€-pull-outer w v = β€-trans (β€-pulll (β€-pulll w)) (β€-pullr v)

β€-extend-inner : a β b β€ c β d β (f β a) β (b β g) β€ (f β c) β (d β g)
β€-extend-inner w = β€-extendr (β€-extendl w)


## Cancellationsπ

  β€-cancell : a β b β€ id β a β b β f β€ f
β€-cancell w = β€-trans (β€-pulll w) (β€-eliml β€-refl)

β€-cancelr : a β b β€ id β (f β a) β b β€ f
β€-cancelr w = β€-trans (β€-pullr w) (β€-elimr β€-refl)


## Dualsπ

  β€-conj : β (f : Hom x x) β f β€ f β f β  β f
β€-conj f =
f                    β€β¨ β©-univ (β€-introl β€-refl) β€-refl β©β€
(id β f) β© f         β€β¨ modular' f id f β©β€
(id β© (f β f β )) β f β€β¨ β€-pushl β©-le-r β©β€
f β f β  β f β€β

β -pulll : a β b β  β€ c β a β (f β b) β  β€ c β f β
β -pulll {a = a} {b = b} {c = c} {f = f} w =
a β (f β b) β  =β¨ ap (a β_) dual-β β©=
a β b β  β f β  β€β¨ β€-pulll w β©β€
c β f β  β€β

β -pullr : a β  β b β€ c β (a β f) β  β b β€ f β  β c
β -pullr {a = a} {b = b} {c = c} {f = f} w =
(a β f) β  β b =β¨ ap (_β b) dual-β β©=
(f β  β a β ) β b β€β¨ β€-pullr w β©β€
f β  β c β€β

β -inner : (p : g β g' β  β‘ h) β (f β g) β (f' β g') β  β‘ f β h β f' β
β -inner p = apβ _β_ refl dual-β β sym (assoc _ _ _)
β apβ _β_ refl (assoc _ _ _ β apβ _β_ p refl)

β -cancell : a β b β  β€ id β a β (f β b) β  β€ f β
β -cancell w = β€-trans (β -pulll w) (β€-eliml β€-refl)

β -cancelr : a β  β b β€ id β (a β f) β  β b β€ f β
β -cancelr w = β€-trans (β -pullr w) (β€-elimr β€-refl)

β -cancel-inner : a β b β  β€ id β (f β a) β (g β b) β  β€ f β g β
β -cancel-inner w = β -pulll (β€-cancelr w)