{-# OPTIONS --allow-unsolved-metas #-}
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 ; id ; idl ; idr ; assoc ; _∘_)
  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
  f fβ€² g gβ€² h : 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≀gf \le g is equivalently f=f∩gf = f \cap g, and f∩gf \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
∩-distribl   : f ∘ (g ∩ h) ≀ (f ∘ g) ∩ (f ∘ h)
∩-distribr   : (g ∩ h) ∘ f ≀ (g ∘ f) ∩ (h ∘ f)
∩-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
∩-distribl = ∩-univ (_ β–Ά ∩-le-l) (_ β–Ά ∩-le-r)
∩-distribr = ∩-univ (∩-le-l β—€ _) (∩-le-r β—€ _)
∩-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               β‰€βˆŽ

†-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)