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

334 stars 63 forks source link

Closed favonia closed 3 months ago

favonia commented 3 months ago

Description

Define fibre posets, similar to fibre categories.

Before submitting a merge request, please check the items below:

[x] I've read the contributing guidelines.
[x] The imports of new modules have been sorted with support/sort-imports.hs (or nix run --experimental-features nix-command -f . sort-imports).
[x] All new code blocks have "agda" as their language.

Lavenza commented 3 months ago