module Cat.Reasoning {o β„“} (C : Precategory o β„“) where

open import Cat.Morphism C public

Reasoning combinators for categoriesπŸ”—

When doing category theory, we often have to perform many β€œtrivial” algebraic manipulations like reassociation, insertion of identity morphisms, etc. On paper we can omit these steps, but Agda is a bit more picky! We could just do these steps in our proofs one after another, but this clutters things up. Instead, we provide a series of reasoning combinators to make writing (and reading) proofs easier.

Most of these helpers were taken from agda-categories.

Identity morphismsπŸ”—

id-comm : βˆ€ {a b} {f : Hom a b} β†’ f ∘ id ≑ id ∘ f
id-comm {f = f} = idr f βˆ™ sym (idl f)

id-comm-sym : βˆ€ {a b} {f : Hom a b} β†’ id ∘ f ≑ f ∘ id
id-comm-sym {f = f} = idl f βˆ™ sym (idr f)

idr2 : βˆ€ {a b c} (f : Hom b c) (g : Hom a b) β†’ f ∘ g ∘ id ≑ f ∘ g
idr2 f g = ap (f ∘_) (idr g)

module _ (a≑id : a ≑ id) where abstract
  eliml : a ∘ f ≑ f
  eliml {f = f} =
    a ∘ f β‰‘βŸ¨ ap (_∘ f) a≑id βŸ©β‰‘
    id ∘ f β‰‘βŸ¨ idl f βŸ©β‰‘
    f ∎

  elimr : f ∘ a ≑ f
  elimr {f = f} =
    f ∘ a β‰‘βŸ¨ ap (f ∘_) a≑id βŸ©β‰‘
    f ∘ id β‰‘βŸ¨ idr f βŸ©β‰‘
    f ∎

  elim-inner : f ∘ a ∘ h ≑ f ∘ h
  elim-inner {f = f} = ap (f ∘_) eliml

  introl : f ≑ a ∘ f
  introl = sym eliml

  intror : f ≑ f ∘ a
  intror = sym elimr

  intro-inner : f ∘ h ≑ f ∘ a ∘ h
  intro-inner {f = f} = ap (f ∘_) introl

ReassocationsπŸ”—

We often find ourselves in situations where we have an equality involving the composition of 2 morphisms, but the association is a bit off. These combinators aim to address that situation.

module _ (ab≑c : a ∘ b ≑ c) where abstract
  pulll : a ∘ (b ∘ f) ≑ c ∘ f
  pulll {f = f} =
    a ∘ b ∘ f   β‰‘βŸ¨ assoc a b f βŸ©β‰‘
    (a ∘ b) ∘ f β‰‘βŸ¨ ap (_∘ f) ab≑c βŸ©β‰‘
    c ∘ f ∎

  pullr : (f ∘ a) ∘ b ≑ f ∘ c
  pullr {f = f} =
    (f ∘ a) ∘ b β‰‘Λ˜βŸ¨ assoc f a b βŸ©β‰‘Λ˜
    f ∘ (a ∘ b) β‰‘βŸ¨ ap (f ∘_) ab≑c βŸ©β‰‘
    f ∘ c ∎

  pull-inner : (f ∘ a) ∘ (b ∘ g) ≑ f ∘ c ∘ g
  pull-inner {f = f} = sym (assoc _ _ _) βˆ™ ap (f ∘_) pulll

module _ (c≑ab : c ≑ a ∘ b) where abstract
  pushl : c ∘ f ≑ a ∘ (b ∘ f)
  pushl = sym (pulll (sym c≑ab))

  pushr : f ∘ c ≑ (f ∘ a) ∘ b
  pushr = sym (pullr (sym c≑ab))

  push-inner : f ∘ c ∘ g ≑ (f ∘ a) ∘ (b ∘ g)
  push-inner {f = f} = ap (f ∘_) pushl βˆ™ assoc _ _ _

module _ (p : f ∘ h ≑ g ∘ i) where abstract
  extendl : f ∘ (h ∘ b) ≑ g ∘ (i ∘ b)
  extendl {b = b} =
    f ∘ (h ∘ b) β‰‘βŸ¨ assoc f h b βŸ©β‰‘
    (f ∘ h) ∘ b β‰‘βŸ¨ ap (_∘ b) p βŸ©β‰‘
    (g ∘ i) ∘ b β‰‘Λ˜βŸ¨ assoc g i b βŸ©β‰‘Λ˜
    g ∘ (i ∘ b) ∎

  extendr : (a ∘ f) ∘ h ≑ (a ∘ g) ∘ i
  extendr {a = a} =
    (a ∘ f) ∘ h β‰‘Λ˜βŸ¨ assoc a f h βŸ©β‰‘Λ˜
    a ∘ (f ∘ h) β‰‘βŸ¨ ap (a ∘_) p βŸ©β‰‘
    a ∘ (g ∘ i) β‰‘βŸ¨ assoc a g i βŸ©β‰‘
    (a ∘ g) ∘ i ∎

  extend-inner : a ∘ f ∘ h ∘ b ≑ a ∘ g ∘ i ∘ b
  extend-inner {a = a} = ap (a ∘_) extendl

CancellationπŸ”—

These lemmas do 2 things at once: rearrange parenthesis, and also remove things that are equal to id.

module _ (inv : h ∘ i ≑ id) where abstract
  cancell : h ∘ (i ∘ f) ≑ f
  cancell {f = f} =
    h ∘ (i ∘ f) β‰‘βŸ¨ pulll inv βŸ©β‰‘
    id ∘ f      β‰‘βŸ¨ idl f βŸ©β‰‘
    f           ∎

  cancelr : (f ∘ h) ∘ i ≑ f
  cancelr {f = f} =
    (f ∘ h) ∘ i β‰‘βŸ¨ pullr inv βŸ©β‰‘
    f ∘ id      β‰‘βŸ¨ idr f βŸ©β‰‘
    f           ∎

  insertl : f ≑ h ∘ (i ∘ f)
  insertl = sym cancell

  insertr : f ≑ (f ∘ h) ∘ i
  insertr = sym cancelr

  cancel-inner : (f ∘ h) ∘ (i ∘ g) ≑ f ∘ g
  cancel-inner = pulll cancelr

  insert-inner : f ∘ g ≑ (f ∘ h) ∘ (i ∘ g)
  insert-inner = pushl insertr

  deleter : (f ∘ g ∘ h) ∘ i ≑ f ∘ g
  deleter = pullr cancelr

  deletel : h ∘ (i ∘ f) ∘ g ≑ f ∘ g
  deletel = pulll cancell

We also have combinators which combine expanding on one side with a cancellation on the other side:

lswizzle : g ≑ h ∘ i β†’ f ∘ h ≑ id β†’ f ∘ g ≑ i
lswizzle {g = g} {h = h} {i = i} {f = f} p q =
  f ∘ g     β‰‘βŸ¨ apβ‚‚ _∘_ refl p βŸ©β‰‘
  f ∘ h ∘ i β‰‘βŸ¨ cancell q βŸ©β‰‘
  i         ∎

rswizzle : g ≑ i ∘ h β†’ h ∘ f ≑ id β†’ g ∘ f ≑ i
rswizzle {g = g} {i = i} {h = h} {f = f} p q =
  g ∘ f       β‰‘βŸ¨ apβ‚‚ _∘_ p refl βŸ©β‰‘
  (i ∘ h) ∘ f β‰‘βŸ¨ cancelr q βŸ©β‰‘
  i           ∎

IsomorphismsπŸ”—

These lemmas are useful for proving that partial inverses to an isomorphism are unique. There’s a helper for proving uniqueness of left inverses, of right inverses, and for proving that any left inverse must match any right inverse.

module _ {y z} (f : y β‰… z) where abstract
  open _β‰…_

  left-inv-unique
    : βˆ€ {g h}
    β†’ g ∘ f .to ≑ id β†’ h ∘ f .to ≑ id
    β†’ g ≑ h
  left-inv-unique {g = g} {h = h} p q =
    g                   β‰‘βŸ¨ intror (f .invl) βŸ©β‰‘
    g ∘ f .to ∘ f .from β‰‘βŸ¨ extendl (p βˆ™ sym q) βŸ©β‰‘
    h ∘ f .to ∘ f .from β‰‘βŸ¨ elimr (f .invl) βŸ©β‰‘
    h                   ∎

  left-right-inv-unique
    : βˆ€ {g h}
    β†’ g ∘ f .to ≑ id β†’ f .to ∘ h ≑ id
    β†’ g ≑ h
  left-right-inv-unique {g = g} {h = h} p q =
    g                    β‰‘βŸ¨ intror (f .invl) βŸ©β‰‘
    g ∘ f .to ∘ f .from  β‰‘βŸ¨ cancell p βŸ©β‰‘
    f .from              β‰‘βŸ¨ intror q βŸ©β‰‘
    f .from ∘ f .to ∘ h  β‰‘βŸ¨ cancell (f .invr) βŸ©β‰‘
    h                    ∎

  right-inv-unique
    : βˆ€ {g h}
    β†’ f .to ∘ g ≑ id β†’ f .to ∘ h ≑ id
    β†’ g ≑ h
  right-inv-unique {g = g} {h} p q =
    g                     β‰‘βŸ¨ introl (f .invr) βŸ©β‰‘
    (f .from ∘ f .to) ∘ g β‰‘βŸ¨ pullr (p βˆ™ sym q) βŸ©β‰‘
    f .from ∘ f .to ∘ h   β‰‘βŸ¨ cancell (f .invr) βŸ©β‰‘
    h                     ∎

If we have a commuting triangle of isomorphisms, then we can flip one of the sides to obtain a new commuting triangle of isomorphisms.

Iso-swapr :
  βˆ€ {a : x β‰… y} {b : y β‰… z} {c : x β‰… z}
  β†’ a ∘Iso b ≑ c
  β†’ a ≑ c ∘Iso (b Iso⁻¹)
Iso-swapr {a = a} {b = b} {c = c} p = β‰…-path $
  a .to                     β‰‘βŸ¨ introl (b .invr) βŸ©β‰‘
  (b .from ∘ b .to) ∘ a .to β‰‘βŸ¨ pullr (ap to p) βŸ©β‰‘
  b .from ∘ c .to           ∎

Iso-swapl :
  βˆ€ {a : x β‰… y} {b : y β‰… z} {c : x β‰… z}
  β†’ a ∘Iso b ≑ c
  β†’ b ≑ (a Iso⁻¹) ∘Iso c
Iso-swapl {a = a} {b = b} {c = c} p = β‰…-path $
  b .to                   β‰‘βŸ¨ intror (a .invl) βŸ©β‰‘
  b .to ∘ a .to ∘ a .from β‰‘βŸ¨ pulll (ap to p) βŸ©β‰‘
  c .to ∘ a .from         ∎

Assume we have a prism of isomorphisms, as in the following diagram:

If the top, front, left, and right faces all commute, then so does the bottom face.

Iso-prism : βˆ€ {a : u β‰… v} {b : v β‰… w} {c : u β‰… w}
      β†’ {d : u β‰… x} {e : v β‰… y} {f : w β‰… z}
      β†’ {g : x β‰… y} {h : y β‰… z} {i : x β‰… z}
      β†’ a ∘Iso b ≑ c
      β†’ a ∘Iso e ≑ d ∘Iso g
      β†’ b ∘Iso f ≑ e ∘Iso h
      β†’ c ∘Iso f ≑ d ∘Iso i
      β†’ g ∘Iso h ≑ i
Iso-prism {a = a} {b} {c} {d} {e} {f} {g} {h} {i} top left right front =
  β‰…-path $
    h .to ∘ g .to                                           β‰‘βŸ¨ apβ‚‚ _∘_ (ap to (Iso-swapl (sym right))) (ap to (Iso-swapl (sym left)) βˆ™ sym (assoc _ _ _)) βŸ©β‰‘
    ((f .to ∘ b .to) ∘ e .from) ∘ (e .to ∘ a .to ∘ d .from) β‰‘βŸ¨ cancel-inner (e .invr) βŸ©β‰‘
    (f .to ∘ b .to) ∘ (a .to ∘ d .from)                     β‰‘βŸ¨ pull-inner (ap to top) βŸ©β‰‘
    f .to ∘ c .to ∘ d .from                                 β‰‘βŸ¨ assoc _ _ _ βˆ™ sym (ap to (Iso-swapl (sym front))) βŸ©β‰‘
    i .to ∎

NotationπŸ”—

When doing equational reasoning, it’s often somewhat clumsy to have to write ap (f ∘_) p when proving that f ∘ g ≑ f ∘ h. To fix this, we define steal some cute mixfix notation from agda-categories which allows us to write β‰‘βŸ¨ refl⟩∘⟨ p ⟩ instead, which is much more aesthetically pleasing!

_⟩∘⟨_ : f ≑ h β†’ g ≑ i β†’ f ∘ g ≑ h ∘ i
_⟩∘⟨_ = apβ‚‚ _∘_

infixr 40 _⟩∘⟨_

refl⟩∘⟨_ : g ≑ h β†’ f ∘ g ≑ f ∘ h
refl⟩∘⟨_ {f = f} p = ap (f ∘_) p

_⟩∘⟨refl : f ≑ h β†’ f ∘ g ≑ h ∘ g
_⟩∘⟨refl {g = g} p = ap (_∘ g) p