diff --git a/foundations/mltt/pi/index.html b/foundations/mltt/pi/index.html index caecaa68..c200fe1f 100644 --- a/foundations/mltt/pi/index.html +++ b/foundations/mltt/pi/index.html @@ -20,89 +20,103 @@ Lambda constructor defines a new lambda function in the space of dependent functions. it is called lambda abstraction and displayed as or .

-

def lambda (A: U) (B: A → U) (b: Pi A B) : Pi A B := λ (x : A), b x -def lam (A B: U) (f: A → B) : A → B := λ (x : A), f x

When codomain is not dependent on valude from domain the function +

def lambda (A: U) (B: A → U) (b: Pi A B) + : Pi A B := λ (x : A), b x + +def lam (A B: U) (f: A → B) + : A → B := λ (x : A), f x

When codomain is not dependent on valude from domain the function is studied in System F, dependent case in studied in Systen P or Calculus of Construction (CoC). -

Elimination

(-application). +

Elimination

(-Induction Principle). States that +if predicate holds for lambda function +then there is a function from function space to the space of predicate.

def П-ind (A : U) (B : A -> U) + (C : Pi A B → U) + (g: Π (x: Pi A B), C x) + : П (p: Pi A B), C p + := \ (p: Pi A B), g p

(-application). Application reduces the term by using recursive substitution. -

-

def apply (A: U) (B: A → U) (f: Pi A B) (a: A) : B a := f a -def app (A B: U) (f: A → B) (x: A): B := f x -

(Composition). +

+

def apply (A: U) (B: A → U) + (f: Pi A B) (a: A) : B a := f a + +def app (A B: U) (f: A → B) + (x: A): B := f x

(Composition). Composition is using application of appropriate singnatures. -

def ∘ᵀ (α β γ: U) : U := (β → γ) → (α → β) → (α → γ) -def ∘ (α β γ : U) : ∘ᵀ α β γ := λ (g: β → γ) (f: α → β) (x: α), g (f x)

Computation

(Computation ). --rule shows that composition +

def ∘ᵀ (α β γ: U) : U + := (β → γ) → (α → β) → (α → γ) + +def ∘ (α β γ : U) : ∘ᵀ α β γ + := λ (g: β → γ) (f: α → β) (x: α), g (f x)

Computation

(Computation ). +-rule shows that composition could be fused. -

+

def Π-β (A : U) (B : A → U) (a : A) (f : Pi A B) : Path (B a) (apply A B (lambda A B f) a) (f a) - := idp (B a) (f a)

Uniqueness

(Uniqueness ). --rule shows that composition could be fused. -

def Π-η (A : U) (B : A → U) (a : A) (f : Pi A B) + := idp (B a) (f a)

Uniqueness

(Uniqueness ). +-rule shows that composition could be fused. +

def Π-η (A : U) (B : A → U) (a : A) (f : Pi A B) : Path (Pi A B) f (λ (x : A), f x) - := idp (Pi A B) f

THEOREMS

(Functions Preserve Paths). For a function -there is an . This is called -application of to path or congruence property (, for non-dependent case). + := idp (Pi A B) f

THEOREMS

(Functions Preserve Paths). For a function +there is an . This is called +application of to path or congruence property (, for non-dependent case). This property behaves functoriality as if paths are groupoid morphisms and types are objects. -

FiberPi (B: U) (F: B -> U) (y: B) - : Path U (fiber (Sigma B F) B (pi1 B F) y) (F y) -

(Trivial Fiber equals Family of Sets). -Inverse image (fiber) of fiber bundle in point equals . -

(Homotopy Equivalence). If fiber space is set for all base, and -there are two functions and two +

def FiberPi (B: U) (F: B -> U) (y: B) + : Path U (fiber (Sigma B F) B (pi1 B F) y) (F y) +

(Trivial Fiber equals Family of Sets). +Inverse image (fiber) of fiber bundle in point equals . +

(Homotopy Equivalence). If fiber space is set for all base, and +there are two functions and two homotopies between them, then these homotopies are equal. -

setPi (A: U) (B: A -> U) (h: (x: A) -> isSet (B x)) (f g: Pi A B) - (p q: Path (Pi A B) f g) : Path (Path (Pi A B) f g) p q -

(HomSet). If codomain is set then space of sections is a set. -

setFun (A B : U) (_: isSet B) : isSet (A -> B) -

(Contractability). If domain and codomain is contractible then +

def setPi (A: U) (B: A -> U) + (h: П (x: A), isSet (B x)) (f g: Pi A B) + (p q: Path (Pi A B) f g) + : Path (Path (Pi A B) f g) p q

(HomSet). If codomain is set then space of sections is a set. +

def setFun (A B : U) (_: isSet B) : isSet (A -> B)

(Contractability). If domain and codomain is contractible then the space of sections is contractible. -

piIsContr (A: U) (B: A -> U) (u: isContr A) - (q: (x: A) -> isContr (B x)) - : isContr (Pi A B)
pathPi (A:U) (B:A->U) (f g : Pi A B) - : Path U (Path (Pi A B) f g) - ((x:A) -> Path (B x) (f x) (g x))

Interpretations

Homotopy Theory

Geometrically, П-type is a space of sections, +

def piIsContr (A: U) (B: A -> U) (u: isContr A) + (q: П (x: A), isContr (B x)) + : isContr (Pi A B)
def pathPi (A: U) (B: A -> U) (f g : Pi A B) + : Path U (Path (Pi A B) f g) + ((x:A) -> Path (B x) (f x) (g x))

Interpretations

Homotopy Theory

Geometrically, П-type is a space of sections, while the dependent codomain is a space of fibrations. Lambda functions are sections or points in these spaces, while the function result is a fibration. -

(Fiber). The fiber of the map in a point -is all points such that . -

(Fiber Bundle). -The fiber bundle on a -total space with fiber layer and base is a -structure where is a surjective +

(Fiber). The fiber of the map in a point +is all points such that . +

(Fiber Bundle). +The fiber bundle on a +total space with fiber layer and base is a +structure where is a surjective map with following property: -for any point exists a neighborhood for which a -homeomorphism +for any point exists a neighborhood for which a +homeomorphism making the following diagram commute. -

-

(Cartesian Product of Family over B). Is a set -of sections of the bundle with elimination map . +

+

(Cartesian Product of Family over B). Is a set +of sections of the bundle with elimination map . such that -

-

is a product projection, so , are moriphisms -of slice category . The universal mapping property of : -for all and morphism in exists -unique map such that everything commute. So a category +

+

is a product projection, so , are moriphisms +of slice category . The universal mapping property of : +for all and morphism in exists +unique map such that everything commute. So a category with all dependent products is necessarily a category with all pullbacks. -

(Trivial Fiber Bundle). -When total space is cartesian product -and then such bundle is called trivial . -

Category Theory

Categorically, -types arise in locally cartesian closed categories. -In this case -type represents the cartesian family of sets, +

(Trivial Fiber Bundle). +When total space is cartesian product +and then such bundle is called trivial . +

Category Theory

Categorically, -types arise in locally cartesian closed categories. +In this case -type represents the cartesian family of sets, generalizing the cartesian product of sets or dependent product. -

(Section). A section of morphism -in some category is the morphism such that - equals the identity morphism on B. -

(Dependent Product). The dependent product along -morphism in category is the right -adjoint of the base change functor. -

(Space of Sections). Let be -a -topos, and let a bundle in -, object in the slice topos. Then the space of sections +

(Section). A section of morphism +in some category is the morphism such that + equals the identity morphism on B. +

(Dependent Product). The dependent product along +morphism in category is the right +adjoint of the base change functor. +

(Space of Sections). Let be +a -topos, and let a bundle in +, object in the slice topos. Then the space of sections of this bundle is the Dependent Product: -

+

\ No newline at end of file diff --git a/foundations/mltt/pi/index.pug b/foundations/mltt/pi/index.pug index 8d0c07c2..43636b03 100644 --- a/foundations/mltt/pi/index.pug +++ b/foundations/mltt/pi/index.pug @@ -65,8 +65,11 @@ block content $$ +code. - def lambda (A: U) (B: A → U) (b: Pi A B) : Pi A B := λ (x : A), b x - def lam (A B: U) (f: A → B) : A → B := λ (x : A), f x + def lambda (A: U) (B: A → U) (b: Pi A B) + : Pi A B := λ (x : A), b x + + def lam (A B: U) (f: A → B) + : A → B := λ (x : A), f x br. +tex. @@ -77,7 +80,19 @@ block content h2 Elimination +tex. - $\mathbf{Definition\ 1.3}$ ($\lambda$-application). + $\mathbf{Definition\ 1.3}$ ($\Pi$-Induction Principle). States that + if predicate holds for lambda function + then there is a function from function space to the space of predicate. + +code. + def П-ind (A : U) (B : A -> U) + (C : Pi A B → U) + (g: Π (x: Pi A B), C x) + : П (p: Pi A B), C p + := \ (p: Pi A B), g p + br. + + +tex. + $\mathbf{Definition\ 1.3.1}$ ($\lambda$-application). Application reduces the term by using recursive substitution. +tex(true). @@ -86,16 +101,23 @@ block content $$ +code. - def apply (A: U) (B: A → U) (f: Pi A B) (a: A) : B a := f a - def app (A B: U) (f: A → B) (x: A): B := f x + def apply (A: U) (B: A → U) + (f: Pi A B) (a: A) : B a := f a + + def app (A B: U) (f: A → B) + (x: A): B := f x + br. +tex. - $\mathbf{Definition\ 1.3.1}$ (Composition). + $\mathbf{Definition\ 1.3.2}$ (Composition). Composition is using application of appropriate singnatures. +code. - def ∘ᵀ (α β γ: U) : U := (β → γ) → (α → β) → (α → γ) - def ∘ (α β γ : U) : ∘ᵀ α β γ := λ (g: β → γ) (f: α → β) (x: α), g (f x) + def ∘ᵀ (α β γ: U) : U + := (β → γ) → (α → β) → (α → γ) + + def ∘ (α β γ : U) : ∘ᵀ α β γ + := λ (g: β → γ) (f: α → β) (x: α), g (f x) br. h2 Computation @@ -141,8 +163,8 @@ block content This property behaves functoriality as if paths are groupoid morphisms and types are objects. +code. - FiberPi (B: U) (F: B -> U) (y: B) - : Path U (fiber (Sigma B F) B (pi1 B F) y) (F y) + def FiberPi (B: U) (F: B -> U) (y: B) + : Path U (fiber (Sigma B F) B (pi1 B F) y) (F y) +tex. $\mathbf{Theorem\ 1.7}$ (Trivial Fiber equals Family of Sets). @@ -154,29 +176,33 @@ block content homotopies between them, then these homotopies are equal. +code. - setPi (A: U) (B: A -> U) (h: (x: A) -> isSet (B x)) (f g: Pi A B) - (p q: Path (Pi A B) f g) : Path (Path (Pi A B) f g) p q + def setPi (A: U) (B: A -> U) + (h: П (x: A), isSet (B x)) (f g: Pi A B) + (p q: Path (Pi A B) f g) + : Path (Path (Pi A B) f g) p q + br. +tex. $\mathbf{Theorem\ 1.9}$ (HomSet). If codomain is set then space of sections is a set. +code. - setFun (A B : U) (_: isSet B) : isSet (A -> B) + def setFun (A B : U) (_: isSet B) : isSet (A -> B) + br. +tex. $\mathbf{Theorem\ 1.10}$ (Contractability). If domain and codomain is contractible then the space of sections is contractible. +code. - piIsContr (A: U) (B: A -> U) (u: isContr A) - (q: (x: A) -> isContr (B x)) - : isContr (Pi A B) + def piIsContr (A: U) (B: A -> U) (u: isContr A) + (q: П (x: A), isContr (B x)) + : isContr (Pi A B) br +code. - pathPi (A:U) (B:A->U) (f g : Pi A B) - : Path U (Path (Pi A B) f g) - ((x:A) -> Path (B x) (f x) (g x)) + def pathPi (A: U) (B: A -> U) (f g : Pi A B) + : Path U (Path (Pi A B) f g) + ((x:A) -> Path (B x) (f x) (g x)) br h1 Interpretations diff --git a/foundations/mltt/sigma/index.html b/foundations/mltt/sigma/index.html index aabe22d8..735f6505 100644 --- a/foundations/mltt/sigma/index.html +++ b/foundations/mltt/sigma/index.html @@ -7,56 +7,56 @@ use[data-c]{stroke-width:3px} SIGMA

CONTEXT SPACES

-type is a space that contains dependent pairs +SIGMA

CONTEXT SPACES

-type is a space that contains dependent pairs where type of the second element depends on the value of the first element. As only one point of fiber domain -present in every defined pair, -type is also a dependent sum, +present in every defined pair, -type is also a dependent sum, where fiber base is a disjoint union.

Spaces of dependent pairs are using in type theory to model cartesian products, disjoint sums, fiber bundles, vector spaces, telescopes, lenses, contexts, objects, algebras, ∃-type, etc. -

Formation

(-Formation, Dependent Sum). The dependent sum -type is indexed over type in the sense of coproduct or disjoint union, -where only one fiber codomain is present in pair.

+

Formation

(-Formation, Dependent Sum). The dependent sum +type is indexed over type in the sense of coproduct or disjoint union, +where only one fiber codomain is present in pair.

def Sigma (A: U) (B: A → U) : U - := Σ (x: A), B(x)

Introduction

(Dependent Pair). The dependent pair -constructor is a way to create indexed pair over type -in the sense of coproduct or disjoint union.

def pair (A: U) (B: A → U) (a: A) (b: B a) - : Sigma A B := (a, b)

Elimination

(Dependent Projections). The dependent projections - and - are pair deconstructors.

def pr₁ (A: U) (B: A → U) (x: Sigma A B) + := Σ (x: A), B(x)

Introduction

(Dependent Pair). The dependent pair +constructor is a way to create indexed pair over type +in the sense of coproduct or disjoint union.

def pair (A: U) (B: A → U) (a: A) (b: B a) + : Sigma A B := (a, b)

Elimination

(Dependent Projections). The dependent projections + and + are pair deconstructors.

def pr₁ (A: U) (B: A → U) (x: Sigma A B) : A := x.1 def pr₂ (A: U) (B: A → U) (x: Sigma A B) - : B (pr₁ A B x) := x.2

If you want to access deep sigma a series of -accessors should be applied followed by . -

(-Induction Principle). States that + : B (pr₁ A B x) := x.2

If you want to access deep sigma a series of +accessors should be applied followed by . +

(-Induction Principle). States that if predicate holds for two projections then predicate holds for total space.

def Σ-ind (A : U) (B : A -> U) (C : Π (s: Σ (x: A), B x), U) (g: Π (x: A) (y: B x), C (x,y)) - (p: Σ (x: A), B x) : C p := g p.1 p.2

Computation

(-Computation). + (p: Σ (x: A), B x) : C p := g p.1 p.2

Computation

(-Computation).

def Σ-β₁ (A : U) (B : A → U) (a : A) (b : B a) : Path A a (pr₁ A B (a ,b)) := idp A a
def Σ-β₂ (A : U) (B : A → U) (a : A) (b : B a) - : Path (B a) b (pr₂ A B (a, b)) := idp (B a) b

Uniqueness

(-Uniqueness).

def Σ-η (A : U) (B : A → U) (p : Sigma A B) + : Path (B a) b (pr₂ A B (a, b)) := idp (B a) b

Uniqueness

(-Uniqueness).

def Σ-η (A : U) (B : A → U) (p : Sigma A B) : Path (Sigma A B) p (pr₁ A B p, pr₂ A B p) := idp (Sigma A B) p -

Theorems

(Axiom of Choice). If for all there is -such that , then there is a function such -that for all there is a witness of . +

Theorems

(Axiom of Choice). If for all there is +such that , then there is a function such +that for all there is a witness of .

def ac (A B: U) (R: A -> B -> U) (g: Π (x: A), Σ (y: B), R x y) : Σ (f: A -> B), Π (x: A), R x (f x) := (\(i:A),(g i).1,\(j:A),(g j).2) -

(Total). If fiber over base implies another fiber +

(Total). If fiber over base implies another fiber over the same base then we can construct total space of section over that base with another fiber.

def total (A:U) (B C : A -> U) (f : Π (x:A), B x -> C x) (w: Σ(x: A), B x) : Σ (x: A), C x := (w.1,f (w.1) (w.2)) -

(Path Between Sigmas). Path between -two sigmas could be decomposed to -sigma of two paths and . +

(Path Between Sigmas). Path between +two sigmas could be decomposed to +sigma of two paths and .

def funDepTr (A: U) (P: A -> U) (a0 a1: A) (p: PathP (<_>A) a0 a1) (u0: P a0) (u1: P a1) : PathP (<_>U) (PathP (<i> P (p @ i)) u0 u1) @@ -72,10 +72,10 @@ (λ(k:I),[]) (transp (<i> P (p @ i)) 0 t.2)) u.2) := funDepTr A P t.1 u.1 p t.2 u.2 -

(Propositions). If codomain -of dependent the function -is a mere proposition and for two sigmas there is -a path then the path between second components +

(Propositions). If codomain +of dependent the function +is a mere proposition and for two sigmas there is +a path then the path between second components is a mere proposition too. Same if codomain is set.

corSigProp (A:U) (B:A-> U) (pB: (x:A) -> isProp (B x)) @@ -86,7 +86,7 @@ (sB: (x:A) -> isSet (B x)) (t u: Sigma A B) (p: Path A t.1 u.1): isProp (PathP (<i>B (p@i)) t.2 u.2) -

(Contractability). If first and second component of sigma +

(Contractability). If first and second component of sigma are contractible then the total space of sigma is contractible.

sigmaIsContr (A: U) (B: A -> U) (u: isContr A) (q: (x: A) -> isContr (B x)) diff --git a/foundations/modal/infinitesimal/index.html b/foundations/modal/infinitesimal/index.html index d3ad2f3e..784afd69 100644 --- a/foundations/modal/infinitesimal/index.html +++ b/foundations/modal/infinitesimal/index.html @@ -7,13 +7,13 @@ use[data-c]{stroke-width:3px} INFINITESIMAL

INFINITESIMAL MODALITY

(Infinitesimal Shape Modality or de Rham stack). The two maps - and +INFINITESIMAL

INFINITESIMAL MODALITY

(Infinitesimal Shape Modality or de Rham stack). The two maps + and are called shape modality if -i) is an equivalence, the type is then called coreduced.; ii) -identity types of coreduced types are coreduced; iii) if -is a dependent type such that for all the type is coreduced, -then we can define a section of by induction. The is called de Rham space. +i) is an equivalence, the type is then called coreduced.; ii) +identity types of coreduced types are coreduced; iii) if +is a dependent type such that for all the type is coreduced, +then we can define a section of by induction. The is called de Rham space.

def ι (A : U) (a : A) : ℑ A := ℑ-unit a def is-coreduced (A : U) : U := isEquiv A (ℑ A) (ι A) @@ -28,11 +28,11 @@ def ℑ-ind (A : U) (B : ℑ A → U) (c : Π (a : ℑ A), is-coreduced (B a)) (f : Π (a : A), B (ι A a)) (a : ℑ A) : B a := -(c a (ind-ℑ A B (λ (x : A), ι (B (ι A x)) (f x)) a)).1.1

ÉTALE MAP

(Étale map). A map is formally étale +(c a (ind-ℑ A B (λ (x : A), ι (B (ι A x)) (f x)) a)).1.1

ÉTALE MAP

(Étale map). A map is formally étale if its naturality square is a pullback: - + with induced naturality equation: - +

def ℑ-app (A B : U) (f : A → B) : ℑ A → ℑ B := ℑ-rec A (ℑ B) (ℑ-coreduced B) (∘ A B (ℑ B) (ι B) f) @@ -43,54 +43,54 @@ isPullbackSq A (ℑ A) B (ℑ B) (ℑ-app A B f) (ι B) (ι A) f (λ (a : A), <_> ℑ-unit (f a))
def ÉtaleMap (A B : U) : U := Σ (f : A → B), isÉtaleMap A B f -

(Infinitesimal Close). -Let , then we have a type which could be +

(Infinitesimal Close). +Let , then we have a type which could be read x is infinitesimally close to y and is given as: - -

def ~ (X : U) (a x′ : X) : U := Path (ℑ X) (ι X a) (ι X x′)

FORMAL DISK BUNDLE

(Formal Disk). -Let be a type and . The type + +

def ~ (X : U) (a x′ : X) : U := Path (ℑ X) (ι X a) (ι X x′)

FORMAL DISK BUNDLE

(Formal Disk). +Let be a type and . The type defined below in three equivalent ways is called the formal disk at a: -i) is the sum of all point infinitesimal close to a; - -ii) is a fiber of at ; -iii) is defined as a pullback square: - +i) is the sum of all point infinitesimal close to a; + +ii) is a fiber of at ; +iii) is defined as a pullback square: +

def 𝔻 (X : U) (a : X) : U := Σ (x′ : X), ~ X a x′ -

(Differential). -If is a type, there is a dependent function - +

(Differential). +If is a type, there is a dependent function + defined as - +

def inf-prox-ap (X Y : U) (f : X → Y) (x x′ : X) (p : ~ X x x′) : ~ Y (f x) (f x′) := <i> ℑ-app X Y f (p @ i) def d (X Y : U) (f : X → Y) (x : X) (ε : 𝔻 X x) : 𝔻 Y (f x) := (f ε.1, inf-prox-ap X Y f x ε.1 ε.2) -

(Formal Disk Bundle). -Let be a type. The type +

(Formal Disk Bundle). +Let be a type. The type defined in one of the equivalent ways below -is called the formal disk bundle of : -i) is the sum over all formal disks in A: - -ii) is defined by pullback square: - +is called the formal disk bundle of : +i) is the sum over all formal disks in A: + +ii) is defined by pullback square: +

def T∞ (A : U) : U := Σ (a : A), 𝔻 A a -

(Hennion). -The tangent complex of a derived algebraic stack +

(Hennion). +The tangent complex of a derived algebraic stack is equivalently the (sheaf of modules of) sections -of the formal neighbourhood of the diagonal of . -We may think of as being the tangent complex of . -

(Kock). The infinitesimal disk bundle construction is +of the formal neighbourhood of the diagonal of . +We may think of as being the tangent complex of . +

(Kock). The infinitesimal disk bundle construction is left adjoint to the jet comonad: - -

(Induced map). -For a map there is an -induced map on the formal disk bundles, given as -

MANIFOLDS

(Homogeneous structure). -A type is homogeneous, if there are terms of the following types: -i) ; ii) ; iii) . + +

(Induced map). +For a map there is an +induced map on the formal disk bundles, given as +

MANIFOLDS

(Homogeneous structure). +A type is homogeneous, if there are terms of the following types: +i) ; ii) ; iii) .

def is-homogeneous (A : U) := Σ (e : A) (t : A → equiv A A), Π (x : A), Path A ((t x).1 e) x

LITERATURE

[1]. Felix Cherubini diff --git a/foundations/modal/localization/index.html b/foundations/modal/localization/index.html index d8f57e05..cef52818 100644 --- a/foundations/modal/localization/index.html +++ b/foundations/modal/localization/index.html @@ -7,13 +7,13 @@ use[data-c]{stroke-width:3px} LOCALIZATION

LOCALIZATION MODALITY

Formation

(Localization Modality). -Given a family of maps a type -is -local if the precomposition map -is an equivalence for all , and the -localization is the -universal -local type admitting a map from .

. -

Introduction

(Localization Modality Constructors). The localization -modality is generated by the following higher inductive composition structure:


data Localize (A X: U) (S T: A -> U) (F : (x:A) -> S x -> T x) +LOCALIZATION

LOCALIZATION MODALITY

Formation

(Localization Modality). +Given a family of maps a type +is -local if the precomposition map +is an equivalence for all , and the -localization is the +universal -local type admitting a map from .

. +

Introduction

(Localization Modality Constructors). The localization +modality is generated by the following higher inductive composition structure:


data Localize (A X: U) (S T: A -> U) (F : (x:A) -> S x -> T x) = center (x: X) | ext (a: A) (f: S a -> Localize A X S T F) (t: T a) | isExt (a: A) (f: S a -> Localize A X S T F) (s: S a) <i> @@ -24,11 +24,11 @@ | isExtEq (a: A) (g h : T a -> Localize A X S T F) (p: (s : S a) -> Path (Localize A X S T F) (g (F a s)) (h (F a s))) (s : S a) <i> [ (i=0) -> extEq {Localize A X S T F} a g h p (F a s) @ i, - (i=>1) -> p s @ i]

(Accessible Modality). Accessible modality + (i=>1) -> p s @ i]

(Accessible Modality). Accessible modality is a modality than can be generated by localization. Examples: --truncations, nullification, open, closed. -

Elimination

(Localization Induction Principle). -For any with :

there is a section such that .

LocalizationInd (A X : U) (S T : A -> U) (F : (x:A) -> S x -> T x) +-truncations, nullification, open, closed. +

Elimination

(Localization Induction Principle). +For any with :

there is a section such that .

LocalizationInd (A X : U) (S T : A -> U) (F : (x:A) -> S x -> T x) (P : Localize A X S T F -> U) (n : (x : X) -> P (center x)) (r : (a : A) (f: S a -> Localize A X S T F) diff --git a/foundations/modal/modality/index.html b/foundations/modal/modality/index.html index 5427379a..5372be8e 100644 --- a/foundations/modal/modality/index.html +++ b/foundations/modal/modality/index.html @@ -7,11 +7,11 @@ use[data-c]{stroke-width:3px} INFINITESIMAL

MODAL SPACES

(Modality). -

(Synonyms). The followin are equivalent: -1) Higher modalities; 2) -closed reflective subuniverses; +MODALITY

MODAL SPACES

(Modality). +

(Synonyms). The followin are equivalent: +1) Higher modalities; 2) -closed reflective subuniverses; 3) Stable orthogonal factorization systems. -

(Modality System). +

(Modality System).

Modality : U = (isModal : U -> U) * (isPropIsModal : (A : U) -> isProp (isModal A)) diff --git a/foundations/univalent/equiv/index.html b/foundations/univalent/equiv/index.html index 34ccf8ba..76069510 100644 --- a/foundations/univalent/equiv/index.html +++ b/foundations/univalent/equiv/index.html @@ -7,12 +7,12 @@ use[data-c]{stroke-width:3px} EQUIV

EQUIVALENCE

Formation

(Fiberwise Equivalence). -Fiberwise equivalence or -of function -represents internal equality of types and -in the universe as contractible fibers of -over base .

def isContr (A: U) : U +EQUIV

EQUIVALENCE

Formation

(Fiberwise Equivalence). +Fiberwise equivalence or +of function +represents internal equality of types and +in the universe as contractible fibers of +over base .

def isContr (A: U) : U := Σ (x: A), Π (y: A), Path A x y def fiber (A B : U) (f: A → B) (y : B): U @@ -22,10 +22,10 @@ := Π (y : B), isContr (fiber A B f y) def equiv (A B : U) : U - := Σ (f : A → B), isEquiv A B f

Introduction

(Fiberwise Reflection). -There is a fiberwise instance -of that is derived -as :

def singl (A: U) (a: A): U + := Σ (f : A → B), isEquiv A B f

Introduction

(Fiberwise Reflection). +There is a fiberwise instance +of that is derived +as :

def singl (A: U) (a: A): U := Σ (x: A), Path A a x def contr (A : U) (a b : A) (p : Path A a b) @@ -39,13 +39,13 @@ 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) + := (\(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) + : (p: equiv A B) -> C A B p

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 @@ -53,21 +53,21 @@ transport between fibrational equivalence as contractability of fibers and homotopical multi-dimentional -heterogeneous path equality (HoTT 2.10):

The type -is called type. Univalence is packed -as isomorphism where intro is obtained by type -and elim -is obtained by transport from constant map.

Formation

(Univalence Formation).

def univ-formation (A B : U) - := equiv A B → PathP (<_> U) A B

Introduction

(Univalence Intro).

def univ-intro (A B : U) +heterogeneous path equality (HoTT 2.10):

The type +is called type. Univalence is packed +as isomorphism where intro is obtained by type +and elim +is obtained by transport from constant map.

Formation

(Univalence Formation).

def univ-formation (A B : U) + := equiv A B → PathP (<_> U) A B

Introduction

(Univalence Intro).

def univ-intro (A B : U) : univ-formation A B := λ (e : equiv A B), <i> Glue B (∂ i) [ (i = 0) → (A, e), - (i = 1) → (B, idEquiv B) ]

Elimination

(Univalence Elimination).

def univ-elim (A B : U) + (i = 1) → (B, idEquiv B) ]

Elimination

(Univalence Elimination).

def univ-elim (A B : U) (p : PathP (<_> U) A B) : equiv A B := transp (<i> equiv A (p @ i)) - 0 (idEquiv A)

Computation

(Univalence Computation).

Uniqueness

(Univalence Uniqueness).

def univ-computation (A B : U) + 0 (idEquiv A)

Computation

(Univalence Computation).

Uniqueness

(Univalence Uniqueness).

def univ-computation (A B : U) (p : PathP (<_> U) A B) : PathP (<_> PathP (<_> U) A B) (univ-intro A B (univ-elim A B p)) p diff --git a/foundations/univalent/funext/index.html b/foundations/univalent/funext/index.html index 92a3d4fb..91a16403 100644 --- a/foundations/univalent/funext/index.html +++ b/foundations/univalent/funext/index.html @@ -8,32 +8,32 @@ FUNEXT

FUNCTION EXTENSIONALITY

Here is presented two packages of homotopy, denoted as -, between two -functions from function space. +, between two +functions from function space. The first is isomorphism structure with - -as encode-decode functions and + +as encode-decode functions and as section-retract properties; and the second is identity -system structure with as reflection -and as induction principle. -

Formation

(Homotopy Formation). Homotopy is -the equality of functions .

.

def ~ (A B: U) (f g: A -> B) - : U := Path (A -> B) f g

Introduction

(Homotopy Introduction, Function Extensionality).

def funext (A B: U) (f g: A → B) +system structure with as reflection +and as induction principle. +

Formation

(Homotopy Formation). Homotopy is +the equality of functions .

.

def ~ (A B: U) (f g: A -> B) + : U := Path (A -> B) f g

Introduction

(Homotopy Introduction, Function Extensionality).

def funext (A B: U) (f g: A → B) (p: Π (x: A), Path B (f x) (g x)) : ~ A B f g - := <i> λ (a: A), p a @ i

(Homotopy Dependent Introduction).

def piext (A: U) (B: A -> U) (f g: (x: A) -> B x) + := <i> λ (a: A), p a @ i

(Homotopy Dependent Introduction).

def piext (A: U) (B: A -> U) (f g: (x: A) -> B x) (p: (x: A) -> Path (B x) (f x) (g x)) : Path ((y: A) -> B y) f g - := <i> λ (a: A), p a @ i

(Homotopy Reflection).

def funext-id (A: U) + := <i> λ (a: A), p a @ i

(Homotopy Reflection).

def funext-id (A: U) : ~ A A (id A) (id A) - := <_> id A

Elimination

(Homotopy Elimination).

def happly (A B: U) (f g: A -> B) + := <_> id A

Elimination

(Homotopy Elimination).

def happly (A B: U) (f g: A -> B) (p: Path (A -> B) f g) (x: A) : Path B (f x) (g x) := cong (A → B) B - (λ (h: A → B), app A B h x) f g p

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

def funext-ind (A B: U) (f g: A → B) (C: funext-D A B) + (λ (h: A → B), app A B h x) f g p

(Homotopy Induction). +For any +and it's evidence at +there is a function . HoTT 5.8.5

def funext-ind (A B: U) (f g: A → B) (C: funext-D A B) (d: Π (f g: A → B), C f f (<_>\(x:A), f x)) : Π (h: Path (A → B) f g), C f g h := λ (h: Path (A → B) f g), @@ -42,16 +42,16 @@ (eta (A → B) f) (g, h) (contr (A → B) f g h) - (d f g)

Computation

(Homotopy Isomorphism Computation).

def funext-β (A B: U) (f g: A → B) + (d f g)

Computation

(Homotopy Isomorphism Computation).

def funext-β (A B: U) (f g: A → B) (p: Π (x: A), Path B (f x) (g x)) : Π (x: A), Path B (f x) (g x) - := λ (x: A), happly A B f g (funext A B f g p) x

(Homotopy Induction Principle Computation).

def funext-ind-β (A B: U) (f g : A → B) (C : funext-D A B) + := λ (x: A), happly A B f g (funext A B f g p) x

(Homotopy Induction Principle Computation).

def funext-ind-β (A B: U) (f g : A → B) (C : funext-D A B) (d: Π (f g: A → B), C f f (<_>\(x:A), f x)) : Path (C f f (<_>f)) (d f f) (funext-ind A B f f C d (<_>f)) := subst-comp (singl (A → B) f) (\ (z: singl (A → B) f), C f (z.1) (z.2)) (eta (A → B) f) - (d f f)

Uniqueness

(Homotopy Isomorphism Uniqueness).

def funext-η (A B: U) (f g: A → B) + (d f f)

Uniqueness

(Homotopy Isomorphism Uniqueness).

def funext-η (A B: U) (f g: A → B) (p: Path (A → B) f g) : Path (Path (A → B) f g) (funext A B f g (happly A B f g p)) p diff --git a/foundations/univalent/iso/index.html b/foundations/univalent/iso/index.html index 04f45439..2116a6c6 100644 --- a/foundations/univalent/iso/index.html +++ b/foundations/univalent/iso/index.html @@ -7,25 +7,25 @@ use[data-c]{stroke-width:3px} ISO

ISOMORPHISM

Just like notion of represents equality -of types and within given universe .

Formation

(Isomorphism Formation).

def iso (A B: U) : U := +ISO

ISOMORPHISM

Just like notion of represents equality +of types and within given universe .

Formation

(Isomorphism Formation).

def iso (A B: U) : U := Σ (f : A -> B) (g : B -> A) (s : section A B f g) - (t : retract A B f g), 𝟏

Introduction

(Isomorphism Introduction).

def iso-intro (A: U) + (t : retract A B f g), 𝟏

Introduction

(Isomorphism Introduction).

def iso-intro (A: U) : iso A A := ( id A, id A, (\(x:A), <_>x), (\(x:A), <_>x), star - )

Elimination

(Isomorphism Induction Principle). -For any -and it's evidence at -there is a function:

def ind-Iso (A B: U) + )

Elimination

(Isomorphism Induction Principle). +For any +and it's evidence at +there is a function:

def ind-Iso (A B: U) (C: Π (A B: U), iso A B → U) (d: C A A (iso-Intro A)) : (p: iso A B) -> C A B p

UNIMORPHISM

Similar to Fibrational Equivalence the notion of Retract/Section based Isomorphism could be introduced as forth-back transport between isomorphism and path equality. This notion is somehow cannonical to all -cubical systems and is called Unimorphism or here.

Formation

(Isomorphism Formation).

Introduction

\ No newline at end of file +cubical systems and is called Unimorphism or here.

Formation

(Isomorphism Formation).

Introduction

\ No newline at end of file diff --git a/foundations/univalent/path/index.html b/foundations/univalent/path/index.html index d91633c8..e3ab1672 100644 --- a/foundations/univalent/path/index.html +++ b/foundations/univalent/path/index.html @@ -7,10 +7,10 @@ use[data-c]{stroke-width:3px} PATH

PATH SPACES

The homotopy identity system defines a -space indexed over type -with elements as functions from interval to values -of that path space . HoTT book +PATH

PATH SPACES

The homotopy identity system defines a +space indexed over type +with elements as functions from interval to values +of that path space . HoTT book defines two induction principles for identity types: path induction and based path induction. The cubical type system CCHM briefly described in [1,2,3,4,5].

1 — Bezem, Coquand, Huber (2014)
@@ -18,33 +18,33 @@ 3 — Pitts, Orton (2016)
4 — Huber (2017)
5 — Vezzosi, Mörtberg , Abel (2019)
-

Formation

(Path Formation).

def Path (A : U) (x y : A) : U +

Formation

(Path Formation).

def Path (A : U) (x y : A) : U := PathP (<_> A) x y def Pathᴵ (A : U) (x y : A) := Π (i : I), A [∂ i |-> [(i = 0) → x , - (i = 1) → y ]]

Introduction

(Path Introduction).

def idp (A: U) (x: A) + (i = 1) → y ]]

Introduction

(Path Introduction).

def idp (A: U) (x: A) : Path A x x := <_> x

Returns a reflexivity path space for a given value of the type. The inhabitant of that path space is the lambda on the homotopy -interval that returns a constant value . Written in -syntax as . -

(Path Application).

def at0 (A: U) (a b: A) +interval that returns a constant value . Written in +syntax as . +

(Path Application).

def at0 (A: U) (a b: A) (p: Path A a b) : A := p @ 0 def at1 (A: U) (a b: A) - (p: Path A a b): A := p @ 1

(Path Connections).

Connections allow you to build a square -with only one element of path: i) ; -ii) . -

-

+ (p: Path A a b): A := p @ 1

(Path Connections).

Connections allow you to build a square +with only one element of path: i) ; +ii) . +

+

def join (A: U) (a b: A) (p: Path A a b) : PathP (<x> Path A (p@x) b) p (<i> b) := <y x> p @ (x \/ y) def meet (A: U) (a b: A) (p: Path A a b) : PathP (<x> Path A a (p@x)) (<i> a) p - := <x y> p @ (x /\ y)

(Path Inversion).

(Congruence).

def ap (A B: U) (f: A -> B) + := <x y> p @ (x /\ y)

(Path Inversion).

(Congruence).

def ap (A B: U) (f: A -> B) (a b: A) (p: Path A a b) : Path B (f a) (f b) @@ -52,56 +52,56 @@ (f: A -> B a) (b: B a) (p: Path A a x) : Path (B a) (f a) (f x)

Maps a given path space between values of one type to path space of another type using an encode function between types. -Implemented as a lambda defined on that returns +Implemented as a lambda defined on that returns application of encode function to path application of -the given path to lamda argument +the given path to lamda argument in both cases. -

(Generalized Transport Kan Operation). +

(Generalized Transport Kan Operation). Transports a value of the left type to the value of the right type -by a given path element of the path space between left and right types.

def transp' (A: U) (x y: A) (p : PathP (<_>A) x y) (i: I) +by a given path element of the path space between left and right types.

def transp' (A: U) (x y: A) (p : PathP (<_>A) x y) (i: I) := transp (<i> (\(_:A),A) (p @ i)) i x def transpᵁ (A B: U) (p : PathP (<_>U) A B) (i: I) - := transp (<i> (\(_:U),U) (p @ i)) i A

(Partial Elements).

def Partial' (A : U) (i : I) - : V := Partial A i

(Cubical Subtypes).

def sub (A : U) (i : I) (u : Partial A i) - : V := A [i ↦ u]

(Cubical Elements).

def inS (A : U) (i : I) (a : A) + := transp (<i> (\(_:U),U) (p @ i)) i A

(Partial Elements).

def Partial' (A : U) (i : I) + : V := Partial A i

(Cubical Subtypes).

def sub (A : U) (i : I) (u : Partial A i) + : V := A [i ↦ u]

(Cubical Elements).

def inS (A : U) (i : I) (a : A) : sub A i [(i = 1) → a] := inc A i a def outS (A : U) (i : I) (u : Partial A i) - : A [i ↦ u] -> A := λ (a: A[i ↦ u]), ouc a

(Heterogeneous Composition Kan Operation).

def compCCHM (A : I → U) (r : I) + : A [i ↦ u] -> A := λ (a: A[i ↦ u]), ouc a

(Heterogeneous Composition Kan Operation).

def compCCHM (A : I → U) (r : I) (u : Π (i : I), Partial (A i) r) (u₀ : (A 0)[r ↦ u 0]) : A 1 := hcomp (A 1) r (λ (i : I), [ (r = 1) → transp (<j> A (i ∨ j)) i (u i 1=>1)]) - (transp (<i> A i) 0 (ouc u₀))

(Homogeneous Composition Kan Operation).

def compCHM (A : U) (r : I) + (transp (<i> A i) 0 (ouc u₀))

(Homogeneous Composition Kan Operation).

def compCHM (A : U) (r : I) (u : I → Partial A r) (u₀ : A[r ↦ u 0]) : A - := hcomp A r u (ouc u₀)

(Substitution).

def subst (A: U) (P: A -> U) (x y: A) (p: Path A x y) + := hcomp A r u (ouc u₀)

(Substitution).

def subst (A: U) (P: A -> U) (x y: A) (p: Path A x y) : P x -> P y - := λ (e: P x), transp (<i> P (p @ i)) 0 e

Other synonyms are and .

(Path Composition).

def pcomp (A: U) (a b c: A) + := λ (e: P x), transp (<i> P (p @ i)) 0 e

Other synonyms are and .

(Path Composition).

def pcomp (A: U) (a b c: A) (p: Path A a b) (q: Path A b c) : Path A a c := subst A (Path A a) b c q p

Composition operation allows building a new path from two given paths in a connected point. The proofterm is -. -

Elimination

(J by Paulin-Mohring).

def J (A: U) +. +

Elimination

(J by Paulin-Mohring).

def J (A: U) (a b: A) (P: singl A a -> U) (u: P (a,refl A a)) : П (p: Path A a b), P (b,p)

J is formulated in a form of Paulin-Mohring and implemented using two facts that singletons are contractible and dependent function transport. -

(Contractability of Singleton).

def singl (A: U) (a: A) : U +

(Contractability of Singleton).

def singl (A: U) (a: A) : U := Σ (x: A), Path A a x def contr (A: U) (a b: A) (p: Path A a b) : Path (singl A a) (a,<_>a) (b,p)

Proof that singleton is contractible space. Implemented as -. -

(HoTT Dependent Eliminator).

def J (A: U) +. +

(HoTT Dependent Eliminator).

def J (A: U) (a: A) (C: (x: A) -> Path A a x -> U) (d: C a (refl A a)) (x: A) : П (p: Path A a x) : C x p

J from HoTT book. -

(Diagonal Path Induction).

def D (A: U) : U +

(Diagonal Path Induction).

def D (A: U) : U := П (x y: A), Path A x y -> U def J (A: U) @@ -109,7 +109,7 @@ (C: D A) (d: C x x (refl A x)) (y: A) - : П (p: Path A x y), C x y p

Computation

(Path Computation).

def trans_comp (A: U) (a: A) + : П (p: Path A x y), C x y p

Computation

(Path Computation).

def trans_comp (A: U) (a: A) : Path A a (trans A A (<_> A) a) def subst_comp (A: U) (P: A -> U) (a: A) (e: P a) diff --git a/intro/index.html b/intro/index.html index bdbab0e0..84d023bc 100644 --- a/intro/index.html +++ b/intro/index.html @@ -13,29 +13,29 @@ впорядкованих у вигляді ізоморфізмів: функцій encode і decode та їх рівнянь — бета і ета правил обчислювальності та унікальності (секції та ретракту). Зазвичай теорія типів вже постачається з наступними типами (примітивами-аксіомами) -та коментарями у вигляді окремих лекцій (конспекти):

Простори функцій ()
- Простори пар ()
- Ідентифікаційні простори ()
- Поліноміальні функтори ()
- Простори шляхів ()
- Склейки ()
- Інфінітезимальні околи ()
- Фактор-простори Lean ()
- CW-комплекси ()

Слухачам курсу (10) пропонується застосувати +та коментарями у вигляді окремих лекцій (конспекти):

Простори функцій ()
+ Простори пар ()
+ Ідентифікаційні простори ()
+ Поліноміальні функтори ()
+ Простори шляхів ()
+ Склейки ()
+ Інфінітезимальні околи ()
+ Фактор-простори Lean ()
+ CW-комплекси ()

Слухачам курсу (10) пропонується застосувати теорію типів для доведення початкового але нетривіального результу, який є відкритою проблемою в теорії типів для однєї із -математик, що є курсами на кафедрі чистої математики (КМ-111):

Теорія гомотопій
- Гомологічна алгебра
- Теорія категорій
- Функціональний аналіз
- Диференціальна геометрія

Курс (10) умовно можна розділити на 4 частини, кожна з яких показує +математик, що є курсами на кафедрі чистої математики (КМ-111):

Теорія гомотопій
+ Гомологічна алгебра
+ Теорія категорій
+ Функціональний аналіз
+ Диференціальна геометрія

Курс (10) умовно можна розділити на 4 частини, кожна з яких показує не тільки типи-аксіоми, але і мета-теоретичні спряження в яких вони приймають участь.

Мотивація

Головна мотивація гомотопічної теорії — надати обчислювальну семантику гомотопічним типам та CW-комплексам. Головна ідея гомотопічної теорії [1] полягає в поєднанні -просторів функцій , просторів контекстів і -просторів шляхів таким чином, що вони +просторів функцій , просторів контекстів і +просторів шляхів таким чином, що вони утворюють фібраційну рівність яка збігається (доводиться в самій теорії) з простором шляхів.

isContr (A: U): U := Σ (x: A), Π (y: A), Path A x y @@ -74,22 +74,22 @@ star )

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


˙

[1]. Pelayo, Warren. Homotopy type theory and Voevodsky's univalent foundations. 2012. -

Фібраційні доведення

Фібраційні доведення моделюються примітивами-аксіомами які є +

Фібраційні доведення

Фібраційні доведення моделюються примітивами-аксіомами які є теоретико-типовими відображеннями категорної мета-теоретичної моделі спряжень трьох функторів Кока-Райта, з яких народжуються простори функцій та простори контекстів: 1) Простір функцій (П); 2) Простір пар (Σ). Ці способи доведення дозволяють безпосреденьо аналізувати розшарування. -

Доведення рівності

В інтенсіональній теорії типів тип рівності вбудований теж +

Доведення рівності

В інтенсіональній теорії типів тип рівності вбудований теж як теоретико-типові примітиви категорної мета-теоретичної моделі спряжень трьох функторів Якобса-Лавіра: 1) Фактор-простору (Q); 2) Ідентифікаційної системи (=); 3) Стягуваного простору (С). Ці способи доведення дозволяють безпосередньо працювати з ідентифікаційними системами: строгою для теорії множин і гомотопічною для теорії гомотопій. -

Індуктивні доведення

В теорії типів індуктивні типи можуть бути вбудованими декількома +

Індуктивні доведення

В теорії типів індуктивні типи можуть бути вбудованими декількома способами: як поліноміальні функтори W і M або загальні схеми ідуктивних типів Полін-Морін (Calculus of Inductive Constructions) з такими властивостями @@ -103,10 +103,10 @@ виступати також простори шляхів, також моделюються поліноміальними функторами, але на відміну F-алгебр Ламбека-Бома тут використовуються монади-алгебри та комонади-коалгебри Люмсдейна-Шульмана-Веццозі. -

Геометричні доведення

Для потреб диференціальної геометрії в теорію типів вбудовують примітиви-аксіоми +

Геометричні доведення

Для потреб диференціальної геометрії в теорію типів вбудовують примітиви-аксіоми категорної мета-теоретичної моделі трьох функторів Шрайбера-Шульмана: 1) Інфінітезімального околу (Im); 2) Редукованої модальності (Re); 3) Інфінітезімального дискретного околу (&). -

Лінійні доведення

+

Лінійні доведення

\ No newline at end of file diff --git a/mathematics/algebra/algebra/index.html b/mathematics/algebra/algebra/index.html index a7fd02f6..dd640f05 100644 --- a/mathematics/algebra/algebra/index.html +++ b/mathematics/algebra/algebra/index.html @@ -10,53 +10,53 @@ ALGEBRA

ALGEBRAIC STRUCTURE

Results presented here are formalized in Ground Zero library using Lean Theorem Prover. -

ALGEBRA

Definition. Signature over given types -(called indices) is an element of type . +

ALGEBRA

Definition. Signature over given types +(called indices) is an element of type .
-Where denotes coproduct type. -

Definition. Vector of length over type -(denoted ) is a type: - +Where denotes coproduct type. +

Definition. Vector of length over type +(denoted ) is a type: +
-Where denotes unit type that contains -only . -

Definition. Assume we have types , -function , and a natural number . -Then we define function : - ≔ -

Definition. -ary algebraic operation over given - type is an element of type: - -

Definition. -ary algebraic relation over given - type is an element of type: - +Where denotes unit type that contains +only . +

Definition. Assume we have types , +function , and a natural number . +Then we define function : + ≔ +

Definition. -ary algebraic operation over given + type is an element of type: + +

Definition. -ary algebraic relation over given + type is an element of type: +
-Where denotes type of all propositions, i.e. - ≔ -

Definition. Algebraic structure over signature constists of: +Where denotes type of all propositions, i.e. + ≔ +

Definition. Algebraic structure over signature constists of: (i) 0-Type called carrier, - (ii) -ary algebraic operation for each , - (iii) -ary algebraic relation for each . + (ii) -ary algebraic operation for each , + (iii) -ary algebraic relation for each .
Or, more explicitly: - ≔ - -
We will write for carrier of algebraic structure , - for its algebraic operations, -and for its relations. -

Mappings

(Homomorphism). Given two algebraic structures over signature -and a function between them , -we say that is homomorphism iff holds: -
(i) , -
(ii) , -
for each or and . -

Composition of two homomorphisms is also homomorphism. -

(Isomorphism). We say that + ≔ + +
We will write for carrier of algebraic structure , + for its algebraic operations, +and for its relations. +

Mappings

(Homomorphism). Given two algebraic structures over signature +and a function between them , +we say that is homomorphism iff holds: +
(i) , +
(ii) , +
for each or and . +

Composition of two homomorphisms is also homomorphism. +

(Isomorphism). We say that is an ismorphism iff it is bijective and homomorphism. -Then we can say that and are isomorphic and write . -

Isomorphism is an equivalence relation, i.e. -
(i) , -
(ii) , -
(iii) . -

(Univalence for Algebraic Structures). - +Then we can say that and are isomorphic and write . +

Isomorphism is an equivalence relation, i.e. +
(i) , +
(ii) , +
(iii) . +

(Univalence for Algebraic Structures). +

\ No newline at end of file diff --git a/mathematics/algebra/homology/index.html b/mathematics/algebra/homology/index.html index 4147ffc1..ec1bc4b5 100644 --- a/mathematics/algebra/homology/index.html +++ b/mathematics/algebra/homology/index.html @@ -10,20 +10,20 @@ HOMOLOGY

HOMOLOGY

Homology package contains basic theorems about general homology theory.

SETS

Definition (Proposition, Set). -Type is a proposition if -all elements of are equal. -Type is a set if -all paths between elements of are equal. -≔ -≔

n_grpd (A: U) (n: N): U = (a b: A) -> rec A a b n where +Type is a proposition if +all elements of are equal. +Type is a set if +all paths between elements of are equal. +≔ +≔

n_grpd (A: U) (n: N): U = (a b: A) -> rec A a b n where rec (A: U) (a b: A) : (k: N) -> U = split { Z -> Path A a b ; S n -> n_grpd (Path A a b) n } isProp (A: U): U = n_grpd A Z -isSet (A: U): U = n_grpd A (S Z)


GROUPS

(Monoid). Monoid is a set equipped +isSet (A: U): U = n_grpd A (S Z)


GROUPS

(Monoid). Monoid is a set equipped with binary associative operation - called multiplication and identity element satisfying -.

isMonoid (M: SET): U + called multiplication and identity element satisfying +.

isMonoid (M: SET): U = (op: M.1 -> M.1 -> M.1) * (assoc: isAssociative M.1 op) * (id: M.1) @@ -36,9 +36,9 @@ monoidhom (a b: monoid): U = (f: a.1.1 -> b.1.1) * (ismonoidhom a b f) -

(Group). Group is a monoid -with inversion satisfying -.

isGroup (G: SET): U +

(Group). Group is a monoid +with inversion satisfying +.

isGroup (G: SET): U = (m: isMonoid G) * (inv: G.1 -> G.1) * (hasInverse G.1 m.1 m.2.2.1 inv) @@ -46,7 +46,7 @@ opGroup (g: group): g.1.1 -> g.1.1 -> g.1.1 idGroup (g: group): g.1.1 invGroup (g: group): g.1.1 -> g.1.1 -

(Differential Group).

isDifferentialGroup (G: SET): U +

(Differential Group).

isDifferentialGroup (G: SET): U = (g: isGroup G) * (comm: isCommutative G.1 g.1.1) * (boundary: G.1 -> G.1) @@ -54,98 +54,98 @@ dgroup: U = (X: SET) * isDifferentialGroup X dgrouphom (a b: dgroup): U = monoidhom (a.1, a.2.1.1) (b.1, b.2.1.1) -unitDGroup: dgroup

(Division). -≔ -≔

ldiv (H: group) (g h: H.1.1) : H.1.1 +unitDGroup: dgroup

(Division). +≔ +≔

ldiv (H: group) (g h: H.1.1) : H.1.1 = (opGroup H) ((invGroup H) g) h rdiv (H: group) (g h: H.1.1) : H.1.1 - = (opGroup H) g ((invGroup H) h)

(Conjugation). -Let be a group, the conjugation of two elements of the group - is defined as .

conjugate (G: group) (g1 g2: G.1.1): G.1.1 - = rdiv G ((opGroup G) g1 g2) g1


SUBGROUPS

(Predicate). Type family - is a predicate iff - is a mere proposition for all . -

subtypeProp (A: U): U + = (opGroup H) g ((invGroup H) h)

(Conjugation). +Let be a group, the conjugation of two elements of the group + is defined as .

conjugate (G: group) (g1 g2: G.1.1): G.1.1 + = rdiv G ((opGroup G) g1 g2) g1


SUBGROUPS

(Predicate). Type family + is a predicate iff + is a mere proposition for all . +

subtypeProp (A: U): U = (P : A -> U) - * (a : A) -> isProp (P a)

(Subtype). -Let be a predicate. Then: -≔

subtype (A : U) (P : subtypeProp A): U + * (a : A) -> isProp (P a)

(Subtype). +Let be a predicate. Then: +≔

subtype (A : U) (P : subtypeProp A): U = (x : A) -- prop - * (P.1 x) -- level

(Subgroup). -Predicate is a subgroup iff -1) -2) and -3)

subgroupProp (G: group): U + * (P.1 x) -- level

(Subgroup). +Predicate is a subgroup iff +1) +2) and +3)

subgroupProp (G: group): U = (prop: G.1.1 -> U) * (level: (x: G.1.1) -> isProp (prop x)) * (ident: prop (idGroup G)) * (inv: (g: G.1.1) -> prop g -> prop ((invGroup G) g)) - * ((g1 g2: G.1.1) -> prop g1 -> prop g2 -> prop ((opGroup G) g1 g2))

(Normal Subgroup). -Subgroup is normal iff for every -it contains conjugate of .

isNormal (G: group) (P: subgroupProp G) : U + * ((g1 g2: G.1.1) -> prop g1 -> prop g2 -> prop ((opGroup G) g1 g2))

(Normal Subgroup). +Subgroup is normal iff for every +it contains conjugate of .

isNormal (G: group) (P: subgroupProp G) : U = (X: group) * (g1 g2: G.1.1) -> P.1 g2 -> P.1 (conjugate G g1 g2) normalSubgroupProp (G: group): U = (P: subgroupProp G) - * isNormal G P


KERNEL and IMAGE

(Kernel of Homomorphism). -≔

isGroupKer (G H: group) (f: G.1.1 -> H.1.1) (x: G.1.1): U - = Path H.1.1 (f x) (idGroup H)

(Image of Homomorphism). -≔

isGroupIm (G H: group) (f: G.1.1 -> H.1.1) (g: H.1.1): U - = propTrunc (fiber G.1.1 H.1.1 f g)

(Kernel of Homomorphism is subgroup).

kerProp (G H: group) (phi: grouphom G H) - : subgroupProp G

(Image of Homomorphism is subgroup).

imProp (G H: group) (phi: grouphom G H) - : subgroupProp H

(Set-Quotient). -Assume some type and relation - on it. -We define as following Higher Inductive Type: -≔

data setQuot (A: U) (R: A -> A -> U) + * isNormal G P


KERNEL and IMAGE

(Kernel of Homomorphism). +≔

isGroupKer (G H: group) (f: G.1.1 -> H.1.1) (x: G.1.1): U + = Path H.1.1 (f x) (idGroup H)

(Image of Homomorphism). +≔

isGroupIm (G H: group) (f: G.1.1 -> H.1.1) (g: H.1.1): U + = propTrunc (fiber G.1.1 H.1.1 f g)

(Kernel of Homomorphism is subgroup).

kerProp (G H: group) (phi: grouphom G H) + : subgroupProp G

(Image of Homomorphism is subgroup).

imProp (G H: group) (phi: grouphom G H) + : subgroupProp H

(Set-Quotient). +Assume some type and relation + on it. +We define as following Higher Inductive Type: +≔

data setQuot (A: U) (R: A -> A -> U) = quotient (a: A) | identification (a b: A) (r: R a b) <i>[ (i=0) -> quotient a, (i=1) -> quotient b ] | trunc (a b : setQuot A R) (p q : Path (setQuot A R) a b) <i j> [ (i = 0) -> p @ j , (i = 1) -> q @ j , - (j = 0) -> a , (j = 1) -> b ]

(Factor Group). -Let be a group and his normal subgroup. We define: -≔ -≔ -We can also define by relation . -If is normal subgroup then . + (j = 0) -> a , (j = 1) -> b ]

(Factor Group). +Let be a group and his normal subgroup. We define: +≔ +≔ +We can also define by relation . +If is normal subgroup then . This statement is proven in Lean.

factorProp (G : group) (P : normalSubgroupProp G) : G.1.1 -> G.1.1 -> U = \(x y : G.1.1) -> P.1.1 (rdiv G x y) factor (G : group) (P : normalSubgroupProp G) : U - = setQuot G.1.1 (factorProp G P)

(Factor group of dihedral group ). -As an test of factor group correctness we prove that , where and , -i. e. smallest nontrivial group.

def D₃.iso : Z₂ ≅ D₃\A₃

(Trivial homomorphism). -Trivial homomorphism between two groups (or monoids) and -maps every element of to identity element of :

trivmonoidhom (a b : monoid) : monoidhom a b + = setQuot G.1.1 (factorProp G P)

(Factor group of dihedral group ). +As an test of factor group correctness we prove that , where and , +i. e. smallest nontrivial group.

def D₃.iso : Z₂ ≅ D₃\A₃

(Trivial homomorphism). +Trivial homomorphism between two groups (or monoids) and +maps every element of to identity element of :

trivmonoidhom (a b : monoid) : monoidhom a b = (\(x : a.1.1) -> idMonoid b, \(x y : a.1.1) -> <i> (hasIdMonoid b).1 (idMonoid b) @ -i, <_> idMonoid b) trivabgrouphom (a b : abgroup) : abgrouphom a b - = trivmonoidhom (group' (abgroup' a)) (group' (abgroup' b))

(Chain complex). + = trivmonoidhom (group' (abgroup' a)) (group' (abgroup' b))

(Chain complex). Chain complex consists of: -1) Sequence of abelian groups . -2) Homomorphisms between these groups . -3) Requirement: the composition of two consecutive homomorphisms is trivial: -

chainComplex : U +1) Sequence of abelian groups . +2) Homomorphisms between these groups . +3) Requirement: the composition of two consecutive homomorphisms is trivial: +

chainComplex : U = (K : nat -> abgroup) * (hom : (n : nat) -> abgrouphom (K (succ n)) (K n)) * ((n : nat) -> Path (abgrouphom (K (succ2 n)) (K n)) (abgrouphomcomp (K (succ2 n)) (K (succ n)) (K n) (hom (succ n)) (hom n)) - (trivabgrouphom (K (succ2 n)) (K n)))

(Cycles). ≔

propZ (C : chainComplex) (n : nat) : subgroupProp (K' C (succ n)) + (trivabgrouphom (K (succ2 n)) (K n)))

(Cycles). ≔

propZ (C : chainComplex) (n : nat) : subgroupProp (K' C (succ n)) = kerProp (K' C (succ n)) (K' C n) (hom C n) -Z (C : chainComplex) (n : nat) : group = subgroup (K' C (succ n)) (propZ C n)

(Boundaries). ≔

B (C : chainComplex) (n : nat) : normalSubgroupProp (Z C n) +Z (C : chainComplex) (n : nat) : group = subgroup (K' C (succ n)) (propZ C n)

(Boundaries). ≔

B (C : chainComplex) (n : nat) : normalSubgroupProp (Z C n) = abelianSubgroupIsNormal (abelianSubgroupIsAbelian (K C (succ n)) (propZ C n)) (subgroupSubgroup (K' C (succ n)) - (imProp (K' C (succ (succ n))) (K' C (succ n)) (hom C (succ n))) (propZ C n))

(Homology Group). ≔

H (C : chainComplex) (n : nat) : group = factorGroup (Z C n) (B C n)

(First Group Isomorphism Theorem). Let and be groups, -and let be a homomorphism. Then: -1) The kernel of is normal subgroup of G. -2) The image of is a subgroup of . -3) The image of is isomorphic to the quotient group .


By composition of and we obtain -a path . -Therefore, contains every conjugation of


kernelIsNormalSubgroup (G H : group) (phi : grouphom G H) + (imProp (K' C (succ (succ n))) (K' C (succ n)) (hom C (succ n))) (propZ C n))

(Homology Group). ≔

H (C : chainComplex) (n : nat) : group = factorGroup (Z C n) (B C n)

(First Group Isomorphism Theorem). Let and be groups, +and let be a homomorphism. Then: +1) The kernel of is normal subgroup of G. +2) The image of is a subgroup of . +3) The image of is isomorphic to the quotient group .


By composition of and we obtain +a path . +Therefore, contains every conjugation of


kernelIsNormalSubgroup (G H : group) (phi : grouphom G H) : normalSubgroupProp G


\ No newline at end of file diff --git a/mathematics/analysis/set/index.html b/mathematics/analysis/set/index.html index c0aa0946..c7dbc319 100644 --- a/mathematics/analysis/set/index.html +++ b/mathematics/analysis/set/index.html @@ -10,11 +10,11 @@ SET

Set Theory

Other disputed foundations for set theory could be taken as: ZFC, NBG, ETCS. We will disctinct syntetically: i) category theory; ii) set theory in univalent foundations; iii) topos theory, grothendieck topos, -elementary topos.

Here is the -groupoid model of sets.

(Mere proposition, ). A type P is a mere proposition -if for all we have :

(0-type). A type A is a 0-type is for all - and we have .

(1-type). A type A is a 1-type if for all - and and , we have .

(A set of elements, ). -A type A is a if for all and , we have :

. If A is a set then A is a 1-type.

data N = Z | S (n: N) +elementary topos.

Here is the -groupoid model of sets.

(Mere proposition, ). A type P is a mere proposition +if for all we have :

(0-type). A type A is a 0-type is for all + and we have .

(1-type). A type A is a 1-type if for all + and and , we have .

(A set of elements, ). +A type A is a if for all and , we have :

. If A is a set then A is a 1-type.

data N = Z | S (n: N) n_grpd (A: U) (n: N): U = (a b: A) -> rec A a b n where rec (A: U) (a b: A) : (k: N) -> U @@ -25,11 +25,11 @@ isSet (A: U): U = n_grpd A (S Z) PROP : U = (X:U) * isProp X -SET : U = (X:U) * isSet X

(-Contractability). if fiber is set then +SET : U = (X:U) * isSet X

(-Contractability). if fiber is set then path space between any sections is contractible.

setPi (A: U) (B: A -> U) (h: (x: A) -> isSet (B x)) (f g: Pi A B) (p q: Path (Pi A B) f g) - : Path (Path (Pi A B) f g) p q

(-Contractability). if fiber is set then is set.

setSig (A:U) (B: A -> U) (sA: isSet A) - (sB : (x:A) -> isSet (B x)) : isSet (Sigma A B)

(Unit type, ). The unit is a type with one element.

data unit = tt + : Path (Path (Pi A B) f g) p q

(-Contractability). if fiber is set then is set.

setSig (A:U) (B: A -> U) (sA: isSet A) + (sB : (x:A) -> isSet (B x)) : isSet (Sigma A B)

(Unit type, ). The unit is a type with one element.

data unit = tt unitRec (C: U) (x: C): unit -> C = split tt -> x -unitInd (C: unit -> U) (x: C tt): (z:unit) -> C z = split tt -> x

( is a proposition).

propUnit : isProp unit

( is a set).

setUnit : isSet unit +unitInd (C: unit -> U) (x: C tt): (z:unit) -> C z = split tt -> x

( is a proposition).

propUnit : isProp unit

( is a set).

setUnit : isSet unit
\ No newline at end of file diff --git a/mathematics/categories/category/index.html b/mathematics/categories/category/index.html index 1f7f1778..30c1836b 100644 --- a/mathematics/categories/category/index.html +++ b/mathematics/categories/category/index.html @@ -8,28 +8,28 @@ CATEGORY

category

Category package contains basic notion of categories, constructions and examples. -

Basics

Monoidal Structure

(Category Signature). The signature of category is -a where could be any universe. -The projection is called and projection is -called , where . +

Basics

Monoidal Structure

(Category Signature). The signature of category is +a where could be any universe. +The projection is called and projection is +called , where .

cat: U = (A: U) * (A -> A -> U) -

Precategory

Precategory defined as set of where - are objects defined by its arrows . +

Precategory

Precategory defined as set of where + are objects defined by its arrows . Properfies of left and right units included with composition c and its associativity. -

(Precategory). More formal, precategory consists of the following. -(i) A type , whose elements are called objects; -(ii) for each , a set , whose elements are called arrows or morphisms. -(iii) For each , a morphism , called the identity morphism. -(iv) For each , a function - -called composition, and denoted . -(v) For each and , - and . -(vi) For each and -, , , -. -

(Small Category). If for all the forms a Set, then +

(Precategory). More formal, precategory consists of the following. +(i) A type , whose elements are called objects; +(ii) for each , a set , whose elements are called arrows or morphisms. +(iii) For each , a morphism , called the identity morphism. +(iv) For each , a function + +called composition, and denoted . +(v) For each and , + and . +(vi) For each and +, , , +. +

(Small Category). If for all the forms a Set, then such category is called small category.

isPrecategory (C: cat): U = (id: (x: C.1) -> C.2 x x) @@ -41,25 +41,25 @@ Path (C.2 x w) (c x z w (c x y z f g) h) (c x y w f (c y z w g h))) precategory: U = (C: cat) * isPrecategory C

Accessors of the precategory structure. -For is carrier and for is hom. +For is carrier and for is hom.

carrier (C: precategory): U = C.1.1 hom (C: precategory) (a b: carrier C): U = C.1.2 a b path (C: precategory) (x: carrier C): hom C x x = C.2.1 x compose (C: precategory) (x y z: carrier C) (f: hom C x y) (g: hom C y z): hom C x z = C.2.2.1 x y z f g -

(Co)-Terminal Objects

(Initial Object). Is such object , -that . -

(Terminal Object). Is such object , -that . +

(Co)-Terminal Objects

(Initial Object). Is such object , +that . +

(Terminal Object). Is such object , +that .

isInitial (C: precategory) (x: carrier C): U = (y: carrier C) -> isContr (hom C x y) isTerminal (C: precategory) (y: carrier C): U = (x: carrier C) -> isContr (hom C x y) initial (C: precategory): U = (x: carrier C) * isInitial C x terminal (C: precategory): U = (y: carrier C) * isTerminal C y -

Functor

(Category Functor). Let and be precategories. -A functor consists of: (i) A function ; -(ii) for each , a function ; -(iii) for each , ; -(iv) for and and , . +

Functor

(Category Functor). Let and be precategories. +A functor consists of: (i) A function ; +(ii) for each , a function ; +(iii) for each , ; +(iv) for and and , .

catfunctor (A B: precategory): U = (ob: carrier A -> carrier B) * (mor: (x y: carrier A) -> hom A x y -> hom B (ob x) (ob y)) @@ -67,10 +67,10 @@ * ((x y z: carrier A) -> (f: hom A x y) -> (g: hom A y z) -> Path (hom B (ob x) (ob z)) (mor x z (compose A x y z f g)) (compose B (ob x) (ob y) (ob z) (mor x y f) (mor y z g))) -

Natural Transformation

(Natural Transformation). For functors , -a nagtural transformation consists of: -(i) for each , a morphism ; -(ii) for each and , . +

Natural Transformation

(Natural Transformation). For functors , +a nagtural transformation consists of: +(i) for each , a morphism ; +(ii) for each and , .

isNaturalTrans (C D: precategory) (F G: catfunctor C D) (eta: (x: carrier C) -> hom D (F.1 x) (G.1 x)): U @@ -82,17 +82,17 @@ ntrans (C D: precategory) (F G: catfunctor C D): U = (eta: (x: carrier C) -> hom D (F.1 x) (G.1 x)) * (isNaturalTrans C D F G eta) -

Kan Extensions

(Kan Extension). +

Kan Extensions

(Kan Extension).

extension (C C' D: precategory) (K: catfunctor C C') (G: catfunctor C D) : U = (F: catfunctor C' D) * (ntrans C D (compFunctor C C' D K F) G) -

Category Isomorphism

Definition (Category Isomorphism). A morphism is an iso -if there is a morphism such that - and -. "f is iso" is +

Category Isomorphism

Definition (Category Isomorphism). A morphism is an iso +if there is a morphism such that + and +. "f is iso" is a mere proposition. -

If A is a precategory and , -then (idtoiso).

iso (C: precategory) (A B: carrier C): U +

If A is a precategory and , +then (idtoiso).

iso (C: precategory) (A B: carrier C): U = (f: hom C A B) * (g: hom C B A) * (eta: Path (hom C A A) (compose C A B A f g) (path C A)) @@ -100,11 +100,11 @@

Rezk-completion

Definition (Category). A category is a precategory such that for all $a:Ob_C$, the $\Pi_{A:Ob_C} isContr \Sigma_{B:Ob_C} iso_C(A,B)$.

isCategory (C: precategory): U = (A: carrier C) -> isContr ((B: carrier C) * iso C A B) -category: U = (C: precategory) * isCategory C

Constructions

(Co)-Product of Categories

(Category Product). +category: U = (C: precategory) * isCategory C

Constructions

(Co)-Product of Categories

(Category Product).

Product (X Y: precategory) : precategory Coproduct (X Y: precategory) : precategory -

Opposite Category

(Opposite Category). The opposite category to category -is a category with same structure, except all arrows are inverted. +

Opposite Category

(Opposite Category). The opposite category to category +is a category with same structure, except all arrows are inverted.

opCat (P: precategory): precategory

(Co)-Slice Category

Definition (Slice Category).

Definition (Coslice Category). @@ -117,7 +117,7 @@ cosliceCat (C D: precategory) (a: carrier C) (F: catfunctor D C) : precategory -

Universal Mapping Property

(Universal Mapping Property). +

Universal Mapping Property

(Universal Mapping Property).

initArr (C D: precategory) (a: carrier C) (F: catfunctor D C): U = initial (cosliceCat C D a F) @@ -125,9 +125,9 @@ termArr (C D: precategory) (a: carrier (opCat C)) (F: catfunctor D (opCat C)): U = terminal (sliceCat C D a F) -

Unit Category

(Unit Category). In unit category both and . +

Unit Category

(Unit Category). In unit category both and .

unitCat: precategory -

Examples

Category of Sets

(Category of Sets). +

Examples

Category of Sets

(Category of Sets).

Set: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = SET Hom (A B: Ob): U = A.1 -> B.1 @@ -139,7 +139,7 @@ Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D) : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h)) = refl (Hom A D) (c A B D f (c B C D g h)) -

Category of Functions

(Category of Functions over Sets). +

Category of Functions

(Category of Functions over Sets).

Functions (X Y: U) (Z: isSet Y): precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = X -> Y Hom (A B: Ob): U = id (X -> Y) @@ -150,7 +150,7 @@ R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = undefined Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D) : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h)) = undefined -

Category of Categories

(Category of Categories). +

Category of Categories

(Category of Categories).

Cat: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = precategory Hom (A B: Ob): U = catfunctor A B @@ -161,7 +161,7 @@ R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = undefined Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D) : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h)) = undefined -

Category of Functors

(Category of Functors). +

Category of Functors

(Category of Functors).

Func (X Y: precategory): precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = catfunctor X Y Hom (A B: Ob): U = ntrans X Y A B diff --git a/mathematics/categories/presheaf/index.html b/mathematics/categories/presheaf/index.html index 3bd8dcbc..880ca24c 100644 --- a/mathematics/categories/presheaf/index.html +++ b/mathematics/categories/presheaf/index.html @@ -12,97 +12,97 @@ Formal Set Topos. Presheaf model of type theory could be seen as generalization of the notion of Kripke model. -

INTRO

(Presheaf over ). -A presheaf over a category is a functor -from to the category of . -We denote as and as , -identity morphisms , -composition for , . -This means a presheaf is given by a family of sets -and restriction maps , for - satisfying the laws and for -. The family of sets is called right action.

By the nature of the rescription maps we could classify presheaves: +

INTRO

(Presheaf over ). +A presheaf over a category is a functor +from to the category of . +We denote as and as , +identity morphisms , +composition for , . +This means a presheaf is given by a family of sets +and restriction maps , for + satisfying the laws and for +. The family of sets is called right action.

By the nature of the rescription maps we could classify presheaves: i) if the restriction map forms a boundary operator (degeneracy map) -, such that +, such that then this is cohomology presheaf; ii) if the restriction map is a process action - then this is process presheaf; + then this is process presheaf; iii) if the restriction map actually restricts the domain the such presheaf is -called topological (default meaning).

(Yoneda presheaf ). -Any object of base category defines a -presheaf represented by . -This presheaf assigns to each object in -the set of arrows . Given anarrow -composition with f maps an arrow to an arrow . -In other words -then a set of maps and the restriction maps defined by composition.

(Seive). -A sieve on is a set of maps with codomain such that -is in whenever is in and .

(Subpresheaf ). -Subpresheaf of a presheaf A is a map , which -for each selects a subset of of shape defined by polyhedron A. - is a presheaf where is a set of decidable seives, -so that we can decide if is a member of . -

DEPENDENT TYPES

(Type). -A type is interpreted as a presheaf , a family of sets with restriction maps - for . A dependent type -B on A is interpreted by a presheaf on category of elements of : the objects -are pairs with and morphisms are -maps such that . A dependent type B is thus given -by a family of sets and restriction maps . -

We think of as a type and as a family of presheves varying . -The operation generalizes the semantics of +called topological (default meaning).

(Yoneda presheaf ). +Any object of base category defines a +presheaf represented by . +This presheaf assigns to each object in +the set of arrows . Given anarrow +composition with f maps an arrow to an arrow . +In other words +then a set of maps and the restriction maps defined by composition.

(Seive). +A sieve on is a set of maps with codomain such that +is in whenever is in and .

(Subpresheaf ). +Subpresheaf of a presheaf A is a map , which +for each selects a subset of of shape defined by polyhedron A. + is a presheaf where is a set of decidable seives, +so that we can decide if is a member of . +

DEPENDENT TYPES

(Type). +A type is interpreted as a presheaf , a family of sets with restriction maps + for . A dependent type +B on A is interpreted by a presheaf on category of elements of : the objects +are pairs with and morphisms are +maps such that . A dependent type B is thus given +by a family of sets and restriction maps . +

We think of as a type and as a family of presheves varying . +The operation generalizes the semantics of implication in a Kripke model. -

(Pi). An element is a family -of functions for such -that when and . -

(Sigma). The set is the set -of pairs when and restriction map . -

SIMPLICIAL TYPES

(Simplicial Types). +

(Pi). An element is a family +of functions for such +that when and . +

(Sigma). The set is the set +of pairs when and restriction map . +

SIMPLICIAL TYPES

(Simplicial Types). The simplicial type is defined as a presheaf on category of -finite linear posets and monotone maps. Let's write a presheaf -as . In a sense that this +finite linear posets and monotone maps. Let's write a presheaf +as . In a sense that this is a category on a shapes, the notion of subpolyhedras is then represented by subpresheaves. -

(). -The category of simplicial types denoted . -

CUBICAL TYPES

(Cubical Presheaf ). +

(). +The category of simplicial types denoted . +

CUBICAL TYPES

(Cubical Presheaf ). The identity types modeled with another presheaf, the presheaf on Lawvere category of distributive lattices (theory of de Morgan algebras) denoted -with . -

. The presheaf : -i) has to distinct global elements and (B); -ii) (I) has a decidable equality for each (B); -iii) is tiny so the path functor has right adjoint (B).; -iv) has meet and join (connections, B). -

NOTE: In the simplicial model B condition is underivable. -

(Cofibrations Subpresheaf ). -The subpresheaf corresponds to a map - so that can -be seen internally as the subpresheaf of propositions in - satisfying the property (which -reads ‘ is cofibrant’). In other words +with . +

. The presheaf : +i) has to distinct global elements and (B); +ii) (I) has a decidable equality for each (B); +iii) is tiny so the path functor has right adjoint (B).; +iv) has meet and join (connections, B). +

NOTE: In the simplicial model B condition is underivable. +

(Cofibrations Subpresheaf ). +The subpresheaf corresponds to a map + so that can +be seen internally as the subpresheaf of propositions in + satisfying the property (which +reads ‘ is cofibrant’). In other words classified cofibrant maps. -

: -i) cofibrant maps should contain isomorphisms and be closed under composition (A); -ii) is closed under disjunction: -(A). -

. This properties defined how we can mix the +

: +i) cofibrant maps should contain isomorphisms and be closed under composition (A); +ii) is closed under disjunction: +(A). +

. This properties defined how we can mix the contexts of depedent types and cubical types: -i) wedge (C); -ii) cofibrations (C). -

NOTE: B could be replaced with strengthened -C. -

: -i) — free monoidal category on interval ; -ii) — free monoidal category on interval with connections and ; -iii) — free symmetric monoidal category on interval; -iv) — free cartesian category on interval; -v) — free cartesian category on distributive lattice. -

NOTE: the cartesian cube category is the opposite of -the category of finite, strictly bipointed sets: . +i) wedge (C); +ii) cofibrations (C). +

NOTE: B could be replaced with strengthened +C. +

: +i) — free monoidal category on interval ; +ii) — free monoidal category on interval with connections and ; +iii) — free symmetric monoidal category on interval; +iv) — free cartesian category on interval; +v) — free cartesian category on distributive lattice. +

NOTE: the cartesian cube category is the opposite of +the category of finite, strictly bipointed sets: .

Theorem (Awodey). -The category of cubical types (presheaves on ) is the -classifying topos of strictly bipointed objects . Geometric -realisation preserves finite products. +The category of cubical types (presheaves on ) is the +classifying topos of strictly bipointed objects . Geometric +realisation preserves finite products.

SIMPLIFICATION

What if we take not a category as the underlying objects for sheaves diff --git a/mathematics/categories/topos/index.html b/mathematics/categories/topos/index.html index 6668b58b..f4a2d5a5 100644 --- a/mathematics/categories/topos/index.html +++ b/mathematics/categories/topos/index.html @@ -26,11 +26,11 @@ Myles Tierney. The main contribution is the reformulation of Grothendieck topology using subobject classifier.

Category Theory

First of all, a very simple category theory up to pullbacks is provided. We provide here -all definitions only to keep the context valid.

(Category Signature). The signature of category is -a where could be any universe. -The projection is called and projection is -called , where .

cat: U = (A: U) * (A -> A -> U)

Precategory defined as set of where -are objects defined by its arrows . +all definitions only to keep the context valid.

(Category Signature). The signature of category is +a where could be any universe. +The projection is called and projection is +called , where .

cat: U = (A: U) * (A -> A -> U)

Precategory defined as set of where +are objects defined by its arrows . Properfies of left and right units included with composition and its associativity.

isPrecategory (C: cat): U = (id: (x: C.1) -> C.2 x x) @@ -39,28 +39,28 @@ * (left: (x y: C.1) -> (f: C.2 x y) -> Path (C.2 x y) (c x x y (id x) f) f) * (right: (x y: C.1) -> (f: C.2 x y) -> Path (C.2 x y) (c x y y f (id y)) f) * ( (x y z w: C.1) -> (f: C.2 x y) -> (g: C.2 y z) -> (h: C.2 z w) -> - Path (C.2 x w) (c x z w (c x y z f g) h) (c x y w f (c y z w g h)))

(Precategory). More formally, precategory consists of the following. -(i) A type , whose elements are called objects; -(ii) for each , a set , whose elements are called arrows or morphisms. -(iii) For each , a morphism , called the identity morphism. -(iv) For each , a function - -called composition, and denoted . -(v) For each and , - and . -(vi) For each and -, , , -.

carrier (C: precategory) : U + Path (C.2 x w) (c x z w (c x y z f g) h) (c x y w f (c y z w g h)))

(Precategory). More formally, precategory consists of the following. +(i) A type , whose elements are called objects; +(ii) for each , a set , whose elements are called arrows or morphisms. +(iii) For each , a morphism , called the identity morphism. +(iv) For each , a function + +called composition, and denoted . +(v) For each and , + and . +(vi) For each and +, , , +.

carrier (C: precategory) : U hom (C: precategory) (a b: carrier C) : U compose (C: precategory) (x y z: carrier C) - (f: hom C x y) (g: hom C y z) : hom C x z

(Terminal Object). Is such object , -that .

isTerminal (C: precategory) (y: carrier C): U = (x: carrier C) -> isContr (hom C x y) -terminal (C: precategory): U = (y: carrier C) * isTerminal C y

(Categorical Pullback). -The pullback of the cospan is a object with -morphisms , , such that -diagram commutes:

Pullback must be universal, meaning that for any -for which diagram also commutes there must exist a unique , -such that and .

homTo (C: precategory) (X: carrier C): U = (Y: carrier C) * hom C Y X + (f: hom C x y) (g: hom C y z) : hom C x z

(Terminal Object). Is such object , +that .

isTerminal (C: precategory) (y: carrier C): U = (x: carrier C) -> isContr (hom C x y) +terminal (C: precategory): U = (y: carrier C) * isTerminal C y

(Categorical Pullback). +The pullback of the cospan is a object with +morphisms , , such that +diagram commutes:

Pullback must be universal, meaning that for any +for which diagram also commutes there must exist a unique , +such that and .

homTo (C: precategory) (X: carrier C): U = (Y: carrier C) * hom C Y X cospan (C: precategory): U = (X: carrier C) * (_: homTo C X) * homTo C X hasCospanCone (C: precategory) (D: cospan C) (W: carrier C) : U @@ -81,11 +81,11 @@ = (h: cospanCone C D) -> isContr (cospanConeHom C D h E) hasPullback (C: precategory) (D: cospan C) : U = (E: cospanCone C D) * isPullback C D E -

Set Theory

Here is the -groupoid model of sets.

(Mere proposition, ). A type P is a mere proposition -if for all we have :

(0-type). A type A is a 0-type is for all - and we have .

(1-type). A type A is a 1-type if for all - and and , we have .

(A set of elements, ). -A type A is a if for all and , we have :

. If A is a set then A is a 1-type.

data N = Z | S (n: N) +

Set Theory

Here is the -groupoid model of sets.

(Mere proposition, ). A type P is a mere proposition +if for all we have :

(0-type). A type A is a 0-type is for all + and we have .

(1-type). A type A is a 1-type if for all + and and , we have .

(A set of elements, ). +A type A is a if for all and , we have :

. If A is a set then A is a 1-type.

data N = Z | S (n: N) n_grpd (A: U) (n: N): U = (a b: A) -> rec A a b n where rec (A: U) (a b: A) : (k: N) -> U @@ -96,15 +96,15 @@ isSet (A: U): U = n_grpd A (S Z) PROP : U = (X:U) * isProp X -SET : U = (X:U) * isSet X

(-Contractability). if fiber is set then +SET : U = (X:U) * isSet X

(-Contractability). if fiber is set then path space between any sections is contractible.

setPi (A: U) (B: A -> U) (h: (x: A) -> isSet (B x)) (f g: Pi A B) (p q: Path (Pi A B) f g) - : Path (Path (Pi A B) f g) p q

(-Contractability). if fiber is set then is set.

setSig (A:U) (B: A -> U) (sA: isSet A) - (sB : (x:A) -> isSet (B x)) : isSet (Sigma A B)

(Unit type, ). The unit is a type with one element.

data unit = tt + : Path (Path (Pi A B) f g) p q

(-Contractability). if fiber is set then is set.

setSig (A:U) (B: A -> U) (sA: isSet A) + (sB : (x:A) -> isSet (B x)) : isSet (Sigma A B)

(Unit type, ). The unit is a type with one element.

data unit = tt unitRec (C: U) (x: C): unit -> C = split tt -> x -unitInd (C: unit -> U) (x: C tt): (z:unit) -> C z = split tt -> x

( is a proposition).

propUnit : isProp unit

( is a set).

setUnit : isSet unit

(Category of Sets, ). Sets forms a Category. +unitInd (C: unit -> U) (x: C tt): (z:unit) -> C z = split tt -> x

( is a proposition).

propUnit : isProp unit

( is a set).

setUnit : isSet unit

(Category of Sets, ). Sets forms a Category. All compositional theorems are proved using reflection rule of internal language. -The proof that forms a set is taken through -contractability.

Set: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where +The proof that forms a set is taken through -contractability.

Set: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = SET Hom (A B: Ob): U = A.1 -> B.1 id (A: Ob): Hom A A = idfun A.1 @@ -119,11 +119,11 @@ structure reformulated in a categorical way as a category of sheaves on a site or as one that has cartesian closure and subobject classifier. We provide two definitions here. -

Topological Structure

(Topology). The topological structure on -(or topology) is a subset with following properties: -i) any finite union of subsets of belongs to ; -ii) any finite intersection of subsets of belongs to . -Subets of are called open sets of family .

Here is a code snippet in Coq for this classical definition.

Structure topology (A : Type) := { +

Topological Structure

(Topology). The topological structure on +(or topology) is a subset with following properties: +i) any finite union of subsets of belongs to ; +ii) any finite intersection of subsets of belongs to . +Subets of are called open sets of family .

Here is a code snippet in Coq for this classical definition.

Structure topology (A : Type) := { open :> (A -> Prop) -> Prop; empty_open: open (empty _); full_open: open (full _); @@ -149,15 +149,15 @@ where topos is defined as category of sheaves on a Grothendieck site with geometric moriphisms as adjoint pairs of functors between topoi, that satisfy exactness properties.

As this flavour of topos theory uses category of sets as a prerequisite, -the formal construction of set topos is cricual in doing sheaf topos theory.

(Sieves). Sieves are a family of subfunctors

such that following axioms hold: i) (base change) If is covering -and is a morphism of , then the subfuntor

is covering for ; ii) (local character) Suppose that are -subfunctors and R is covering. If is covering for -all in , then is covering; iii) - is covering for all .

(Coverage). A coverage is a function assigning -to each the family of morphisms called -covering families, such that for any exist -a covering family such that -each composite factors some :

Co (C: precategory) (cod: carrier C) : U +the formal construction of set topos is cricual in doing sheaf topos theory.

(Sieves). Sieves are a family of subfunctors

such that following axioms hold: i) (base change) If is covering +and is a morphism of , then the subfuntor

is covering for ; ii) (local character) Suppose that are +subfunctors and R is covering. If is covering for +all in , then is covering; iii) + is covering for all .

(Coverage). A coverage is a function assigning +to each the family of morphisms called +covering families, such that for any exist +a covering family such that +each composite factors some :

Co (C: precategory) (cod: carrier C) : U = (dom: carrier C) * (hom C dom cod) @@ -169,55 +169,55 @@ = (cod: carrier C) * (fam: Delta C cod) * (coverings: carrier C -> Delta C cod -> U) - * (coverings cod fam)

(Grothendieck Topology). Suppose category has all pullbacks. -Since is small, a pretopology on consists of families of sets of -morphisms

called covering families, such that following axioms hold: -i) suppose that is a covering family -and that is a morphism of . -Then the collection is a cvering family for . -ii) If is covering, -and -is covering for all , then the family of composites

is covering; -iii) The family is covering for all .

(Site). Site is a category having either a coverage, + * (coverings cod fam)

(Grothendieck Topology). Suppose category has all pullbacks. +Since is small, a pretopology on consists of families of sets of +morphisms

called covering families, such that following axioms hold: +i) suppose that is a covering family +and that is a morphism of . +Then the collection is a cvering family for . +ii) If is covering, +and +is covering for all , then the family of composites

is covering; +iii) The family is covering for all .

(Site). Site is a category having either a coverage, grothendieck topology, or sieves.

site (C: precategory): U = (C: precategory) - * Coverage C

(Presheaf). Presheaf of a category + * Coverage C

(Presheaf). Presheaf of a category is a functor from opposite category to category of sets: -.

presheaf (C: precategory): U - = catfunctor (opCat C) Set

(Presheaf Category, ). -Presheaf category for a site is category +.

presheaf (C: precategory): U + = catfunctor (opCat C) Set

(Presheaf Category, ). +Presheaf category for a site is category were objects are presheaves and morphisms are natural transformations -of presheaf functors.

(Sheaf). Sheaf is a presheaf on a site. In other words -a presheaf such that the -cannonical map of inverse limit

is an isomorphism for each covering sieve . -Equivalently, all induced functions

should be bijections.

sheaf (C: precategory): U +of presheaf functors.

(Sheaf). Sheaf is a presheaf on a site. In other words +a presheaf such that the +cannonical map of inverse limit

is an isomorphism for each covering sieve . +Equivalently, all induced functions

should be bijections.

sheaf (C: precategory): U = (S: site C) - * presheaf S.1

(Sheaf Category, ). Sheaf category + * presheaf S.1

(Sheaf Category, ). Sheaf category is a category where objects are sheaves and morphisms are natural transformation of sheves. Sheaf category is a full subcategory -of category of presheaves .

(Grothendieck Topos). Topos is the category -of sheaves on a site with topology .

(Giraud). A category is a Grothiendieck topos if +of category of presheaves .

(Grothendieck Topos). Topos is the category +of sheaves on a site with topology .

(Giraud). A category is a Grothiendieck topos if it has following properties: i) has all finite limits; ii) has small disjoint coproducts stable under pullbacks; iii) any epimorphism is coequalizer; -iv) any equivalence relation is a kernel pair and has a quotient; -v) any coequalizer is stably exact; -vi) there is a set of objects that generates .

(Geometric Morphism). Suppose that and -are Grothendieck sites. A geometric morphism

consists of functors and - such that is -left adjoint to and preserves finite limits. The left adjoint is called -the inverse image functor, while is called the direct image. The inverse image functor - is left and right exact in the sense that it preserves all finite -colimits and limits, respectively.

(Point of a Topos). -A point of a topos is a geometric morphism: .

(Stalk). -The stalk at of an object is the image of under +iv) any equivalence relation is a kernel pair and has a quotient; +v) any coequalizer is stably exact; +vi) there is a set of objects that generates .

(Geometric Morphism). Suppose that and +are Grothendieck sites. A geometric morphism

consists of functors and + such that is +left adjoint to and preserves finite limits. The left adjoint is called +the inverse image functor, while is called the direct image. The inverse image functor + is left and right exact in the sense that it preserves all finite +colimits and limits, respectively.

(Point of a Topos). +A point of a topos is a geometric morphism: .

(Stalk). +The stalk at of an object is the image of under corresponding inverse image morphism -.

(Étale space é). -Let a topological space, a category and is a -valued presheaf on . -Then, the étalé space is a a pair É where: -i) É is a disjoin union of stalks of ; -ii) É is the canonical projection. +.

(Étale space é). +Let a topological space, a category and is a -valued presheaf on . +Then, the étalé space is a a pair É where: +i) É is a disjoin union of stalks of ; +ii) É is the canonical projection.

Elementary Topos

Giraud theorem was a synonymical topos definition that involved only topos properties but not site properties. That was a step forward in predicative definition. The other step was made by Lawvere and Tierney, @@ -231,15 +231,15 @@ theory is more suited for logic needs rather than for geometry, as its set properties are hidden under predicative pullback definition of subobject classifier rather than functorial notation of presheaf functor. So we can simplify proofs -at the homotopy levels, not to lift everything to 2-categorical model.

(Monomorphism). A morphism is a monic or mono -if for any object and every pair of parralel morphisms the

More abstractly, f is mono if for any the takes it to an injective -function between hom sets .

mono (P: precategory) (Y Z: carrier P) (f: hom P Y Z): U +at the homotopy levels, not to lift everything to 2-categorical model.

(Monomorphism). A morphism is a monic or mono +if for any object and every pair of parralel morphisms the

More abstractly, f is mono if for any the takes it to an injective +function between hom sets .

mono (P: precategory) (Y Z: carrier P) (f: hom P Y Z): U = (X: carrier P) (g1 g2: hom P X Y) -> Path (hom P X Z) (compose P X Y Z g1 f) (compose P X Y Z g2 f) - -> Path (hom P X Y) g1 g2

(Subobject Classifier). In category with finite limits, -a subobject classifier is a monomorphism out of terminal -object , such that for any mono there is a unique -morphism and a pullback diagram:

subobjectClassifier (C: precategory): U + -> Path (hom P X Y) g1 g2

(Subobject Classifier). In category with finite limits, +a subobject classifier is a monomorphism out of terminal +object , such that for any mono there is a unique +morphism and a pullback diagram:

subobjectClassifier (C: precategory): U = (omega: carrier C) * (end: terminal C) * (trueHom: hom C end.1 omega) @@ -249,21 +249,21 @@ * ((V X: carrier C) (j: hom C V X) (k: hom C X omega) -> mono C V X j -> hasPullback C (omega,(end.1,trueHom),(X,k)) - -> Path (hom C X omega) (chi V X j) k)

(Category of Sets has Subobject Classifier).

(Cartesian Closed Categories). -The category is called cartesian closed if exists all: + -> Path (hom C X omega) (chi V X j) k)

(Category of Sets has Subobject Classifier).

(Cartesian Closed Categories). +The category is called cartesian closed if exists all: i) terminals; ii) products; iii) exponentials. Note that this definition -lacks beta and eta rules which could be found in embedding .

isCCC (C: precategory): U +lacks beta and eta rules which could be found in embedding .

isCCC (C: precategory): U = (Exp: (A B: carrier C) -> carrier C) * (Prod: (A B: carrier C) -> carrier C) * (Apply: (A B: carrier C) -> hom C (Prod (Exp A B) A) B) * (P1: (A B: carrier C) -> hom C (Prod A B) A) * (P2: (A B: carrier C) -> hom C (Prod A B) B) * (Term: terminal C) - * unit

(Category of Sets has Cartesian Closure). As you can see -from exp and pro we internalize and types as instances, -the predicates are provided with contractability. -Exitense of terminals is proved by . The same technique you -can find in embedding.

cartesianClosure : isCCC Set + * unit

(Category of Sets has Cartesian Closure). As you can see +from exp and pro we internalize and types as instances, +the predicates are provided with contractability. +Exitense of terminals is proved by . The same technique you +can find in embedding.

cartesianClosure : isCCC Set = (expo,prod,appli,proj1,proj2,term,tt) where exp (A B: SET): SET = (A.1 -> B.1, setFun A.1 B.1 B.2) pro (A B: SET): SET = (prod A.1 B.1, @@ -277,12 +277,12 @@ unitContr (x: SET) (f: x.1 -> unit) : isContr (x.1 -> unit) = (f, \(z: x.1 -> unit) -> propPi x.1 (\(_:x.1)->unit) (\(x:x.1) ->propUnit) f z) term: terminal Set = ((unit,setUnit),\(x: SET) -> unitContr x (\(z: x.1) -> tt))

Note that rules of cartesian closure form a type theoretical language -called lambda calculus.

elementary Topos). Topos is a precategory which is +called lambda calculus.

elementary Topos). Topos is a precategory which is cartesian closed and has subobject classifier.

Topos (cat: precategory) : U = (cartesianClosure: isCCC cat) - * subobjectClassifier cat

(Topos Definitions). Any Grothendieck topos is an elementary topos too. -The proof is sligthly based on results of Giraud theorem.

(Category of Sets forms a Topos). There is a + * subobjectClassifier cat

(Topos Definitions). Any Grothendieck topos is an elementary topos too. +The proof is sligthly based on results of Giraud theorem.

(Category of Sets forms a Topos). There is a cartesian closure and subobject classifier for a categoty of sets.

internal : Topos Set = (cartesianClosure,hasSubobject)

Literature

[70]. P.T. Johnstone. Topos Theory. 2014, diff --git a/mathematics/geometry/bundle/index.html b/mathematics/geometry/bundle/index.html index 25e6850d..eae76c67 100644 --- a/mathematics/geometry/bundle/index.html +++ b/mathematics/geometry/bundle/index.html @@ -11,31 +11,31 @@ Bundle package contains basic information about fibers (needed for weak-equivalence) and fiber bundles, constructions from algebraic topology. -

Fiber

(Fiber). The fiber of the map in a point -is all points such that .

fiber (E B: U) (p: E -> B) (y: B): U +

Fiber

(Fiber). The fiber of the map in a point +is all points such that .

fiber (E B: U) (p: E -> B) (y: B): U = (x: E) * Path B y (p x) -

Fiber Bundle

(Fiber Bundle). The fiber bundle on a -total space with fiber layer and base is a -structure where is a surjective +

Fiber Bundle

(Fiber Bundle). The fiber bundle on a +total space with fiber layer and base is a +structure where is a surjective map with following property: -for any point exists a neighborhood for which a -homeomorphism -making the following diagram commute.

-

Trivial Fiber Bundle

(Trivial Fiber Bundle). -When total space is cartesian product -and then such bundle is called trivial .

Family (B: U): U = B -> U +for any point exists a neighborhood for which a +homeomorphism +making the following diagram commute.

+

Trivial Fiber Bundle

(Trivial Fiber Bundle). +When total space is cartesian product +and then such bundle is called trivial .

Family (B: U): U = B -> U total (B: U) (F: Family B): U = Sigma B F trivial (B: U) (F: Family B): total B F -> B = \ (x: total B F) -> x.1 homeo (B E: U) (F: Family B) (p: E -> B) (y: B) : fiber E B p y -> total B F -

Fiber is a Dependent Family

(Fiber in a trivial total space is a family over base). -Inverse image (fiber) of fiber bundle in point equals . +

Fiber is a Dependent Family

(Fiber in a trivial total space is a family over base). +Inverse image (fiber) of fiber bundle in point equals . Thre proof sketch is following:

F y = (_: isContr B) * (F y) = (x y: B) * (_: Path B x y) * (F y) = (z: B) * (k: F z) * Path B z y = (z: E) * Path B z.1 y - = fiber (total B F) B (trivial B F) y

The equality is proven by lemma and functions.

encode (B: U) (F: B -> U) (y: B) + = fiber (total B F) B (trivial B F) y

The equality is proven by lemma and functions.

encode (B: U) (F: B -> U) (y: B) : fiber (total B F) B (trivial B F) y -> F y = \ (x: fiber (total B F) B (trivial B F) y) -> subst B F x.1.1 y (<i>x.2@-i) x.1.2 @@ -61,6 +61,6 @@ g: A -> T = decode B F y s (x: A): Path A (f (g x)) x = lem2 B F y x t (x: T): Path T (g (f x)) x = lem3 B F y x -

G-structure

The structure group of an -fiber bundle is just , -the loop space of . +

G-structure

The structure group of an -fiber bundle is just , +the loop space of .

\ No newline at end of file diff --git a/mathematics/geometry/derham/index.html b/mathematics/geometry/derham/index.html index 9db692ff..a5d6efee 100644 --- a/mathematics/geometry/derham/index.html +++ b/mathematics/geometry/derham/index.html @@ -7,53 +7,53 @@ use[data-c]{stroke-width:3px} DE RHAM

DE RHAM

(Cohesive -Topos). -An -Topos which is local and -connected is called cohesive. +DERHAM

DE RHAM

(Cohesive -Topos). +An -Topos which is local and -connected is called cohesive. Here is very short intro to de Rham cohesion built on -top of and modalities. -

(Cohesive -Topos). -An -Topos which is local and -connected is called cohesive. -

(de Rham shape modality). +top of and modalities. +

(Cohesive -Topos). +An -Topos which is local and -connected is called cohesive. +

(de Rham shape modality). de Rham cohesive homotopy type of A is defined as a homotopy cofiber of the unit of the shape modality: -

+

or the (looping opetaion of) the cokernel of the unit of the shape modality. It is also called de Rham shape modality. -

-

(de Rham flat modality). +

+

(de Rham flat modality). de Rham complex with coefficients in A is defined as the homotopy fiber of the counit of the flat modality: -

+

or the (delooping opetaion of) the cokernel of the unit of the shape modality. It is also called de Rham flat modality. -

-

The object A is called de Rham coefficient object of . -

(Loop Space Object). -Loop space objects are defined in any -category -with homotopy pullbacks: for any pointed object of -with point , its loop space object is the homotopy pullback - of this point along itself: -

-

(Delooping). -if is given and a homotopy pullback diagram -

-

exists, with the point -being essentially unique, by the above has been -realized as the loop space object of . - is called delooping of X: -

-

(Milnor–Lurie). +

+

The object A is called de Rham coefficient object of . +

(Loop Space Object). +Loop space objects are defined in any -category +with homotopy pullbacks: for any pointed object of +with point , its loop space object is the homotopy pullback + of this point along itself: +

+

(Delooping). +if is given and a homotopy pullback diagram +

+

exists, with the point +being essentially unique, by the above has been +realized as the loop space object of . + is called delooping of X: +

+

(Milnor–Lurie). There is an adjoint functor -

-

between -groups of and uniquely pointed -connected objects in which are doneted . -Where is a looping and is a delooping operations. -

(Maurer-Cartan form). -For and -group in the cohesive --topos Maurer-Cartan form is defines as -

-

for the -valued de Rham cocycle on induced by pullback pasting: -

+

+

between -groups of and uniquely pointed +connected objects in which are doneted . +Where is a looping and is a delooping operations. +

(Maurer-Cartan form). +For and -group in the cohesive +-topos Maurer-Cartan form is defines as +

+

for the -valued de Rham cocycle on induced by pullback pasting: +

LITERATURE

[1]. Urs Schreiber. Differential cohomology in a cohesive ∞-topos

\ No newline at end of file diff --git a/mathematics/homotopy/cw/index.html b/mathematics/homotopy/cw/index.html index 1d8e9336..d7843bd1 100644 --- a/mathematics/homotopy/cw/index.html +++ b/mathematics/homotopy/cw/index.html @@ -17,22 +17,22 @@ higher inductive types could be described as CW-complexes. Defining HIT means to define some CW-complex directly using cubical homogeneous composition structure as an -element of initial algebra inside cubical model.

(HIT). With a given context variables +element of initial algebra inside cubical model.

(HIT). With a given context variables Δ,K ⊢ (Γ,Ξ,Ψ,𝜑,𝑒) and telescope (𝛿 : Δ) (𝑖 : 𝕀) (𝜑 : 𝔽) (𝑢₀: H 𝛿 [𝜑 ↦ 𝑢[0/𝑖]]) every HIT is defines as: 1) ctorⁱ (𝛾: Γⁱ [𝛿]) (𝑥: Ξⁱ [𝛿,𝛾] → H 𝛿) (s: Ψₓ) : H 𝛿 [𝜑ₛ ↦ 𝑒[𝛾,𝑥]]; 2) hcompⁱ [𝜑 ↦ 𝑢] 𝑢₀ : H 𝛿 [𝜑 ↦ 𝑢[1/𝑖]]; -3) transpⁱ 𝜑 𝑢₀ : H 𝛿 [1] [𝜑 ↦ 𝑢₀].

. One of the notables is pushout as it's used +3) transpⁱ 𝜑 𝑢₀ : H 𝛿 [1] [𝜑 ↦ 𝑢₀].

. One of the notables is pushout as it's used to define the cell attachment formally, as others cofibrant objects.

data pushout (A B C: U) (f: C -> A) (g: C -> B) = po1 (_: A) | po2 (_: B) | po3 (c: C) <i> [ (i = 0) -> po1 (f c) , - (i = 1) -> po2 (g c) ]

. Here are some examples of using + (i = 1) -> po2 (g c) ]

. Here are some examples of using dimensions to construct spherical shapes.

data S1 = base | loop <i> [ (i = 0) -> base, (i = 1) -> base ]
data S2 = point | surf <i j> [ (i = 0) -> point, (i = 1) -> point, (j = 0) -> point, (j = 1) -> point ]
data D3 (x: S2) = border (x: S2) | space <i j k> [ ( i = 0) -> border x, (i = 1) -> border x , ( j = 0) -> border x, (j = 1) -> border x , - ( k = 0) -> border x, (k = 1) -> border x ]

. Structure of same as of . ASCII proof + ( k = 0) -> border x, (k = 1) -> border x ]

. Structure of same as of . ASCII proof that comp parameters are the same as in surf constructor:

I2 (A: U) (a0 a1 b0 b1: A) (u: Path A a0 a1) (v: Path A b0 b1) (r0: Path A a0 b0) (r1: Path A a1 b1) : U = PathP (<i> (PathP (<j> A) (u@i) (v@i))) r0 r1 @@ -52,25 +52,25 @@ This decomposition is intended to solve the problem of interpretation of higher inductive types with parameters.

MATHEMATICS

In definition of homotopy groups, a special role belongs -to inclusions . We study spaces -obtained through iterated attachments of along . -

(Attachment). Attaching n-cell to a space -along a map means taking a pushout -

-

where the notation means that the result depends -on homotopy class of . -

(CW-Complex). Inductively. The only -CW-complex of dimention is . -A CW-complex of dimension on is a -space obtained by attaching a collection of n-cells -to a CW-complex of dimension . -

A CW-complex is a space which is the colimit(X_i) of a -sequence of -CW-complexes of dimension , with -obtained from by i-cell attachments. +to inclusions . We study spaces +obtained through iterated attachments of along . +

(Attachment). Attaching n-cell to a space +along a map means taking a pushout +

+

where the notation means that the result depends +on homotopy class of . +

(CW-Complex). Inductively. The only +CW-complex of dimention is . +A CW-complex of dimension on is a +space obtained by attaching a collection of n-cells +to a CW-complex of dimension . +

A CW-complex is a space which is the colimit(X_i) of a +sequence of +CW-complexes of dimension , with +obtained from by i-cell attachments. Thus if X is a CW-complex, it comes with a filtration - -where is a CW-complex of dimension called + +where is a CW-complex of dimension called the i-skeleton, and hence the filtration is called the skeletal filtration.

\ No newline at end of file diff --git a/mathematics/homotopy/hopf/index.html b/mathematics/homotopy/hopf/index.html index 3da5c1e0..8bea1122 100644 --- a/mathematics/homotopy/hopf/index.html +++ b/mathematics/homotopy/hopf/index.html @@ -6,28 +6,28 @@ .mjx-dotted{stroke-linecap:round;stroke-dasharray:0,140} use[data-c]{stroke-width:3px} HOPF

Hopf Fibrations

The geometric and topological interpretation

HOPF

This article defines the Hopf Fibration (HF), the concept -of splitting the sphere onto the twisted cartesian product -of spheres and . +of splitting the sphere onto the twisted cartesian product +of spheres and . Basic HF applications are: 1) HF is a Fiber Bundle structure of Dirac Monopole; -2) HF is a map from the in H to the Bloch sphere; -3) If HF is a vector field in then there exists a solution +2) HF is a map from the in H to the Bloch sphere; +3) If HF is a vector field in then there exists a solution to compressible non-viscous Navier-Stokes equations. It was figured out that there are only 4 dimensions of fibers with Hopf invariant 1, namely -, , , .

This article consists of two parts: -1) geometric visualization of projection of to (frontend); +, , , .

This article consists of two parts: +1) geometric visualization of projection of to (frontend); 2) formal topological version of HF in cubical type theory (backend). Consider this a basic intro and a summary of results or companion guide to the chapter 8.5 from HoTT. -

Geometry

Let’s imagine as smooth differentiable manifold and build +

Geometry

Let’s imagine as smooth differentiable manifold and build a projection onto the display as if demoscene is still alive. -

Equations

Definition (Sphere ). Like a little baby in :after math classes in quaternions : -

Definition (Locus). The is realized as a disjoint -union of circular fibers in Hopf coordinates , -where and :

Definition (Mapping on ). -A mapping of the Locus to the has points on the circles -parametrized by :

Code in three.js:

var fiber = new THREE.Curve(), +

Equations

Definition (Sphere ). Like a little baby in :after math classes in quaternions : +

Definition (Locus). The is realized as a disjoint +union of circular fibers in Hopf coordinates , +where and :

Definition (Mapping on ). +A mapping of the Locus to the has points on the circles +parametrized by :

Code in three.js:

var fiber = new THREE.Curve(), color = sphericalCoords.color; fiber.getPoint = function(t) { @@ -44,49 +44,49 @@ };

Topology

Can we reason about spheres without a metric? Yes! But can we do this in a constructive way? Also yes. -

Fiber

Definition (Fiber). The fiber of the map in a point -is all points such that .

fiber (E B: U) (p: E -> B) (y: B): U +

Fiber

Definition (Fiber). The fiber of the map in a point +is all points such that .

fiber (E B: U) (p: E -> B) (y: B): U = (x: E) * Path B y (p x) -

Fiber Bundle

Definition (Fiber Bundle). The fiber bundle on a -total space with fiber layer and base is a -structure where is a surjective +

Fiber Bundle

Definition (Fiber Bundle). The fiber bundle on a +total space with fiber layer and base is a +structure where is a surjective map with following property: -for any point exists a neighborhood for which a -homeomorphism +for any point exists a neighborhood for which a +homeomorphism making the following diagram commute. - +

Trivial Fiber Bundle

Definition (Trivial Fiber Bundle). -When total space is cartesian product -and then such bundle is called trivial .

Family (B: U): U = B -> U +When total space is cartesian product +and then such bundle is called trivial .

Family (B: U): U = B -> U total (B: U) (F: Family B): U = Sigma B F trivial (B: U) (F: Family B): total B F -> B = \ (x: total B F) -> x.1

Theorem (Fiber Bundle is a Type Family). -Inverse image (fiber) of fiber bundle in point equals .

FiberPi (B: U) (F: B -> U) (y: B) +Inverse image (fiber) of fiber bundle in point equals .

FiberPi (B: U) (F: B -> U) (y: B) : Path U (fiber (total B F) B (trivial B F) y) (F y)

Definition (Structure Group). The structure group of -an -fiber bundle is just Aut(F), the loop space of BAut(F). -

Higher Spheres

Definition (2-points, Bool, Sphere ).

data bool = false | true +an -fiber bundle is just Aut(F), the loop space of BAut(F). +

Higher Spheres

Definition (2-points, Bool, Sphere ).

data bool = false | true

Definition (Suspension).

data susp (A: U) = north | south | merid (a: A) <i> [ (i = 0) -> north, - (i = 1) -> south ]

Definition (Sphere ). Direct definition.

data S1 + (i = 1) -> south ]

Definition (Sphere ). Direct definition.

data S1 = base | loop <i> [ (i = 0) -> base, (i = 1) -> base ] -

Definition (Sphere ). Recursive definition.

S: nat -> U = split +

Definition (Sphere ). Recursive definition.

S: nat -> U = split zero -> bool succ x -> susp (S x) S2: U = susp S1 S3: U = susp S2 S4: U = susp S3 -

Hopf Fibrations

Theorem (Hopf Fibrations). There are fiber bundles:

Definition (H-space). H-space over a carrier is a tuple.

Example ( Hopf Fiber ). Mobius fiber. +

Hopf Fibrations

Theorem (Hopf Fibrations). There are fiber bundles:

Definition (H-space). H-space over a carrier is a tuple.

Example ( Hopf Fiber ). Mobius fiber. In cubicaltt type checker.

moebius : S1 -> U = split base -> bool loop @ i -> ua bool bool negBoolEquiv @ i -H0 : U = (c : S1) * moebius c

Example ( Hopf Fiber ). Guillaume Brunerie. +H0 : U = (c : S1) * moebius c

Example ( Hopf Fiber ). Guillaume Brunerie. In cubicaltt type checker.

rot: (x : S1) -> Path S1 x x = split base -> loop1 loop @ i -> constSquare S1 base loop1 @ i @@ -101,7 +101,7 @@ south -> S1 merid x @ i -> ua S1 S1 (mu x) @ i -total : U = (c : S2) * H c

Example ( Hopf Fiber ). By Egbert Rijke and Ulrik Buchholtz. +total : U = (c : S2) * H c

Example ( Hopf Fiber ). By Egbert Rijke and Ulrik Buchholtz. In Lean prover.

definition pfiber_quaternionic_phopf : pfiber quaternionic_phopf ≃* S* 3 := begin @@ -113,13 +113,13 @@ refine fiber.equiv_precompose _ (hopf.total (S 3))− 1 e _ ·e _, apply fiber_pr1 }, { reflexivity } -end

Definition (Hopf Invariant). Let a continuous map. -Then homotopy pushout (cofiber) of is has -ordinary cohomologyHence for generators of the cohomology groups in -degree and , respectively, there exists an integer -that expresses the cup product square of -as a multiple of — . -This integer is called Hopf invariant of .

Theorem (Adams, Atiyah). Hopf Fibrations are only -maps that have Hopf invariant . +end

Definition (Hopf Invariant). Let a continuous map. +Then homotopy pushout (cofiber) of is has +ordinary cohomologyHence for generators of the cohomology groups in +degree and , respectively, there exists an integer +that expresses the cup product square of +as a multiple of — . +This integer is called Hopf invariant of .

Theorem (Adams, Atiyah). Hopf Fibrations are only +maps that have Hopf invariant .

Literature

[1]. Ulrik Buchholtz, Egbert Rijke. The Cayley-Dickson Construction in Homotopy Type Theory


\ No newline at end of file diff --git a/mathematics/homotopy/pullback/index.html b/mathematics/homotopy/pullback/index.html index eb1a1b3e..61b0f77b 100644 --- a/mathematics/homotopy/pullback/index.html +++ b/mathematics/homotopy/pullback/index.html @@ -9,10 +9,10 @@ LIB LIMIT

PULLBACK

Pullback package contains basic information about Homotopy Limits known as Pullbacks. -

Definitions

(Homotopy Pullback). -The pullback of the first diagram (which is called cospan)

is a -together with the projection maps making the second -diagram commute up to homotopy .

pullback (A B C:U) (f: A -> C) (g: B -> C): U +

Definitions

(Homotopy Pullback). +The pullback of the first diagram (which is called cospan)

is a +together with the projection maps making the second +diagram commute up to homotopy .

pullback (A B C:U) (f: A -> C) (g: B -> C): U = (a: A) * (b: B) * Path C (f a) (g b) pb1 (A B C: U) (f: A -> C) (g: B -> C) @@ -22,11 +22,11 @@ pb3 (A B C: U) (f: A -> C) (g: B -> C) : (x: pullback A B C f g) -> Path C (f x.1) (g x.2.1) = \(x: pullback A B C f g) -> x.2.2 -

> (Homotopy Pullback Square). A homotopy pullback or cospan +

> (Homotopy Pullback Square). A homotopy pullback or cospan is called a homotopy pullback square if there exists a homotopy -equivalence satisfying - -and . Map is called induced map.

induced (Z A B C: U) (f: A -> C) (g: B -> C) +equivalence satisfying + +and . Map is called induced map.

induced (Z A B C: U) (f: A -> C) (g: B -> C) (z1: Z -> A) (z2: Z -> B) (h: (z:Z) -> Path C ((o Z A C f z1) z) (((o Z B C g z2)) z)) : Z -> pullback A B C f g @@ -38,7 +38,7 @@ isPullbackSq (Z A B C: U) (f: A -> C) (g: B -> C) (z1: Z -> A) (z2: Z -> B) (h: (z:Z) -> Path C ((o Z A C f z1) z) (((o Z B C g z2)) z)): U - = isEquiv Z (pullback A B C f g) (induced Z A B C f g z1 z2 h)

(Existence of Pullback Square). + = isEquiv Z (pullback A B C f g) (induced Z A B C f g z1 z2 h)

(Existence of Pullback Square). Pullback Square exists and equals Pullback, where induced map is identity. Given as 2.11 Exercise in HoTT Chapter 2.

completePullback (A B C: U) (f: A -> C) (g: B -> C) : pullbackSq (pullback A B C f g) A B C f g (pb1 A B C f g) (pb2 A B C f g) diff --git a/mathematics/homotopy/pushout/index.html b/mathematics/homotopy/pushout/index.html index 096418e7..89b1dc88 100644 --- a/mathematics/homotopy/pushout/index.html +++ b/mathematics/homotopy/pushout/index.html @@ -7,23 +7,23 @@ use[data-c]{stroke-width:3px} PUSHOUT

PUSHOUT

(Span). -The two maps with the same domain are called span:

(Homotopy Pushout). -The homotopy pushout or homotopy colimit (denoted as ) -of the span diagram:

where is an equivalence relation and -for . If is a based space with basepoint , we -add the relation for all .

data pushout (A B C: U) (f: C -> A) (g: C -> B) +COLIMIT

PUSHOUT

(Span). +The two maps with the same domain are called span:

(Homotopy Pushout). +The homotopy pushout or homotopy colimit (denoted as ) +of the span diagram:

where is an equivalence relation and +for . If is a based space with basepoint , we +add the relation for all .

data pushout (A B C: U) (f: C -> A) (g: C -> B) = po1 (_: A) | po2 (_: B) | po3 (c: C) <i> [ (i = 0) -> po1 (f c) , - (i = 1) -> po2 (g c) ]

EXAMPLES

(Homotopy Fibers).

hofiber (A B: U) (f: A -> B) (y: B): U + (i = 1) -> po2 (g c) ]

EXAMPLES

(Homotopy Fibers).

hofiber (A B: U) (f: A -> B) (y: B): U = pullback A unit B f (\(x: unit) -> y) -

(Fiber Pullback).

fiberPullback (A B: U) (f: A -> B) (y: B) +

(Fiber Pullback).

fiberPullback (A B: U) (f: A -> B) (y: B) : pullbackSq (hofiber A B f y) -

(Homotopy Cofiber).

cofiber (A B: U) (f: B -> A): U +

(Homotopy Cofiber).

cofiber (A B: U) (f: B -> A): U = pushout A unit B f (\(x: B) -> tt) -

(Kernel).

kernel (A B: U) (f: A -> B): U +

(Kernel).

kernel (A B: U) (f: A -> B): U = pullback A A B f f -

(Cokernel).

cokernel (A B: U) (f: B -> A): U +

(Cokernel).

cokernel (A B: U) (f: B -> A): U = pushout A A B f f

LITERATURE

[1]. Brian Munson and Ismar Volić. Cubical Homotopy Theory

\ No newline at end of file diff --git a/spec/index.html b/spec/index.html index 0eeaeca7..72bf5b7c 100644 --- a/spec/index.html +++ b/spec/index.html @@ -7,20 +7,20 @@ use[data-c]{stroke-width:3px} SPECIFICATION

BINARY FORMAT

Here is given a preliminary specification on Anders external term format.

is a byte.
- (from qword) is a 64-bit little-endian integer constisting of 4 bytes.
- is a UTF-8 string encoded as its length followed by the string itself. - In a BNF-like notation this written as
- represents here string (given by Z.to_bits function) that encodes Zarith integer.
- is a ident, - where first part represents ignored variable (like in ).
- represents interval elements ( and respectively).
- is a face.
- is a language expression.
- is a cubical system. -

COSMOS

-

ΠΣ

-

INTERVAL

-

KAN

+SPEC

BINARY FORMAT

Here is given a preliminary specification on Anders external term format.

is a byte.
+ (from qword) is a 64-bit little-endian integer constisting of 4 bytes.
+ is a UTF-8 string encoded as its length followed by the string itself. + In a BNF-like notation this written as
+ represents here string (given by Z.to_bits function) that encodes Zarith integer.
+ is a ident, + where first part represents ignored variable (like in ).
+ represents interval elements ( and respectively).
+ is a face.
+ is a language expression.
+ is a cubical system. +

COSMOS

+

ΠΣ

+

INTERVAL

+

KAN

\ No newline at end of file