UniMath / GrpdHITs

6 stars 3 forks source link

PIE #8

Closed nmvdw closed 3 years ago

nmvdw commented 3 years ago

Say in the introduction that PIE limits are homotopy limits, since our bicategories are (2,1)-categories.

We show that the bicategory of algebras has PIE limits and we prove a version of the first isomorphism theorem for 1-types

We prove that this bicategory has PIE limits.

Cite: Homotopy limits in type theory

co-dan commented 3 years ago

P I E