Homotopy Type Theory cohesive homotopy type theory > history (changes)

Showing changes from revision #19 to #20: Added | Removed | Changed



We use objective type theory? as the base type theory of cohesive types, and build the theory of crisp judgments on top of objective type theory.

\subsection{Judgments and contexts}

Cohesive homotopy type theory consists of the following judgments:

  • Type judgments, where we judge AA to be a type, AtypeA \; \mathrm{type}

  • Cohesive term judgments, where we judge aa to cohesively be an element of AA, a:Aa:A

  • Crisp term judgments, where we judge aa to crisply be an element of AA, a::Aa::A

  • Context judgments, where we judge Ξ|Γ\Xi \vert \Gamma to be a context, Ξ|Γctx\Xi \vert \Gamma \; \mathrm{ctx}.

Contexts are lists of crisp term judgments a::Aa::A, b::Bb::B, c::Cc::C, et cetera, followed by lists of cohesive variable judgments a:Aa:A, b:Bb:B, c:Cc:C, et cetera, and are formalized by the rules for the empty context and extending the context by a crisp or cohesive variable judgment

()|()ctxΞ|()ctxΞ|()Atype(Ξ,a::A)|()ctxΞ|ΓctxΞ|ΓAtypeΞ|(Γ,a:A)ctx\frac{}{() \vert () \; \mathrm{ctx}} \qquad \frac{\Xi \vert () \; \mathrm{ctx} \quad \Xi \vert () \vdash A \; \mathrm{type}}{(\Xi, a::A) \vert () \; \mathrm{ctx}} \qquad \frac{\Xi \vert \Gamma \; \mathrm{ctx} \quad \Xi \vert \Gamma \vdash A \; \mathrm{type}}{\Xi \vert (\Gamma, a:A) \; \mathrm{ctx}}

\subsection{Structural rules}

Within any dependent type theory, the structural rules include the variable rule?, the weakening rule?, and the substitution rule?. In cohesive homotopy type theory these rules are only for cohesive term judgments.

The variable rules state that we may derive a cohesive or crisp term judgment if the term judgment is in the context already:

Ξ,a::A,Δ|()ctxΞ,a::A,Δ|()a::AΞ|Γ,a:A,ΔctxΞ|Γ,a:A,Δa:A\frac{\Xi, a::A, \Delta \vert () \; \mathrm{ctx}}{\Xi, a::A, \Delta \vert () \vdash a::A} \quad \frac{\Xi \vert \Gamma, a:A, \Delta \; \mathrm{ctx}}{\Xi \vert \Gamma, a:A, \Delta \vdash a:A}

Let 𝒥\mathcal{J} be any arbitrary judgment. Then we have the following rules:

The weakening rules:

Ξ,Δ|()𝒥Ξ|()AtypeΞ,a::A,Δ|()𝒥Ξ|Γ,Δ𝒥Ξ|ΓAtypeΞ|Γ,a:A,Δ𝒥\frac{\Xi, \Delta \vert () \vdash \mathcal{J} \quad \Xi \vert () \vdash A \; \mathrm{type}}{\Xi, a::A, \Delta \vert () \vdash \mathcal{J}} \qquad \frac{\Xi \vert \Gamma, \Delta \vdash \mathcal{J} \quad \Xi \vert \Gamma \vdash A \; \mathrm{type}}{\Xi \vert \Gamma, a:A, \Delta \vdash \mathcal{J}}

The substitution rules:

Ξ|()a::AΞ,b::A,Δ|()𝒥Ξ,Δ[a/b]|()𝒥[a/b]Ξ|Γa:AΞ|Γ,b:A,Δ𝒥Ξ|Γ,Δ[a/b]𝒥[a/b]\frac{\Xi \vert () \vdash a::A \quad \Xi, b::A, \Delta \vert () \vdash \mathcal{J}}{\Xi, \Delta[a/b] \vert () \vdash \mathcal{J}[a/b]} \qquad \frac{\Xi \vert \Gamma \vdash a:A \quad \Xi \vert \Gamma, b:A, \Delta \vdash \mathcal{J}}{\Xi \vert \Gamma, \Delta[a/b] \vdash \mathcal{J}[a/b]}

The weakening and substitution rules are admissible rules: they do not need to be explicitly included in the type theory as they could be proven by induction on the structure of all possible derivations.

\subsection{Identity types}

  • Formation rule for identity types:
Ξ|ΓAtypeΞ|Γa:AΞ|Γb:AΞ|Γa= Abtype\frac{\Xi \vert \Gamma \vdash A \; \mathrm{type} \quad \Xi \vert \Gamma \vdash a:A \quad \Xi \vert \Gamma \vdash b:A}{\Xi \vert \Gamma \vdash a =_A b \; \mathrm{type}}
  • Introduction rule for identity types:
Ξ|ΓAtypeΞ|Γa:AΞ|Γrefl A(a):a= Aa\frac{\Xi \vert \Gamma \vdash A \; \mathrm{type} \quad \Xi \vert \Gamma \vdash a:A}{\Xi \vert \Gamma \vdash \mathrm{refl}_A(a) : a =_A a}
  • Elimination rule for identity types:

    Ξ|Γ,x:A,y:A,p:a= AbCtypeΞ|Γ,z:At:C[z/a,z/b,refl A(z)/p]Ξ|Γa:AΞ|Γb:AΞ|Γq:a= AbΞ|Γind = A x.y.p.C(z.t,a,b,q):C[a,b,q/x,y,p]\frac{\Xi \vert \Gamma, x:A, y:A, p:a =_A b \vdash C \; \mathrm{type} \quad \Xi \vert \Gamma, z:A \vdash t:C[z/a, z/b, \mathrm{refl}_A(z)/p] \quad \Xi \vert \Gamma \vdash a:A \quad \Xi \vert \Gamma \vdash b:A \quad \Xi \vert \Gamma \vdash q:a =_A b}{\Xi \vert \Gamma \vdash \mathrm{ind}_{=_A}^{x.y.p.C}(z.t, a, b, q):C[a, b, q/x, y, p]}
  • Computation rules for identity types:

    Ξ|Γ,x:A,y:A,p:a= AbCtypeΞ|Γ,z:At:C[z/a,z/b,refl A(z)/p]Ξ|Γa:AΞ|Γβ = A x.y.p.C(a):ind = A x.y.p.C(z.t,a,a,refl(a))= C[a,a,refl A(a)/x,y,p]t\frac{\Xi \vert \Gamma, x:A, y:A, p:a =_A b \vdash C \; \mathrm{type} \quad \Xi \vert \Gamma, z:A \vdash t:C[z/a, z/b, \mathrm{refl}_A(z)/p] \quad \Xi \vert \Gamma \vdash a:A}{\Xi \vert \Gamma \vdash \beta_{=_A}^{x.y.p.C}(a):\mathrm{ind}_{=_A}^{x.y.p.C}(z.t, a, a, \mathrm{refl}(a)) =_{C[a, a, \mathrm{refl}_A(a)/x, y, p]} t}

\section{Sharp modality}

  • Formation rule for sharp types:
Ξ,Γ|()AtypeΞ|ΓAtype\frac{\Xi, \Gamma \vert () \vdash A \; \mathrm{type}}{\Xi \vert \Gamma \vdash \sharp A \; \mathrm{type}}
  • Introduction rule for sharp types:
Ξ,Γ|()a:AΞ|Γa :A\frac{\Xi, \Gamma \vert () \vdash a:A}{\Xi \vert \Gamma \vdash a^\sharp:\sharp A}
  • Elimination rule for sharp types:
Ξ|()a:AΞ|Γa :A\frac{\Xi \vert () \vdash a:\sharp A}{\Xi \vert \Gamma \vdash a_\sharp:A}
  • Computation rule for sharp types:
Ξ|()a:AΞ|Γβ (a):(a ) = Aa\frac{\Xi \vert () \vdash a:A}{\Xi \vert \Gamma \vdash \beta_\sharp(a):(a^\sharp)_\sharp =_A a}
  • Uniqueness rule for sharp types:
Ξ|()a:AΞ|Γη (a):(a ) = Aa\frac{\Xi \vert () \vdash a:\sharp A}{\Xi \vert \Gamma \vdash \eta_\sharp(a):(a_\sharp)^\sharp =_{\sharp A} a}

\section{See also}


\section{External links}

Last revised on November 28, 2022 at 03:21:30. See the history of this page for a list of all contributions to it.