open import Cat.Prelude

import Cat.Functor.Reasoning
import Cat.Reasoning

module Cat.Natural.Reasoning
  {o β„“ o' β„“'}
  {π’ž : Precategory o β„“} {π’Ÿ : Precategory o' β„“'}
  {F G : Functor π’ž π’Ÿ}
  (Ξ± : F => G)
  where

private
  module π’ž = Cat.Reasoning  π’ž
  module π’Ÿ = Cat.Reasoning π’Ÿ
  module F = Cat.Functor.Reasoning F
  module G = Cat.Functor.Reasoning G
open _=>_ Ξ± public

private variable
  A B C : π’ž.Ob
  X Y Z : π’Ÿ.Ob
  a b c : π’ž.Hom A B
  f g h : π’Ÿ.Hom X Y

Reasoning combinators for natural transformationsπŸ”—

LensesπŸ”—

Our first set of reasoning combinators let you re-arrange goals by conjugating with naturality. The mnemonic here is that naturall lets you move the natural transformation left.

naturall
  : Ξ· _ π’Ÿ.∘ F.₁ a ≑ Ξ· _ π’Ÿ.∘ F.₁ b
  β†’ G.₁ a π’Ÿ.∘ Ξ· _ ≑ G.₁ b π’Ÿ.∘ Ξ· _
naturall p = sym (is-natural _ _ _) Β·Β· p Β·Β· is-natural _ _ _

naturalr
  : G.₁ a π’Ÿ.∘ Ξ· _ ≑ G.₁ b π’Ÿ.∘ Ξ· _
  β†’ Ξ· _ π’Ÿ.∘ F.₁ a ≑ Ξ· _ π’Ÿ.∘ F.₁ b
naturalr p = is-natural _ _ _ Β·Β· p Β·Β· sym (is-natural _ _ _)

We also provide a pair of combinators that simultaneously apply naturality and focus on a subexpression.

viewr
  : G.₁ a ≑ G.₁ b
  β†’ Ξ· _ π’Ÿ.∘ F.₁ a ≑ Ξ· _ π’Ÿ.∘ F.₁ b
viewr p = naturalr (ap (π’Ÿ._∘ Ξ· _) p)

viewl
  : F.₁ a ≑ F.₁ b
  β†’ G.₁ a π’Ÿ.∘ Ξ· _ ≑ G.₁ b π’Ÿ.∘ Ξ· _
viewl p = naturall (ap (Ξ· _ π’Ÿ.∘_) p)

Commuting Ξ· through compositesπŸ”—

pulll
  : (p : Ξ· _ π’Ÿ.∘ f ≑ g)
  β†’ Ξ· _ π’Ÿ.∘ F.₁ a π’Ÿ.∘ f ≑ G.₁ a π’Ÿ.∘ g
pulll p = π’Ÿ.pulll (is-natural _ _ _) βˆ™ π’Ÿ.pullr p

pullr
  : (p : f π’Ÿ.∘ Ξ· _ ≑ g)
  β†’ (f π’Ÿ.∘ G.₁ a) π’Ÿ.∘ Ξ· _ ≑ g π’Ÿ.∘ F.₁ a
pullr p = π’Ÿ.pullr (sym (is-natural _ _ _)) βˆ™ π’Ÿ.pulll p

popl
  : (p : Ξ· _ π’Ÿ.∘ F.₁ b ≑ f)
  β†’ Ξ· _ π’Ÿ.∘ F.₁ (a π’ž.∘ b) ≑ G.₁ a π’Ÿ.∘ f
popl p =  F.popl (is-natural _ _ _) βˆ™ π’Ÿ.pullr p

popr
  : (p : G.₁ a π’Ÿ.∘ Ξ· _ ≑ f)
  β†’ G.₁ (a π’ž.∘ b) π’Ÿ.∘ Ξ· _ ≑ f π’Ÿ.∘ F.₁ b
popr p = G.popr (sym (is-natural _ _ _)) βˆ™ π’Ÿ.pulll p

shiftl
  : (p : F.₁ a π’Ÿ.∘ f ≑ g)
  β†’ G.₁ a π’Ÿ.∘ Ξ· _ π’Ÿ.∘ f ≑ Ξ· _ π’Ÿ.∘ g
shiftl p = π’Ÿ.pulll (sym (is-natural _ _ _)) βˆ™ π’Ÿ.pullr p

shiftr
  : (p : f π’Ÿ.∘ G.₁ a ≑ g)
  β†’ (f π’Ÿ.∘ Ξ· _) π’Ÿ.∘ F.₁ a ≑ g π’Ÿ.∘ Ξ· _
shiftr p = π’Ÿ.pullr (is-natural _ _ _) βˆ™ π’Ÿ.pulll p

CancellationsπŸ”—

cancell
  : (p : Ξ· _ π’Ÿ.∘ f ≑ π’Ÿ.id)
  β†’ Ξ· _ π’Ÿ.∘ F.₁ a π’Ÿ.∘ f ≑ G.₁ a
cancell p = π’Ÿ.pulll (is-natural _ _ _) βˆ™ π’Ÿ.cancelr p

cancelr
  : (p : f π’Ÿ.∘ Ξ· _ ≑ π’Ÿ.id)
  β†’ (f π’Ÿ.∘ G.₁ a) π’Ÿ.∘ Ξ· _ ≑ F.₁ a
cancelr p = π’Ÿ.pullr (sym (is-natural _ _ _)) βˆ™ π’Ÿ.cancell p