open import 1Lab.Equiv
open import 1Lab.Path

open import Cat.Functor.Base using (module F-iso)
open import Cat.Base

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

private
  module π’ž = Cat.Reasoning π’ž
  module π’Ÿ = Cat.Reasoning π’Ÿ
open Functor F public
open F-iso F public
private variable
  A B C : π’ž.Ob
  a a' b b' c c' d : π’ž.Hom A B
  X Y Z : π’Ÿ.Ob
  f g h i : π’Ÿ.Hom X Y

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

  intro : π’Ÿ.id ≑ F₁ a
  intro = sym F-id βˆ™ ap F₁ (sym a≑id)

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

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

module _ {X : π’ž.Ob} {f : π’Ÿ.Hom (Fβ‚€ X) (Fβ‚€ X)} where

  id-equivr : (f ≑ F₁ π’ž.id) ≃ (f ≑ π’Ÿ.id)
  id-equivr = βˆ™-post-equiv F-id

  id-equivl : (F₁ π’ž.id ≑ f) ≃ (π’Ÿ.id ≑ f)
  id-equivl = βˆ™-pre-equiv (sym F-id)

  module id-equivr = Equiv id-equivr
  module id-equivl = Equiv id-equivl

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 _ (abc≑d : a π’ž.∘ b π’ž.∘ c ≑ d) where
  collapse3 : F₁ a π’Ÿ.∘ F₁ b π’Ÿ.∘ F₁ c ≑ F₁ d
  collapse3 = ap (F₁ a π’Ÿ.∘_) (sym (F-∘ b c)) βˆ™ collapse abc≑d

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

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

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

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

  extendl3 : F₁ a π’Ÿ.∘ (F₁ b π’Ÿ.∘ (F₁ c π’Ÿ.∘ f)) ≑ F₁ a' π’Ÿ.∘ (F₁ b' π’Ÿ.∘ (F₁ c' π’Ÿ.∘ f))
  extendl3 = π’Ÿ.extendl3 weave3

  extendr3 : ((f π’Ÿ.∘ F₁ a) π’Ÿ.∘ F₁ b) π’Ÿ.∘ F₁ c ≑ ((f π’Ÿ.∘ F₁ a') π’Ÿ.∘ F₁ b') π’Ÿ.∘ F₁ c'
  extendr3 = π’Ÿ.extendr3 weave3

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

popl : f π’Ÿ.∘ F₁ a ≑ g β†’ f π’Ÿ.∘ F₁ (a π’ž.∘ b) ≑ g π’Ÿ.∘ F₁ b
popl p = π’Ÿ.pushr (F-∘ _ _) βˆ™ apβ‚‚ π’Ÿ._∘_ p refl

popr : F₁ b π’Ÿ.∘ f ≑ g β†’ F₁ (a π’ž.∘ b) π’Ÿ.∘ f ≑ F₁ a π’Ÿ.∘ g
popr p = π’Ÿ.pushl (F-∘ _ _) βˆ™ apβ‚‚ π’Ÿ._∘_ refl p

pokel : g ≑ f π’Ÿ.∘ F₁ a β†’ g π’Ÿ.∘ F₁ b ≑ f π’Ÿ.∘ F₁ (a π’ž.∘ b)
pokel p = apβ‚‚ π’Ÿ._∘_ p refl βˆ™ π’Ÿ.pullr (sym (F-∘ _ _))

poker : g ≑ F₁ b π’Ÿ.∘ f β†’ F₁ a π’Ÿ.∘ g ≑ F₁ (a π’ž.∘ b) π’Ÿ.∘ f
poker p = apβ‚‚ π’Ÿ._∘_ refl p βˆ™ π’Ÿ.pulll (sym (F-∘ _ _))

shufflel : f π’Ÿ.∘ F₁ a ≑ g π’Ÿ.∘ h β†’ f π’Ÿ.∘ F₁ (a π’ž.∘ b) ≑ g π’Ÿ.∘ h π’Ÿ.∘ F₁ b
shufflel p = popl p βˆ™ sym (π’Ÿ.assoc _ _ _)

shuffler : F₁ b π’Ÿ.∘ f ≑ g π’Ÿ.∘ h β†’ F₁ (a π’ž.∘ b) π’Ÿ.∘ f ≑ (F₁ a π’Ÿ.∘ g) π’Ÿ.∘ h
shuffler p = popr p βˆ™ (π’Ÿ.assoc _ _ _)

remover : F₁ b π’Ÿ.∘ f ≑ π’Ÿ.id β†’ F₁ (a π’ž.∘ b) π’Ÿ.∘ f ≑ F₁ a
remover p = popr p βˆ™ π’Ÿ.idr _

removel : f π’Ÿ.∘ F₁ a ≑ π’Ÿ.id β†’ f π’Ÿ.∘ F₁ (a π’ž.∘ b) ≑ F₁ b
removel p = popl p βˆ™ π’Ÿ.idl _

CancellationπŸ”—

module _ (inv : a π’ž.∘ b ≑ π’ž.id) where
  annihilate : F₁ a π’Ÿ.∘ F₁ b ≑ π’Ÿ.id
  annihilate = collapse 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

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

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

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

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

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

LensesπŸ”—

unpackl
  : F₁ a π’Ÿ.∘ F₁ b ≑ f
  β†’ F₁ (a π’ž.∘ b) ≑ f
unpackl p = F-∘ _ _ βˆ™ p

packl
  : F₁ (a π’ž.∘ b) ≑ f
  β†’ F₁ a π’Ÿ.∘ F₁ b ≑ f
packl p = sym (F-∘ _ _) βˆ™ p

unpackr
  : f ≑ F₁ a π’Ÿ.∘ F₁ b
  β†’ f ≑ F₁ (a π’ž.∘ b)
unpackr p = p βˆ™ sym (F-∘ _ _)

packr
  : f ≑ F₁ (a π’ž.∘ b)
  β†’ f ≑ F₁ a π’Ÿ.∘ F₁ b
packr p = p βˆ™ F-∘ _ _

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₁