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  _◀_ _▶_
infixr  _=⟨_⟩_ _=˘⟨_⟩_ _≤⟨_⟩_
infix   _≤∎

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)