Add the universal property of identity systems to the overview tables (…

…UniMath#789)
fredrik-bakke · Sep 19, 2023 · a081293 · a081293
1 parent 9d2c235
commit a081293
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/src/foundation-core/identity-types.lagda.md b/src/foundation-core/identity-types.lagda.md
@@ -69,6 +69,7 @@ identifications in arbitrary types.
 | Torsorial type families                           | [`foundation.torsorial-type-families`](foundation.torsorial-type-families.md)                                             |
 | Transport along identifications (foundation)      | [`foundation.transport-along-identifications`](foundation.transport-along-identifications.md)                             |
 | Transport along identifications (foundation-core) | [`foundation-core.transport-along-identifications`](foundation-core.transport-along-identifications.md)                   |
+| The universal property of identity systems        | [`foundation.universal-property-identity-systems`](foundation.universal-property-identity-systems.md)                     |
 | The universal property of identity types          | [`foundation.universal-property-identity-types`](foundation.universal-property-identity-types.md)                         |
 
 ## Definition

diff --git a/src/foundation/identity-types.lagda.md b/src/foundation/identity-types.lagda.md
@@ -57,6 +57,7 @@ identifications in arbitrary types.
 | Torsorial type families                           | [`foundation.torsorial-type-families`](foundation.torsorial-type-families.md)                                             |
 | Transport along identifications (foundation)      | [`foundation.transport-along-identifications`](foundation.transport-along-identifications.md)                             |
 | Transport along identifications (foundation-core) | [`foundation-core.transport-along-identifications`](foundation-core.transport-along-identifications.md)                   |
+| The universal property of identity systems        | [`foundation.universal-property-identity-systems`](foundation.universal-property-identity-systems.md)                     |
 | The universal property of identity types          | [`foundation.universal-property-identity-types`](foundation.universal-property-identity-types.md)                         |
 
 ## Properties