agda-unimath
agda-unimath copied to clipboard
UniMath
The agda-unimath library
## Goals **Overarching goal:** formalize the positive results from _Idempotents in Intensional Type Theory_. - [x] Infrastructure for the total type of retracts of a type - [X] Infrastructure for...
### Discussed in https://github.com/UniMath/agda-unimath/discussions/1102 Originally posted by **fredrik-bakke** March 30, 2024 Since the carrier types are sets the proofs are already irrelevant so it seems reasonable to do this. On...
Refactors some equivalences related to coproducs and adds one new definition. - removes the abstract block around `is-equiv-coproduct` in `foundation.functorality-coproduct-types`, thus allowing `map-inv-equiv (equiv-coproduct e e')` to compute to `map-coproduct...
This pull request introduces the concept of subsequence of a sequence and asymptotical behavior of sequences. In addition, we introduce a few illustrative results using these concepts on sequences in...
Module containing the formalization of normal modal logics. It includes: - Syntax and Kripke semantics of modal logics - Definition of modal logics K and S5 - Constructive proofs of...
This is a simple PR dualizing the vertical fiber condition for pullbacks.
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...
The biggest changes come from a change in the definition of the quotient of a divisible natural number. The updated definition defines the quotient of `n` by `d`, provided that...