Code

Relative monad#92

Code

Draft

maxsnew wants to merge 11 commits intomainmaxsnew/cubical-categorical-logic:mainfrom

relative-monadmaxsnew/cubical-categorical-logic:relative-monadCopy head branch name to clipboard

Commits

Commits on May 20, 2024

• Monads relative to a profunctor and their algebras

  maxsnew

  committed
  a93e638

  Copy full SHA for a93e638

• fix universes in Displayed Functor cat, some more displayed limits

  maxsnew

  committed
  a1cbf6f

  Copy full SHA for a1cbf6f

• [broken] WIP on algebras lift limits

  maxsnew

  committed
  78ed9e9

  Copy full SHA for 78ed9e9

• line lengths

  maxsnew

  committed
  2a17987

  Copy full SHA for 2a17987

Commits on Jun 14, 2024

• checkin, but found limitation: need a preservation of limits

  Show description for c13706e
  maxsnew

  committed
  c13706e

  Copy full SHA for c13706e

Commits on Jun 24, 2024

• tiny tweak to wip on algebras lift limits

  maxsnew

  committed
  c0c73c6

  Copy full SHA for c0c73c6

Commits on Jun 25, 2024

• displayed category of elements of sets, presheaves

  maxsnew

  committed
  f990e21

  Copy full SHA for f990e21

• define preservation of limits

  maxsnew

  committed
  3ebb4c4

  Copy full SHA for 3ebb4c4

• correct definition of a displayed category lifting a limit

  maxsnew

  committed
  19610f0

  Copy full SHA for 19610f0

• fix the assumptions for the ALGEBRA lifts limits proof

  maxsnew

  committed
  93cb85f

  Copy full SHA for 93cb85f

• tweak to preservesLimit definition

  maxsnew

  committed
  9481be0

  Copy full SHA for 9481be0