Commit 6aaf089
authored
Discrete cocartesian fibrations (the1lab#458)
This PR refactors our discrete cartesian fibration module a bit, and
implements discrete cocartesian fibrations.1 parent e6e22bc commit 6aaf089
File tree
4 files changed
+517
-143
lines changed- src/Cat/Displayed
- Cartesian
- Cocartesian
- Instances
4 files changed
+517
-143
lines changed
0 commit comments