open import 1Lab.Path

open import Cat.Base

import Cat.Reasoning

module Cat.Functor.Reasoning
  {o β„“ oβ€² β„“β€²}
  {π’ž : Precategory o β„“} {π’Ÿ : Precategory oβ€² β„“β€²}
  (F : Functor π’ž π’Ÿ) where

module π’ž = Cat.Reasoning π’ž
module π’Ÿ = Cat.Reasoning π’Ÿ
open Functor F public

Reasoning Combinators for FunctorsπŸ”—

The combinators exposed in category reasoning abstract out a lot of common algebraic manipulations, and make proofs much more concise. However, once functors get involved, those combinators start to get unwieldy! Therefore, we have to write some new combinators for working with functors specifically. This module is meant to be imported qualified.

Identity MorphismsπŸ”—

module _ (a≑id : a ≑ π’ž.id) where
  elim : F₁ a ≑ π’Ÿ.id
  elim = ap F₁ a≑id βˆ™ F-id

  eliml : F₁ a π’Ÿ.∘ f ≑ f 
  eliml = π’Ÿ.eliml elim

  elimr : f π’Ÿ.∘ F₁ a ≑ f
  elimr = π’Ÿ.elimr elim

  introl : f ≑ F₁ a π’Ÿ.∘ f
  introl = π’Ÿ.introl elim

  intror : f ≑ f π’Ÿ.∘ F₁ a
  intror = π’Ÿ.intror elim

ReassociationsπŸ”—

module _ (ab≑c : a π’ž.∘ b ≑ c) where
  collapse : F₁ a π’Ÿ.∘ F₁ b ≑ F₁ c
  collapse = sym (F-∘ a b) βˆ™ ap F₁ ab≑c

  pulll : F₁ a π’Ÿ.∘ (F₁ b π’Ÿ.∘ f) ≑ F₁ c π’Ÿ.∘ f
  pulll = π’Ÿ.pulll collapse

  pullr : (f π’Ÿ.∘ F₁ a) π’Ÿ.∘ F₁ b ≑ f π’Ÿ.∘ F₁ c
  pullr = π’Ÿ.pullr collapse

module _ (c≑ab : c ≑ a π’ž.∘ b) where
  expand : F₁ c ≑ F₁ a π’Ÿ.∘ F₁ b
  expand = sym (collapse (sym c≑ab))

  pushl : F₁ c π’Ÿ.∘ f ≑ F₁ a π’Ÿ.∘ (F₁ b π’Ÿ.∘ f)
  pushl = π’Ÿ.pushl expand

  pushr : f π’Ÿ.∘ F₁ c ≑ (f π’Ÿ.∘ F₁ a) π’Ÿ.∘ F₁ b
  pushr = π’Ÿ.pushr expand

module _ (p : a π’ž.∘ c ≑ b π’ž.∘ d) where
  weave : F₁ a π’Ÿ.∘ F₁ c ≑ F₁ b π’Ÿ.∘ F₁ d
  weave = sym (F-∘ a c) βˆ™ ap F₁ p βˆ™ F-∘ b d

  extendl : F₁ a π’Ÿ.∘ (F₁ c π’Ÿ.∘ f) ≑ F₁ b π’Ÿ.∘ (F₁ d π’Ÿ.∘ f)
  extendl = π’Ÿ.extendl weave

  extendr : (f π’Ÿ.∘ F₁ a) π’Ÿ.∘ F₁ c ≑ (f π’Ÿ.∘ F₁ b) π’Ÿ.∘ F₁ d
  extendr = π’Ÿ.extendr weave

  extend-inner :
    f π’Ÿ.∘ F₁ a π’Ÿ.∘ F₁ c π’Ÿ.∘ g ≑ f π’Ÿ.∘ F₁ b π’Ÿ.∘ F₁ d π’Ÿ.∘ g
  extend-inner = π’Ÿ.extend-inner weave

CancellationπŸ”—

module _ (inv : a π’ž.∘ b ≑ π’ž.id) where
  annihilate : F₁ a π’Ÿ.∘ F₁ b ≑ π’Ÿ.id
  annihilate = sym (F-∘ a b) βˆ™ ap F₁ inv βˆ™ F-id

  cancell : F₁ a π’Ÿ.∘ (F₁ b π’Ÿ.∘ f) ≑ f
  cancell = π’Ÿ.cancell annihilate

  cancelr : (f π’Ÿ.∘ F₁ a) π’Ÿ.∘ F₁ b ≑ f
  cancelr = π’Ÿ.cancelr annihilate

  insertl : f ≑ F₁ a π’Ÿ.∘ (F₁ b π’Ÿ.∘ f)
  insertl = π’Ÿ.insertl annihilate

  insertr : f ≑ (f π’Ÿ.∘ F₁ a) π’Ÿ.∘ F₁ b
  insertr = π’Ÿ.insertr annihilate

  cancel-inner : (f π’Ÿ.∘ F₁ a) π’Ÿ.∘ (F₁ b π’Ÿ.∘ g) ≑ f π’Ÿ.∘ g
  cancel-inner = π’Ÿ.cancel-inner annihilate

NotationπŸ”—

Writing ap F₁ p is somewhat clunky, so we define a bit of notation to make it somewhat cleaner.

⟨_⟩ : a ≑ b β†’ F₁ a ≑ F₁ b
⟨_⟩ = ap F₁