Characterize identity types of dependent sequential diagrams

UniMath / agda-unimath

The agda-unimath library

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

MIT License

211 stars 67 forks source link

Characterize identity types of dependent sequential diagrams #1149

Closed VojtechStep closed 3 weeks ago

VojtechStep commented 3 weeks ago

Equivalences of dependent sequential diagrams characterize their identity type

VojtechStep commented 3 weeks ago

I just had this laying around for some time. This PR is completely orthogonal to the other refactors/enhancements I'm doing to synthetic homotopy theory right now.