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