search

maxsnew / cubical-categorical-logic

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

Vertical products #94

Closed hejohns closed 5 months ago

hejohns commented 5 months ago

After one more cleaning pass, this is ready for review

maxsnew commented 5 months ago

I just tweaked the gluing example slightly to make the generator a single morphism from 1 to ans x ans, so that it uses the products in a slightly non-trivial way

hejohns commented 5 months ago

I just tweaked the gluing example slightly to make the generator a single morphism from 1 to ans x ans, so that it uses the products in a slightly non-trivial way

Great, thanks for doing that

maxsnew commented 5 months ago

whoops meant to squash and merge, oh well.