search

UniMath / agda-unimath

The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
219 stars 70 forks source link

Identity systems of descent data for pushouts #1150

Closed VojtechStep closed 3 months ago

VojtechStep commented 3 months ago

This PR replaces the (unfinished, non-dependent) universal property of identity types of pushouts with the induction principle, expressed as the property of being an identity system.

I show that the canonical descent data for identity types is an identity system, and that identity systems are uniquely unique.

VojtechStep commented 3 months ago

This PR depends on #1148. New commits start at "Make flattening lemmas take non-dependent universal properties".