Vojtěch Štěpančík
Vojtěch Štěpančík
The first middle-dot is · ("MIDDLE DOT", codepoint #xb7), and it's used in left and right whiskering (`_·l_` and `_·r_` in `foundation-core.homotopies`). The other one is ∙ ("BULLET OPERATOR", codepoint...
Chapter names are used for rendering the sidebar table of contents. When it contains latex markup, then it's rendered correctly in the chapter contents, but the sidebar has the unrendered...
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...
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...
This PR adds the following constructions and proofs around coequalizers: - descent data, morphisms and equivalences - descent property of coequalizers - characterizations of various type families over coequalizers -...
@JobPetrovcic created an interactive graph for exploring definitions in the library. This PR embeds the explorer on our website. Some more work is still required outside of this repository, which...
### Bug report criteria - [X] This bug report is not security related, security issues should be disclosed privately via [etcd maintainers](mailto:[email protected]). - [X] This is not a support request...
Still a draft with a long way to go. This is now my procrastination fuel. Typos/potential oversights found during transcription: - Page 114, Exercise 9.7 (e), typo in condition (ii)...
~~There are still two holes left to fill, but they seem to be conceptually easy enough that I'm confident publishing this *draft* PR now — in particular they don't have...
Reasoning syntax doesn't produce the expected result for relations which aren't strictly left unital
Equational reasoning works as advertised: `equational-reasoning x ＝ y by p` computes to `p`, but it relies on `refl` being a strict left unit with respect to path composition, since...