agda-unimath
agda-unimath copied to clipboard
UniMath
The agda-unimath library
Formalizes a fine-grained analysis of the construction used for the Cantor-Schröder-Bernstein-Escardó theorem, and uses this deconstruction to give a series of generalizations of the theorem. Perhaps most importantly, although not...
This pull request is part of the formalization of higher category theory project with Ivan. Here we construct Hofmann-Streicher universes for: - directed graphs - reflexive directed graphs - globular...
If we are to give credit to the original formalizers of the "100 theorems" theorems, we need to know who they are. For easy reference, the agda-unimath page on "Formalizing...
I'm guessing this is related to #658 and is a bug on the side of `mdbook`. Still, I wanted to at least record it.
@spcfox made an impressive pull request, but unfortunately we haven't heard from him since. This is an attempt to bring his pull request to a mergeable state.
Adds a module about iterating families of maps over a map, and does some refactoring for inverse sequential diagrams.
I see some ill-formed concept macro invocations are slipping through the cracks, such as the following in [`synthetic-catetegory-theory.equivalences-synthetic-categories`](https://unimath.github.io/agda-unimath/synthetic-category-theory.equivalences-synthetic-categories.html): ```md {{#concept "equivalence" Disambiguation="Synthetic categories}} ``` surely such invocations should not be...
Defines continuation modalities as a generalization of the double negation modality, and shows they define Lavwere–Tierney topologies on types. It also improves term usage in the file about reflective subuniverses.
- When the domain is $n+r+2$-truncated the type of $n$-path-cosplittings is $r$-truncated - When the domain is $n+1$-truncated $n$-path-cosplittings are unique - When the domain is $n$-truncated there are unique...
### Summary - Implement a new naming scheme for files about local and separated objects at localizations/subuniverses/maps, as discussed with Egbert privately. - Improve particular wordings in the OFS namespace....