Code

Create Adjunctions.agda#326

Code

Draft

tetrapharmakon wants to merge 46 commits intoagda:masteragda/agda-categories:masterfrom tetrapharmakon:patch-4tetrapharmakon/agda-categories:patch-4Copy head branch name to clipboard

+397-9

Commits

Commits on Nov 30, 2021

• Create Adjunctions.agda

  Show description for 1806521
  

  fouche

  authored
  1806521

  Copy full SHA for 1806521

• whoops, file was in the wrong place

  

  fouche

  committed
  c6f1d21

  Copy full SHA for c6f1d21

• stub one thing at a time...

  

  fouche

  committed
  4f12528

  Copy full SHA for 4f12528

• little progress

  

  fouche

  committed
  5973e7f

  Copy full SHA for 5973e7f

Commits on Dec 1, 2021

• Finish Split category definition

  iwilare

  committed
  f755c48

  Copy full SHA for f755c48

• def of kleisli-object

  

  fouche

  committed
  5700870

  Copy full SHA for 5700870

Commits on Dec 2, 2021

• revert to 1.7

  

  fouche

  committed
  fa0b87c

  Copy full SHA for fa0b87c

• progress

  

  fouche

  committed
  f1bc8e7

  Copy full SHA for f1bc8e7

• proof of Kl-initial

  

  fouche

  committed
  a0b6dba

  Copy full SHA for a0b6dba

• cose

  

  fouche

  committed
  59d6ef6

  Copy full SHA for 59d6ef6

• Clean modules and definitions

  iwilare

  committed
  b9f877c

  Copy full SHA for b9f877c

Commits on Dec 9, 2021

• lazily think about it

  

  fouche

  committed
  f6168a8

  Copy full SHA for f6168a8

• revert agda-lib to 1.7

  

  fouche

  committed
  fd94bd7

  Copy full SHA for fd94bd7

Commits on Jan 14, 2022

• a blind, automatic commit

  

  fouche

  committed
  38c00aa

  Copy full SHA for 38c00aa

Commits on May 29, 2022

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

  iwilare

  committed
  44603fc

  Copy full SHA for 44603fc

Commits on Jul 23, 2022

• Refactor with simpler names

  iwilare

  committed
  1166118

  Copy full SHA for 1166118

Commits on Aug 6, 2022

• Simplify homomorphism, refactor into lemma on adjunction

  iwilare

  committed
  f1ad63f

  Copy full SHA for f1ad63f

Commits on Aug 18, 2022

• Complete homomorphism for bang

  iwilare

  committed
  0439ad0

  Copy full SHA for 0439ad0

Commits on Aug 19, 2022

• Progress on initiality of Kleisli

  iwilare

  committed
  f876929

  Copy full SHA for f876929

Commits on Jan 2, 2023

• WIP

  iwilare

  committed
  a23a132

  Copy full SHA for a23a132

Commits on Jan 3, 2023

• gnagna

  

  fouche

  committed
  f731926

  Copy full SHA for f731926

• WIP with μ-comp

  iwilare

  committed
  30aad51

  Copy full SHA for 30aad51

Commits on Jan 9, 2023

• Minima

  iwilare

  committed
  4b25a8b

  Copy full SHA for 4b25a8b

• aloora

  

  fouche

  committed
  ac22091

  Copy full SHA for ac22091

• pulizia

  

  fouche

  committed
  d9f6b10

  Copy full SHA for d9f6b10

• underscore

  

  fouche

  committed
  260272d

  Copy full SHA for 260272d

• ostia

  

  fouche

  committed
  0c9a245

  Copy full SHA for 0c9a245

• nomi di mucomp

  

  fouche

  committed
  f13489a

  Copy full SHA for f13489a

• un mucomp fatto

  

  fouche

  committed
  399992c

  Copy full SHA for 399992c

• underscores

  

  fouche

  committed
  6926096

  Copy full SHA for 6926096

• qualcosa fatto

  

  fouche

  committed
  c25e87b

  Copy full SHA for c25e87b

• removed ids

  

  fouche

  committed
  baec081

  Copy full SHA for baec081

• swoosh

  

  fouche

  committed
  4543667

  Copy full SHA for 4543667

Commits on Jan 10, 2023

• simplify mucomp ids

  

  fouche

  committed
  b4972e3

  Copy full SHA for b4972e3

• smol steps

  

  fouche

  committed
  3902c5b

  Copy full SHA for 3902c5b

• mucomp fatto

  

  fouche

  committed
  42cebd6

  Copy full SHA for 42cebd6

• typechecka fin qui

  

  fouche

  committed
  09b1dda

  Copy full SHA for 09b1dda

• KL-initial

  

  fouche

  committed
  3c1a416

  Copy full SHA for 3c1a416

• remove push of pippo

  

  fouche

  committed
  72e3bea

  Copy full SHA for 72e3bea

• just a comp from the end

  

  fouche

  committed
  a576da1

  Copy full SHA for a576da1

• Minima

  iwilare

  committed
  d2cf221

  Copy full SHA for d2cf221

Commits on Jan 11, 2023

• smol homomorphism

  

  fouche

  committed
  27dd32d

  Copy full SHA for 27dd32d

• Style fixes

  iwilare

  committed
  7712bb5

  Copy full SHA for 7712bb5

• Make terms explicit

  iwilare

  committed
  20c26f8

  Copy full SHA for 20c26f8

• Revert Categories.Tactic.Category

  iwilare

  committed
  e963814

  Copy full SHA for e963814

Commits on Jan 12, 2023

• Small progress on mu-comp

  iwilare

  committed
  3cee6a1

  Copy full SHA for 3cee6a1