Prove SETᴰ is a fibration

maxsnew / cubical-categorical-logic

Extensions to the cubical stdlib category theory for categorical logic/type theory

MIT License

25 stars 5 forks source link

Prove SETᴰ is a fibration #63

Closed maxsnew closed 8 months ago

maxsnew commented 8 months ago

part of https://github.com/maxsnew/multi-poly-cats/issues/62

maxsnew commented 8 months ago

Ok I pushed a little more that implements the reverse direction between hi tech and explicit notion of cartesian lifts. Should be good to go now @hejohns