open import 1Lab.Path
open import 1Lab.Type

module 1Lab.Function.Reasoning where

Reasoning combinators for functionsπŸ”—

Unlike for paths and categories, reasoning about functions is often easy because composition of functions is strict, i.e.Β definitionally unital and associative.

private variable
  β„“ : Level
  A B : Type β„“
  f g h i : A β†’ B

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 steal some cute mixfix notation from agda-categories which allows us to write β‰‘βŸ¨ refl⟩∘⟨ p ⟩ instead, which is much more aesthetically pleasing!

As unification is sometimes fiddly when functions are involved, we also provide a way to write β‰‘βŸ¨ f ∘⟨ p ⟩ instead.

_⟩∘⟨_ : f ≑ h β†’ g ≑ i β†’ f ∘ g ≑ h ∘ i
_⟩∘⟨_ = apβ‚‚ (Ξ» x y β†’ x ∘ y)

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

_∘⟨_ : (f : A β†’ B) β†’ g ≑ h β†’ f ∘ g ≑ f ∘ h
f ∘⟨ p = ap (f ∘_) p

_⟩∘_ : f ≑ h β†’ (g : A β†’ B) β†’ f ∘ g ≑ h ∘ g
p ⟩∘ g = ap (_∘ g) p

infixr 39 _⟩∘⟨_ _∘⟨_ _⟩∘_