From cb0841c727f53fb3c24c5c5df91e18a05d274042 Mon Sep 17 00:00:00 2001 From: 5HT Date: Sun, 29 Oct 2023 21:42:54 +0200 Subject: [PATCH] intro --- intro/index.html | 36 ++++++++++++++++++------------------ intro/index.pug | 36 ++++++++++++++++++------------------ 2 files changed, 36 insertions(+), 36 deletions(-) diff --git a/intro/index.html b/intro/index.html index cbc6b988..944f32ab 100644 --- a/intro/index.html +++ b/intro/index.html @@ -56,30 +56,30 @@ дорівнюють між собою, отже простір шляхів утворює багатовимірну структуру інфініті-групоїда. -

isProp (A : U) : U := Π (a b : A), - Path A a b +

def isProp (A : U) : U + := Π (a b : A), Path A a b -isSet (A : U) : U := Π (a b : A) - (a0 b0 : Path A a b), +def isSet (A : U) : U + := Π (a b : A) (a0 b0 : Path A a b), Path (Path A a b) a0 b0 -isGroupoid (A : U) : U +def isGroupoid (A : U) : U := Π (a b : A) (x y : Path A a b) (i j : Path (Path A a b) x y), Path (Path (Path A a b) x y) i j

Групоїдна інтерпретація теорії типів ставить питання про існування мови, -в якій можна довести механічно всі всластивості категорного визначення групоїда.

CatGroupoid (X : U) (G : isGroupoid X) - : isCatGroupoid (PathCat X) - := ( idp X, - comp-Path X, - G, - sym X, - comp-inv-Path⁻¹ X, - comp-inv-Path X, - comp-Path-left X, - comp-Path-right X, - comp-Path-assoc X, - star - )

За цей час були перепробувані глобулярні та сімліціальні моделі, але +в якій можна довести механічно всі всластивості категорного визначення групоїда.

def CatGroupoid (X : U) (G : isGroupoid X) + : isCatGroupoid (PathCat X) + := ( idp X, + comp-Path X, + G, + sym X, + comp-inv-Path⁻¹ X, + comp-inv-Path X, + comp-Path-left X, + comp-Path-right X, + comp-Path-assoc X, + ★ + )

За цей час були перепробувані глобулярні та сімліціальні моделі, але аксіома унівалентності конструктивно валідується тільки в кубічних множинах, на рівні теорії типів це відбувається в Кан-операціях та .


˙

[1]. Pelayo, Warren. Homotopy type theory and Voevodsky's univalent foundations. 2012. diff --git a/intro/index.pug b/intro/index.pug index 8298fc0a..5252c7d4 100644 --- a/intro/index.pug +++ b/intro/index.pug @@ -92,14 +92,14 @@ block content інфініті-групоїда. +code. - isProp (A : U) : U := Π (a b : A), - Path A a b + def isProp (A : U) : U + := Π (a b : A), Path A a b - isSet (A : U) : U := Π (a b : A) - (a0 b0 : Path A a b), + def isSet (A : U) : U + := Π (a b : A) (a0 b0 : Path A a b), Path (Path A a b) a0 b0 - isGroupoid (A : U) : U + def isGroupoid (A : U) : U := Π (a b : A) (x y : Path A a b) (i j : Path (Path A a b) x y), Path (Path (Path A a b) x y) i j @@ -108,19 +108,19 @@ block content Групоїдна інтерпретація теорії типів ставить питання про існування мови, в якій можна довести механічно всі всластивості категорного визначення групоїда. +code. - CatGroupoid (X : U) (G : isGroupoid X) - : isCatGroupoid (PathCat X) - := ( idp X, - comp-Path X, - G, - sym X, - comp-inv-Path⁻¹ X, - comp-inv-Path X, - comp-Path-left X, - comp-Path-right X, - comp-Path-assoc X, - star - ) + def CatGroupoid (X : U) (G : isGroupoid X) + : isCatGroupoid (PathCat X) + := ( idp X, + comp-Path X, + G, + sym X, + comp-inv-Path⁻¹ X, + comp-inv-Path X, + comp-Path-left X, + comp-Path-right X, + comp-Path-assoc X, + ★ + ) +tex. За цей час були перепробувані глобулярні та сімліціальні моделі, але аксіома унівалентності конструктивно валідується тільки в кубічних множинах,