search

the1lab / 1lab

A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory
https://1lab.dev
GNU Affero General Public License v3.0
333 stars 63 forks source link

(Co)Limit Reasoning Module #84

Open TOTBWF opened 2 years ago

TOTBWF commented 2 years ago

It would be nice to have a good API for reasoning about (Co)Limits, much like we have with Cat.Reasoning and Cat.Functor.Reasoning.

TOTBWF commented 2 years ago

@plt-amy do you have any concrete design suggestions for this?