search

maxsnew / cubical-categorical-logic

Extensions to the cubical stdlib category theory for categorical logic/type theory
MIT License
21 stars 5 forks source link

Relative Monad Theory #77

Open maxsnew opened 1 month ago

maxsnew commented 1 month ago

Relative adjunctions, monads, algebras and prove that the forgetful functor from algebras reflects limits.

maxsnew commented 1 month ago

WIP on https://github.com/maxsnew/cubical-categorical-logic/pull/92