Horizontal fiber condition for pullbacks

UniMath / agda-unimath

The agda-unimath library

https://unimath.github.io/agda-unimath/

MIT License

211 stars 67 forks source link

Open fredrik-bakke opened 1 month ago

fredrik-bakke commented 1 month ago

This is a simple PR dualizing the vertical fiber condition for pullbacks.