From d399617f54cd3a876b06033768b00dec8ef899be Mon Sep 17 00:00:00 2001 From: 5HT Date: Mon, 23 Oct 2023 15:11:57 +0300 Subject: [PATCH] J-equiv --- foundations/univalent/equiv/index.html | 18 +++++++++++------- foundations/univalent/equiv/index.pug | 22 +++++++++++++--------- lib/foundations/univalent/equiv.anders | 6 +++--- 3 files changed, 27 insertions(+), 19 deletions(-) diff --git a/foundations/univalent/equiv/index.html b/foundations/univalent/equiv/index.html index 76069510..0c29f09b 100644 --- a/foundations/univalent/equiv/index.html +++ b/foundations/univalent/equiv/index.html @@ -40,17 +40,21 @@ def idEquiv (A : U) : equiv A A := (\(a:A) -> a, isContrSingl A)

Elimination

(Fiberwise Induction Principle). -For any -and it's evidence at -there is a function . HoTT 5.8.5

def ind-Equiv (A B: U) - (C: Π (A B: U), equiv A B → U) - (d: C A A (idEquiv A)) - : (p: equiv A B) -> C A B p

Computation

(Fiberwise Computation of Induction Principle).

def compute-Equiv (A : U) +For any +and it's evidence at +there is a function . HoTT 5.8.5

def J-equiv (A B: U) + (P: Π (A B: U), equiv A B → U) + (d: P B B (idEquiv B)) + : Π (e: equiv A B), P A B e + := λ (e: equiv A B), + subst (single B) (\ (z: single B), P z.1 B z.2) + (B,idEquiv B) (A,e) + (contrSinglEquiv A B e) d

Computation

(Fiberwise Computation of Induction Principle).

def compute-Equiv (A : U) (C : Π (A B: U), equiv A B → U) (d: C A A (idEquiv A)) : Path (C A A (idEquiv A)) d (ind-Equiv A A C d (idEquiv A))

UNIVALENCE

The notion of univalence represents -transport between fibrational equivalence +transport between fibrational equivalence as contractability of fibers and homotopical multi-dimentional heterogeneous path equality (HoTT 2.10):

The type diff --git a/foundations/univalent/equiv/index.pug b/foundations/univalent/equiv/index.pug index 34ec3c78..79295cb6 100644 --- a/foundations/univalent/equiv/index.pug +++ b/foundations/univalent/equiv/index.pug @@ -85,24 +85,28 @@ block content h2 Elimination +tex. $\mathbf{Definition}$ (Fiberwise Induction Principle). - For any $C : A \rightarrow B \rightarrow A \simeq B \rightarrow U$ - and it's evidence $d$ at $(A,A,\mathrm{id_\simeq}(A))$ + For any $P : A \rightarrow B \rightarrow A \simeq B \rightarrow U$ + and it's evidence $d$ at $(B,B,\mathrm{id_\simeq}(B))$ there is a function $\mathbf{ind}_\simeq$. HoTT 5.8.5 +tex(true). $$ - \mathbf{ind}_\simeq(C,d) : (p: A\simeq B) \rightarrow C(A,B,p). + \mathbf{ind}_\simeq(P,d) : (p: A\simeq B) \rightarrow P(A,B,p). $$ +code. - def ind-Equiv (A B: U) - (C: Π (A B: U), equiv A B → U) - (d: C A A (idEquiv A)) - : (p: equiv A B) -> C A B p + def J-equiv (A B: U) + (P: Π (A B: U), equiv A B → U) + (d: P B B (idEquiv B)) + : Π (e: equiv A B), P A B e + := λ (e: equiv A B), + subst (single B) (\ (z: single B), P z.1 B z.2) + (B,idEquiv B) (A,e) + (contrSinglEquiv A B e) d br. h2 Computation +tex. $\mathbf{Definition}$ (Fiberwise Computation of Induction Principle). +code. - def compute-Equiv (A : U) + def compute-Equiv (A : U) (C : Π (A B: U), equiv A B → U) (d: C A A (idEquiv A)) : Path (C A A (idEquiv A)) d @@ -113,7 +117,7 @@ block content h1 UNIVALENCE +tex. The notion of univalence represents - transport between fibrational equivalence + transport between fibrational equivalence as contractability of fibers and homotopical multi-dimentional heterogeneous path equality (HoTT 2.10): diff --git a/lib/foundations/univalent/equiv.anders b/lib/foundations/univalent/equiv.anders index da92cdf0..a22432a9 100644 --- a/lib/foundations/univalent/equiv.anders +++ b/lib/foundations/univalent/equiv.anders @@ -54,9 +54,9 @@ def isContr→isProp (A: U) (w: isContr A) (a b : A) : Path A a b def contrSinglEquiv (A B : U) (e : equiv A B) : Path (single B) (B,idEquiv B) (A,e) := isContr→isProp (single B) (EquivIsContr B) (B,idEquiv B) (A,e) -def J-equiv (A B: U) (P: Π (A: U), equiv A B → U) (r: P B (idEquiv B)) - : Π (e: equiv A B), P A e - := λ (e: equiv A B), subst (single B) (\ (z: single B), P z.1 z.2) +def J-equiv (A B: U) (P: Π (A B: U), equiv A B → U) (r: P B B (idEquiv B)) + : Π (e: equiv A B), P A B e + := λ (e: equiv A B), subst (single B) (\ (z: single B), P z.1 B z.2) (B,idEquiv B) (A,e) (contrSinglEquiv A B e) r --- [Pitts] 2016