From 40327246954332f40cd82c48d102bf4257ad719e Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 8 Dec 2023 17:00:21 +0300 Subject: [PATCH] Format recId.rzk.md --- docs/docs/examples/recId.rzk.md | 189 ++++++++++++++++++-------------- 1 file changed, 106 insertions(+), 83 deletions(-) diff --git a/docs/docs/examples/recId.rzk.md b/docs/docs/examples/recId.rzk.md index 9637578c..94ffcff8 100644 --- a/docs/docs/examples/recId.rzk.md +++ b/docs/docs/examples/recId.rzk.md @@ -13,40 +13,50 @@ We begin by introducing common HoTT definitions: #lang rzk-1 -- A is contractible there exists x : A such that for any y : A we have x = y. -#define iscontr (A : U) : U - := Σ (a : A), (x : A) → a =_{A} x +#define iscontr (A : U) + : U + := Σ ( a : A) , (x : A) → a =_{A} x -- A is a proposition if for any x, y : A we have x = y -#define isaprop (A : U) : U - := (x : A) → (y : A) → x =_{A} y +#define isaprop (A : U) + : U + := ( x : A) → (y : A) → x =_{A} y -- A is a set if for any x, y : A the type x =_{A} y is a proposition -#define isaset (A : U) : U - := (x : A) → (y : A) → isaprop (x =_{A} y) +#define isaset (A : U) + : U + := ( x : A) → (y : A) → isaprop (x =_{A} y) -- Non-dependent product of A and B -#define prod (A : U) (B : U) : U - := Σ (x : A), B +#define prod (A : U) (B : U) + : U + := Σ ( x : A) , B -- A function f : A → B is an equivalence -- if there exists g : B → A -- such that for all x : A we have g (f x) = x -- and for all y : B we have f (g y) = y -#define isweq (A : U) (B : U) (f : A → B) : U - := Σ (g : B → A), prod ((x : A) → g (f x) =_{A} x) ((y : B) → f (g y) =_{B} y) +#define isweq (A : U) (B : U) (f : A → B) + : U + := Σ ( g : B → A) + , prod + ( ( x : A) → g (f x) =_{A} x) + ( ( y : B) → f (g y) =_{B} y) -- Equivalence of types A and B -#define weq (A : U) (B : U) : U - := Σ (f : A → B), isweq A B f +#define weq (A : U) (B : U) + : U + := Σ ( f : A → B) + , isweq A B f -- Transport along a path #define transport - (A : U) - (C : A → U) - (x y : A) - (p : x =_{A} y) - : C x → C y - := \ cx → idJ(A, x, (\z q → C z), cx, y, p) + ( A : U) + ( C : A → U) + ( x y : A) + ( p : x =_{A} y) + : C x → C y + := \ cx → idJ(A , x , (\ z q → C z) , cx , y , p) ``` ## Relative function extensionality @@ -55,26 +65,30 @@ We can now define relative function extensionality. There are several formulatio ```rzk -- [RS17, Axiom 4.6] Relative function extensionality. -#define relfunext : U - := (I : CUBE) - → (ψ : I → TOPE) - → (φ : ψ → TOPE) - → (A : ψ → U) - → ((t : ψ) → iscontr (A t)) - → (a : (t : φ) → A t) - → (t : ψ) → A t [ φ t ↦ a t] +#define relfunext + : U + := ( I : CUBE) + → ( ψ : I → TOPE) + → ( φ : ψ → TOPE) + → ( A : ψ → U) + → ( ( t : ψ) → iscontr (A t)) + → ( a : ( t : φ) → A t) + → ( t : ψ) → A t [ φ t ↦ a t] -- [RS17, Proposition 4.8] A (weaker) formulation of function extensionality. -#define relfunext2 : U - := (I : CUBE) - → (ψ : I → TOPE) - → (φ : ψ → TOPE) - → (A : ψ → U) - → (a : (t : φ) → A t) - → (f : (t : ψ) → A t [ φ t ↦ a t ]) - → (g : (t : ψ) → A t [ φ t ↦ a t ]) - → weq (f = g) - ((t : ψ) → (f t =_{A t} g t) [ φ t ↦ refl ]) +#define relfunext2 + : U + := + ( I : CUBE) + → ( ψ : I → TOPE) + → ( φ : ψ → TOPE) + → ( A : ψ → U) + → ( a : ( t : φ) → A t) + → ( f : (t : ψ) → A t [ φ t ↦ a t ]) + → ( g : ( t : ψ) → A t [ φ t ↦ a t ]) + → weq + ( f = g) + ( ( t : ψ) → (f t =_{A t} g t) [ φ t ↦ refl ]) ``` ## Construction of `recId` @@ -93,14 +107,14 @@ First, we define how to restrict an extension type to a subshape: -- Restrict extension type to a subshape. #define restrict_phi - (a : (t : φ) → A t) - : (t : I | ψ t ∧ φ t) → A t + ( a : ( t : φ) → A t) + : ( t : I | ψ t ∧ φ t) → A t := \ t → a t -- Restrict extension type to a subshape. #define restrict_psi - (a : (t : ψ) → A t) - : (t : I | ψ t ∧ φ t) → A t + ( a : ( t : ψ) → A t) + : ( t : I | ψ t ∧ φ t) → A t := \ t → a t ``` @@ -109,14 +123,16 @@ Then, how to reformulate an `a` (or `b`) as an extension of its restriction: ```rzk -- Reformulate extension type as an extension of a restriction. #define ext-of-restrict_psi - (a : (t : ψ) → A t) - : (t : ψ) → A t [ ψ t ∧ φ t ↦ restrict_psi a t ] + ( a : ( t : ψ) → A t) + : ( t : ψ) + → A t [ ψ t ∧ φ t ↦ restrict_psi a t ] := a -- type is coerced automatically here -- Reformulate extension type as an extension of a restriction. #define ext-of-restrict_phi - (a : (t : φ) → A t) - : (t : φ) → A t [ ψ t ∧ φ t ↦ restrict_phi a t ] + ( a : ( t : φ) → A t) + : ( t : φ) + → A t [ ψ t ∧ φ t ↦ restrict_phi a t ] := a -- type is coerced automatically here ``` @@ -125,17 +141,20 @@ Now, assuming relative function extensionality, we construct a path between rest ```rzk -- Transform extension of an identity into an identity of restrictions. #define restricts-path - (a_psi : (t : ψ) → A t) - (a_phi : (t : φ) → A t) - (e : (t : I | ψ t ∧ φ t) → a_psi t = a_phi t) - : restrict_psi a_psi = restrict_phi a_phi - := (first (second (r I - (\t → ψ t ∧ φ t) - (\t → BOT) - (\t → A t) - (\t → recBOT) - (\t → a_psi t) - (\t → a_phi t)))) e + ( a_psi : (t : ψ) → A t) + ( a_phi : (t : φ) → A t) + : ( e : (t : I | ψ t ∧ φ t) → a_psi t = a_phi t) + → restrict_psi a_psi = restrict_phi a_phi + := + first + ( second + ( r I + ( \ t → ψ t ∧ φ t) + ( \ t → BOT) + ( \ t → A t) + ( \ t → recBOT) + ( \ t → a_psi t) + ( \ t → a_phi t))) ``` Finally, we bring everything together into `recId`: @@ -145,20 +164,22 @@ Finally, we bring everything together into `recId`: -- recOR(ψ, φ, a, b) demands that for ψ ∧ φ we have a == b (definitionally) -- (recId ψ φ a b e) demands that e is the proof that a = b (intensionally) for ψ ∧ φ #define recId uses (r) -- we declare that recId is using r on purpose - (a_psi : (t : ψ) → A t) - (a_phi : (t : φ) → A t) - (e : (t : I | ψ t ∧ φ t) → a_psi t = a_phi t) - : (t : I | ψ t ∨ φ t) → A t - := \t → recOR( - ψ t ↦ transport - ((s : I | ψ s ∧ φ s) → A s) - (\ra → (s : ψ) → A s [ ψ s ∧ φ s ↦ ra s ]) - (restrict_psi a_psi) - (restrict_phi a_phi) - (restricts-path a_psi a_phi e) - (ext-of-restrict_psi a_psi) - t, - φ t ↦ ext-of-restrict_phi a_phi t + ( a_psi : (t : ψ) → A t) + ( a_phi : (t : φ) → A t) + ( e : (t : I | ψ t ∧ φ t) → a_psi t = a_phi t) + : ( t : I | ψ t ∨ φ t) → A t + := \ t → recOR( + ψ t ↦ + transport + ( ( s : I | ψ s ∧ φ s) → A s) + ( \ ra → (s : ψ) → A s [ ψ s ∧ φ s ↦ ra s ]) + ( restrict_psi a_psi) + ( restrict_phi a_phi) + ( restricts-path a_psi a_phi e) + ( ext-of-restrict_psi a_psi) + ( t) + , φ t ↦ + ext-of-restrict_phi a_phi t ) #end construction-of-recId @@ -173,18 +194,20 @@ whenever we can show that they are equal on the intersection of shapes: -- If two extension types are equal along two subshapes, -- then they are also equal along their union. #define id-along-border - (r : relfunext2) - (I : CUBE) - (ψ : I → TOPE) - (φ : I → TOPE) - (A : (t : I | ψ t ∨ φ t) → U) - (a b : (t : I | ψ t ∨ φ t) → A t) - (e_psi : (t : ψ) → a t = b t) - (e_phi : (t : φ) → a t = b t) - (border-is-a-set : (t : I | ψ t ∧ φ t) → isaset (A t)) - : (t : I | ψ t ∨ φ t) → a t = b t - := recId r I ψ φ - (\t → a t = b t) - e_psi e_phi - (\t → border-is-a-set t (a t) (b t) (e_psi t) (e_phi t)) + ( r : relfunext2) + ( I : CUBE) + ( ψ : I → TOPE) + ( φ : I → TOPE) + ( A : (t : I | ψ t ∨ φ t) → U) + ( a b : (t : I | ψ t ∨ φ t) → A t) + ( e_psi : (t : ψ) → a t = b t) + ( e_phi : (t : φ) → a t = b t) + ( border-is-a-set : (t : I | ψ t ∧ φ t) → isaset (A t)) + : ( t : I | ψ t ∨ φ t) → a t = b t + := + recId r I ψ φ + ( \ t → a t = b t) + ( e_psi) + ( e_phi) + ( \ t → border-is-a-set t (a t) (b t) (e_psi t) (e_phi t)) ```