agda-unimath
agda-unimath copied to clipboard
UniMath
The agda-unimath library
In this PR I - compute the maps induced by functoriality on inclusion morphisms of shifts of sequential diagrams - define zigzags between sequential diagrams - show that both maps...
Establishes some properties related to that the `pullback-hom` is functorial. I aim to show that orthogonal maps are closed under retracts of either map.
Fixes links and makes consistent naming changes related to the Eckmann-Hilton file. Also adds an updated reference to the page.
So, it turns out this hole goes a lot deeper than I thought, so I will have to split this PR into four parts. 1. The current PR in fact...
It seems to me that the most principled approach to adding colimits to the library through postulates is to postulate their individual existence, their dependent eliminator, and its computation rules,...
The Rust dependencies we pull in have dependencies on some native tools/libraries, which might not always be installed; I know at least about - `perl`; symptom: `Can't locate FindBin.pm in...
From this, it follows that having pairs `(eq-htpy , is-section-eq-htpy)` and `(eq-equiv , is-section-eq-equiv)` are propositions, so we can remove the redundant postulates `is-retraction-eq-(htpy|equiv)'` and `coh-eq-(htpy|equiv)'` as introduced in #1119.
A possible approach to proving this fact is to first prove that the interval type $𝕀$ (defined in `synthetic-homotopy-theory.interval-type`) is a representing object for identifications, i.e. $$A^𝕀 \simeq \sum_{(x,y:A)}(x=_Ay)$$ for...
Find the right infrastructure to make the construction of `compute-glue-cogap` just an application of a more general construction. The current construction is very almost `coherence-htpy-cocone-coherence-htpy-dependent-cocone-constant-type-family`, but an `apd-constant-type-family` has snuck...