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