Code

Duskin's Monadicity Theorem#76

Code

Draft

TOTBWF wants to merge 14 commits intomainthe1lab/1lab:mainfrom duskins-monadicitythe1lab/1lab:duskins-monadicityCopy head branch name to clipboard

+984-101

Commits

Commits on May 15, 2022

• defn: sections, retractions, split monos/epis

  TOTBWF

  committed
  bf86b57

  Copy full SHA for bf86b57

• defn: Add id₂ to Cat.Reasoning

  TOTBWF

  committed
  9f8475d

  Copy full SHA for 9f8475d

• defn: split coequalizers

  TOTBWF

  committed
  72ca5a3

  Copy full SHA for 72ca5a3

• defn: absoluteness of split coequalisers

  TOTBWF

  committed
  b01a536

  Copy full SHA for b01a536

• fix: tweak public exports of Finitely-complete

  TOTBWF

  committed
  4b774fb

  Copy full SHA for 4b774fb

• defn: Split coequalizers induce quotients

  TOTBWF

  committed
  8b8e735

  Copy full SHA for 8b8e735

• format: formatting fixes for split coequalisers

  TOTBWF

  committed
  b010e02

  Copy full SHA for b010e02

• format: formatting fixes for split coequaliser properties

  TOTBWF

  committed
  bad2d4c

  Copy full SHA for bad2d4c

• refactor: define product diagrams over the 2 object category

  TOTBWF

  committed
  df55454

  Copy full SHA for df55454

Commits on May 16, 2022

• defn: split epis of kernel pairs are split coequalizers

  TOTBWF

  committed
  3508d94

  Copy full SHA for 3508d94

• defn: reflection of colimits, isomorphisms of colimit coapexes

  TOTBWF

  committed
  1a79e3d

  Copy full SHA for 1a79e3d

• defn: conservative functors preserve colimits

  TOTBWF

  committed
  4f00251

  Copy full SHA for 4f00251

• defn: coequalisers are colimits

  TOTBWF

  committed
  782abd7

  Copy full SHA for 782abd7

• fixup: avoid subst in conservative-reflects-limits

  Show description for 1633a24
  plt-amy

  committed
  1633a24

  Copy full SHA for 1633a24