From c6d981cf6bdbd41888b7ed47700040e6c69e4037 Mon Sep 17 00:00:00 2001 From: 5HT Date: Tue, 24 Oct 2023 20:38:06 +0300 Subject: [PATCH] identity system --- foundations/mltt/id/index.html | 4 ++-- foundations/mltt/id/index.pug | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/foundations/mltt/id/index.html b/foundations/mltt/id/index.html index 25eb6b92..56d386cf 100644 --- a/foundations/mltt/id/index.html +++ b/foundations/mltt/id/index.html @@ -47,9 +47,9 @@ (d : C a a (=-ctor a)), Path (C a a (=-ctor a)) d (=-elim a C d a (=-ctor a))), 𝟏

There are number of equality signs used in this tutorial, -all of them listed in the following table of identity systems:

(Fundamental Theorem of Identity System).

(Strict Identity System). An identity system +all of them listed in the following table of identity systems:

(Fundamental Theorem of Identity System).

(Strict Identity System). An identity system over type and universe of pretypes is called strict identity -system (), which respects UIP.

(Homotopy Identity System). An identity system +system (), which respects UIP.

(Homotopy Identity System). An identity system over type and universe of homotopy types is called homotopy identity system (), which models discrete infinity groupoid.

\ No newline at end of file diff --git a/foundations/mltt/id/index.pug b/foundations/mltt/id/index.pug index f5347a22..c85959c8 100644 --- a/foundations/mltt/id/index.pug +++ b/foundations/mltt/id/index.pug @@ -141,11 +141,11 @@ block content +tex. $\mathbf{Theorem\ 3.7}$ (Fundamental Theorem of Identity System). +tex. - $\mathbf{Theorem\ 3.8}$ (Strict Identity System). An identity system + $\mathbf{Definition\ 3.8}$ (Strict Identity System). An identity system over type $A$ and universe of pretypes $V_i$ is called strict identity system ($=$), which respects UIP. +tex. - $\mathbf{Theorem\ 3.9}$ (Homotopy Identity System). An identity system + $\mathbf{Definition\ 3.9}$ (Homotopy Identity System). An identity system over type $A$ and universe of homotopy types $U_i$ is called homotopy identity system ($\equiv$), which models discrete infinity groupoid.