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

348 stars 68 forks source link

Closed favonia closed 4 months ago

favonia commented 4 months ago

Description

Define injections from fibre posets to the total space.

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 4 months ago