nLab
cohesive homotopy type theory with two kinds of types
Contents
under construction
Contents
Introduction
In Shulman18 , the authors write
One might argue that it would be better to include a separate kind of type representing objects in the base category, and type constructors represent-ing the functors p * p_* , p * p^* , etc. rather than the monads and comonads they induce. This would be in line with the “judgmental deconstruction” of Reed (2009) that decomposes □ \Box and ◯ \bigcirc into pairs of adjoint functors. It could be that this is indeed better; in fact, the current rules for ♭ \flat and ♯ \sharp were deduced from a generalization of Reed (2009) developed by Licata and Shulman (2016).
This is an attempt at developing such a cohesive homotopy type theory .
Overview
This presentation of cohesive homotopy type theory is a dependent type theory consisting of two different kinds of types , spaces and homotopy types . There exist judgments
for spaces
Γ Γ ⊢ S space \frac{\Gamma}{\Gamma \vdash S\ space}
for homotopy types
Γ Γ ⊢ T homotopy type \frac{\Gamma}{\Gamma \vdash T\ homotopy\ type}
for points
Γ ⊢ S space Γ ⊢ s : S \frac{\Gamma \vdash S\ space}{\Gamma \vdash s:S}
for terms
Γ ⊢ T homotopy type Γ ⊢ t : T \frac{\Gamma \vdash T\ homotopy\ type}{\Gamma \vdash t:T}
for fibrations
Γ ⊢ S space Γ , s : S ⊢ A ( s ) space \frac{\Gamma \vdash S\ space}{\Gamma, s:S \vdash A(s)\ space}
for dependent types
Γ ⊢ T homotopy type Γ , t : T ⊢ B ( t ) homotopy type \frac{\Gamma \vdash T\ homotopy\ type}{\Gamma, t:T \vdash B(t)\ homotopy\ type}
for sections
Γ ⊢ S space Γ , s : S ⊢ a ( s ) : A ( s ) \frac{\Gamma \vdash S\ space}{\Gamma, s:S \vdash a(s):A(s)}
for dependent terms
Γ ⊢ T homotopy type Γ , t : T ⊢ b ( t ) : B ( t ) \frac{\Gamma \vdash T\ homotopy\ type}{\Gamma, t:T \vdash b(t):B(t)}
Cohesive homotopy type theory has the following additional judgments, 2 for turning spaces into homotopy types and the other two for turning homotopy types into spaces:
Every space has an underlying homotopy type
Γ ⊢ S space Γ ⊢ p * ( S ) homotopy type \frac{\Gamma \vdash S\ space}{\Gamma \vdash p_*(S)\ homotopy\ type}
Every space has a fundamental homotopy type
Γ ⊢ S space Γ ⊢ p ! ( S ) homotopy type \frac{\Gamma \vdash S\ space}{\Gamma \vdash p_!(S)\ homotopy\ type}
Every homotopy type has a discrete space
Γ ⊢ T homotopy type Γ ⊢ p * ( T ) space \frac{\Gamma \vdash T\ homotopy\ type}{\Gamma \vdash p^*(T)\ space}
Every homotopy type has an indiscrete space
Γ ⊢ T homotopy type Γ ⊢ p ! ( T ) space \frac{\Gamma \vdash T\ homotopy\ type}{\Gamma \vdash p^!(T)\ space}
The underlying homotopy type and fundamental homotopy type are sometimes represented by the greek letters Γ \Gamma and Π \Pi respectively, but both are already used in dependent type theory to represent the context and the dependent product type .
Modalities
From these judgements one could construct the sharp modality as
♯ ( S ) ≔ p ! ( p * ( S ) ) \sharp(S) \coloneqq p^!(p_*(S))
the flat modality as
♭ ( S ) ≔ p * ( p * ( S ) ) \flat(S) \coloneqq p^*(p_*(S))
and the shape modality as
ʃ ( S ) ≔ p * ( p ! ( S ) ) \esh(S) \coloneqq p^*(p_!(S))
for a space S S .
Other types
Path spaces
Γ , a : S , b : S Γ ⊢ a = S b space \frac{\Gamma, a:S, b:S}{\Gamma \vdash a =_S b\ space}
Identity types
Γ , a : T , b : T Γ ⊢ a = T b homotopy type \frac{\Gamma, a:T, b:T}{\Gamma \vdash a =_T b\ homotopy\ type}
Mapping spaces
Γ , A space , B space Γ ⊢ A → B space \frac{\Gamma, A\ space, B\ space}{\Gamma \vdash A \to B\ space}
Function types
Γ , A homotopy type , B homotopy type Γ ⊢ A → B homotopy type \frac{\Gamma, A\ homotopy\ type, B\ homotopy\ type}{\Gamma \vdash A \to B\ homotopy\ type}
Section spaces
Γ , s : S ⊢ A ( s ) space Γ ⊢ ∏ s : S A ( s ) space \frac{\Gamma, s:S \vdash A(s)\ space}{\Gamma \vdash \prod_{s:S} A(s)\ space}
Dependent function types
Γ , t : T ⊢ A ( t ) homotopy type Γ ⊢ ∏ t : T A ( t ) homotopy type \frac{\Gamma, t:T \vdash A(t)\ homotopy\ type}{\Gamma \vdash \prod_{t:T} A(t)\ homotopy\ type}
Product spaces
Γ , A space , B space Γ ⊢ A × B space \frac{\Gamma, A\ space, B\ space}{\Gamma \vdash A \times B\ space}
Pair types
Γ , A homotopy type , B homotopy type Γ ⊢ A × B homotopy type \frac{\Gamma, A\ homotopy\ type, B\ homotopy\ type}{\Gamma \vdash A \times B\ homotopy\ type}
Total spaces
Γ , s : S ⊢ A ( s ) space Γ ⊢ ∑ s : S A ( s ) space \frac{\Gamma, s:S \vdash A(s)\ space}{\Gamma \vdash \sum_{s:S} A(s)\ space}
Dependent pair types
Γ , t : T ⊢ A ( t ) homotopy type Γ ⊢ ∑ t : T A ( t ) homotopy type \frac{\Gamma, t:T \vdash A(t)\ homotopy\ type}{\Gamma \vdash \sum_{t:T} A(t)\ homotopy\ type}
Unit space
Γ Γ ⊢ 𝟙 space \frac{\Gamma}{\Gamma \vdash \mathbb{1}\ space}
Unit type
Γ Γ ⊢ 𝟙 homotopy type \frac{\Gamma}{\Gamma \vdash \mathbb{1}\ homotopy\ type}
Other properties
The fundamental homotopy type of the unit space is equivalent to the unit type.
p ! ( 𝟙 ) ≅ 𝟙 p_!(\mathbb{1}) \cong \mathbb{1}
The product of the fundamental homotopy types of spaces A A and B B is equivalent to the fundamental homotopy type of the product of spaces A A and B B :
p ! ( A × B ) ≅ p ! ( A ) × p ! ( B ) p_!(A \times B) \cong p_!(A) \times p_!(B)
Sources
Created on June 19, 2022 at 23:30:27.
See the history of this page for a list of all contributions to it.