Create Adjunctions.agda#326

Draft

tetrapharmakon wants to merge 46 commits intoagda:masterfrom

tetrapharmakon:patch-4

Commits on Nov 30, 2021

Create Adjunctions.agda
fouche
authored
whoops, file was in the wrong place
fouche
committed
stub one thing at a time...
fouche
committed
little progress
fouche
committed

Commits on Dec 1, 2021

Finish Split category definition
iwilare
committed
def of kleisli-object
fouche
committed

Commits on Dec 2, 2021

revert to 1.7
fouche
committed
progress
fouche
committed
proof of Kl-initial
fouche
committed
cose
fouche
committed
Clean modules and definitions
iwilare
committed

Commits on Dec 9, 2021

lazily think about it
fouche
committed
revert agda-lib to 1.7
fouche
committed

Commits on Jan 14, 2022

a blind, automatic commit
fouche
committed

Commits on May 29, 2022

Add μ-eq, move to Adjunction.Properties, fill some definitions
iwilare
committed

Commits on Jul 23, 2022

Refactor with simpler names
iwilare
committed

Commits on Aug 6, 2022

Simplify homomorphism, refactor into lemma on adjunction
iwilare
committed

Commits on Aug 18, 2022

Complete homomorphism for bang
iwilare
committed

Commits on Aug 19, 2022

Progress on initiality of Kleisli
iwilare
committed

Commits on Jan 2, 2023

WIP
iwilare
committed

Commits on Jan 3, 2023

gnagna
fouche
committed
WIP with μ-comp
iwilare
committed

Commits on Jan 9, 2023

Commits on Jan 10, 2023

simplify mucomp ids
fouche
committed
smol steps
fouche
committed
mucomp fatto
fouche
committed
typechecka fin qui
fouche
committed
KL-initial
fouche
committed
remove push of pippo
fouche
committed
just a comp from the end
fouche
committed
Minima
iwilare
committed

Commits on Jan 11, 2023

smol homomorphism
fouche
committed
Style fixes
iwilare
committed
Make terms explicit
iwilare
committed
Revert Categories.Tactic.Category
iwilare
committed

Commits on Jan 12, 2023

Small progress on mu-comp
iwilare
committed