Descent and induction principle of identity types of coequalizers - Githubissues

UniMath / agda-unimath

The agda-unimath library

https://unimath.github.io/agda-unimath/

MIT License

219 stars 70 forks source link

Descent and induction principle of identity types of coequalizers #1140

Open VojtechStep opened 4 months ago

VojtechStep commented 4 months ago

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
variant of the flattening lemma using descent data
induction principle of identity types of coequalizers

The formalization itself is finished, but I still need to finish writing the prose in order for the PR to be mergeable