nLab objective type theory

Contents

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Deduction and Induction

Constructivism, Realizability, Computability

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axiom

Removing axioms

Contents

Idea

Objective type theory is a dependent type theory without judgmental equality.

This means that the computation and uniqueness rules (beta-reduction and eta-conversion) for each type in the type theory are all typal computational and uniqueness rules using the identity type, and in particular means that the identity type has to be introduced at the same time the dependent function type is introduced. As a result, the results in objective type theory are more general than in models which use judgmental equality for computational and uniqueness rules, since judgmental equality implies typal equality, while the converse isn’t necessarily the case.

In addition, objective type theory is similar to other non-type theory foundations such as the various flavors of set theory, since it also only has one notion of equality, propositional equality, and uses propositional equality in definitions.

Objective type theory has decidable type checking, and the type checking can be done in quadratic time.

Syntax

Judgments and contexts

Objective type theory consists of the following judgments:

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

  • Type definition judgments, where we judge BB to be defined as the type AA, BAtypeB \coloneqq A \; \mathrm{type}

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

  • Element definition judgments, where we judge bb to be defined as the term a:Aa:A, ba:Ab \coloneqq a:A

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

Contexts are lists of element 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 element judgment

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

Note that type and element definition judgments are not judgmental equalities; the former are single assignment operators while the latter are equivalence relations.

Structural rules

There are three structural rules in objective type theory, the variable rule?, the weakening rule, and the substitution rule.

The variable rule states that we may derive a element judgment if the element judgment is in the context already:

Γ,a:A,ΔctxΓ,a:A,Δa:A\frac{\Gamma, a:A, \Delta \; \mathrm{ctx}}{\Gamma, a:A, \Delta \vdash a:A}

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

The weakening rule:

Γ,Δ𝒥ΓAtypeΓ,a:A,Δ𝒥\frac{\Gamma, \Delta \vdash \mathcal{J} \quad \Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, \Delta \vdash \mathcal{J}}

The substitution rule:

Γa:AΓ,b:A,Δ(b)𝒥(b)Γ,Δ(a)𝒥(a)\frac{\Gamma \vdash a:A \quad \Gamma, b:A, \Delta(b) \vdash \mathcal{J}(b)}{\Gamma, \Delta(a) \vdash \mathcal{J}(a)}

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.

Families of types and elements

A family of types is a type BB in the context of the element judgment x:Ax:A, x:ABtypex:A \vdash B \; \mathrm{type}, they are usually written as B(x)B(x) to indicate its dependence upon xx. Given a particular element a:Aa:A, the type B(a)B(a) is a type dependent upon a:Aa:A.

A family of terms is a term b:Bb:B in the context of the variable judgment x:Ax:A, x:Ab:Bx:A \vdash b:B. They are likewise usually written as b(x)b(x) to indicate its dependence upon xx. Given a particular element a:Aa:A, the element b(a)b(a) is an element dependent upon a:Aa:A.

Basic type formers - identification types and dependent function types

In this section, we give the rules for the basic type formers of type theory, which are identification types and dependent function types.

Formation rules for identification types:

ΓAtypeΓ,a:A,b:Aa= Abtype\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, b:A \vdash a =_A b \; \mathrm{type}}

Formation rules for dependent function types:

ΓAtypeΓ,x:AB(x)typeΓ x:AB(x)type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \prod_{x:A} B(x) \; \mathrm{type}}

Introduction rules for identification types:

ΓAtypeΓ,a:Arefl A(a):a= Aa\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A \vdash \mathrm{refl}_A(a) : a =_A a}

Introduction rules for dependent function types:

ΓAtypeΓ,x:AB(x)typeΓ,x:Ab(x):B(x)Γλ(x:A).b(x): x:AB(x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash b(x):B(x)}{\Gamma \vdash \lambda(x:A).b(x):\prod_{x:A} B(x)}

Elimination rule for identification types:

Γ,x:A,y:A,p:x= AyC(x,y,p)typeΓ,t: a:AC(a,a,refl A(a)),x:A,y:A,p:x= AyJ A(t,x,y,p):C(x,y,p)\frac{\Gamma, x:A, y:A, p:x =_A y \vdash C(x, y, p) \; \mathrm{type}}{\Gamma, t:\prod_{a:A} C(a, a, \mathrm{refl}_A(a)), x:A, y:A, p:x =_A y \vdash J_A(t, x, y, p):C(x, y, p)}

Elimination rules for dependent function types:

ΓAtypeΓ,x:AB(x)typeΓ,f: x:AB(x),a:Aind x:AB(x)(f,a):B(a)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, f:\prod_{x:A} B(x), a:A \vdash \mathrm{ind}_{\prod_{x:A} B(x)}(f, a):B(a)}

Computation rules for identification types:

Γ,x:A,y:A,p:x= AyC(x,y,p)typeΓ,t: a:AC(a,a,refl A(a)),x:Aβ = A(t,x):ind = A(t,x,x,refl A(x))= C(x,x,refl A(x))t(x)\frac{\Gamma, x:A, y:A, p:x =_A y \vdash C(x, y, p) \; \mathrm{type}}{\Gamma, t:\prod_{a:A} C(a, a, \mathrm{refl}_A(a)), x:A \vdash \beta_{=_A}(t, x):\mathrm{ind}_{=_A}(t, x, x, \mathrm{refl}_A(x)) =_{C(x, x, \mathrm{refl}_A(x))} t(x)}

Computation rules for dependent function types

ΓAtypeΓ,x:AB(x)typeΓ,x:Ab(x):B(x)Γ,a:Aβ x:AB(x)(a):ind x:AB(x)(λ(x:A).b(x),a)= B(a)b(a)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash b(x):B(x)}{\Gamma, a:A \vdash \beta_{\prod_{x:A} B(x)}(a):\mathrm{ind}_{\prod_{x:A} B(x)}(\lambda(x:A).b(x), a) =_{B(a)} b(a)}

Optional Uniqueness rules for identification types

Γ,x:A,y:A,p:x= AyC(x,y,p)typeΓ,t: a:AC(a,a,refl A(a)),x:A,y:A,p:x= Ay,q:C(x,y,p)η = A(t,x,y,p,q):J A(t,x,y,p)= C(x,y,p)q\frac{\Gamma, x:A, y:A, p:x =_A y \vdash C(x, y, p) \; \mathrm{type}}{\Gamma, t:\prod_{a:A} C(a, a, \mathrm{refl}_A(a)), x:A, y:A, p:x =_A y, q:C(x, y, p) \vdash \eta_{=_A}(t, x, y, p, q):J_A(t, x, y, p) =_{C(x, y, p)} q}

Uniqueness rules for dependent function types:

ΓAtypeΓ,x:AB(x)typeΓ,f: x:AB(x)η x:AB(x)(f):f= x:AB(x)λ(x).f(x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, f:\prod_{x:A} B(x) \vdash \eta_{\prod_{x:A} B(x)}(f):f =_{\prod_{x:A} B(x)} \lambda(x).f(x)}

Function types

Formation rules for function types:

ΓAtypeΓBtypeΓABtype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \to B \; \mathrm{type}}

Introduction rules for function types:

ΓAtypeΓBtypeΓ,x:Ab(x):BΓλ(x:A).b(x):AB\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, x:A \vdash b(x):B}{\Gamma \vdash \lambda(x:A).b(x):A \to B}

Elimination rules for function types:

ΓAtypeΓBtypeΓ,f:AB,a:Aind AB(f,a):B\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:A \to B, a:A \vdash \mathrm{ind}_{A \to B}(f, a):B}

Computation rules for function types

ΓAtypeΓBtypeΓ,x:Ab(x):BΓ,a:Aβ AB(a):ind AB(λ(x:A).b(x),a)= Bb(a)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, x:A \vdash b(x):B}{\Gamma, a:A \vdash \beta_{A \to B}(a):\mathrm{ind}_{A \to B}(\lambda(x:A).b(x), a) =_{B} b(a)}

Uniqueness rules for function types:

ΓAtypeΓBtypeΓ,f:ABη AB(f):f= ABλ(x).f(x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:A \to B \vdash \eta_{A \to B}(f):f =_{A \to B} \lambda(x).f(x)}

Heterogeneous identification types

Now that we have identification types and dependent product types, we can define heterogeneous identification types, which are important for defining the isEquiv dependent type on a function, used to determine whether a function is an equivalence, and then used to define definitions.

Formation rule for heterogeneous identification types:

ΓAtypeΓBtype Γa:AΓb:AΓp:a= AbΓy:BΓz:BΓy= B pztype\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \quad \Gamma \vdash y:B \quad \Gamma \vdash z:B \end{array} }{\Gamma \vdash y =_{B}^{p} z \; \mathrm{type}}

Introduction rule for heterogeneous identification types:

ΓAtypeΓBtype Γf:ABΓa:AΓb:AΓp:a= AbΓap B(f,a,b,p):ind AB(f,a)= B pind AB(f,b)\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \\ \Gamma \vdash f:A \to B \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \end{array} }{\Gamma \vdash \mathrm{ap}_{B}(f, a, b, p):\mathrm{ind}_{A \to B}(f, a) =_{B}^{p} \mathrm{ind}_{A \to B}(f, b)}

Elimination rule for heterogeneous identification types:

ΓAtypeΓBtype Γ,a:A,b:A,p:a= Ab,y:B(a),z:B(b),q:y= B pzC(a,b,p,y,z,q)type Γt: f:AB a:A b:A p:a= AbC(a,b,p,ind AB(f,a),ind AB(f,b),ap B(f,a,b,p)) Γa:AΓb:AΓp:a= AbΓy:BΓz:BΓq:y= B pzΓJ B(t,a,y,b,z,p,q):C(a,y,b,z,p,q)\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \\ \Gamma, a:A, b:A, p:a =_A b, y:B(a), z:B(b), q:y =_{B}^p z \vdash C(a, b, p, y, z, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{f:A \to B} \prod_{a:A} \prod_{b:A} \prod_{p:a =_A b} C(a, b, p, \mathrm{ind}_{A \to B}(f, a), \mathrm{ind}_{A \to B}(f, b), \mathrm{ap}_{B}(f, a, b, p)) \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \quad \Gamma \vdash y:B \quad \Gamma \vdash z:B \quad \Gamma \vdash q:y =_{B}^p z \end{array} }{\Gamma \vdash J_{B}(t, a, y, b, z, p, q):C(a, y, b, z, p, q)}

Computation rules for heterogeneous identification types:

ΓAtypeΓ,x:AB(x)type Γ,a:A,b:A,p:a= Ab,y:B,z:B,q:y= B pzC(a,b,p,y,z,q)type Γt: f:AB a:A b:A p:a= AbC(a,b,p,ind AB(f,a),ind AB(f,b),ap B(f,a,b,p)) Γf:ABΓa:AΓb:AΓp:a= AbΓβ = B p(t,f,a,b,p):J B(t,a,ind AB(f,a),b,ind AB(f,b),p,ap B(f,a,b,p))= C(a,ind AB(f,a),b,ind AB(f,b),p,ap B(f,a,b,p))t\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma, a:A, b:A, p:a =_A b, y:B, z:B, q:y =_{B}^p z \vdash C(a, b, p, y, z, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{f:A \to B} \prod_{a:A} \prod_{b:A} \prod_{p:a =_A b} C(a, b, p, \mathrm{ind}_{A \to B}(f, a), \mathrm{ind}_{A \to B}(f, b), \mathrm{ap}_{B}(f, a, b, p)) \\ \Gamma \vdash f:A \to B \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \end{array} }{\Gamma \vdash \beta_{=_{B}^p}(t, f, a, b, p):J_{B}(t, a, \mathrm{ind}_{A \to B}(f, a), b, \mathrm{ind}_{A \to B}(f, b), p, \mathrm{ap}_{B}(f, a, b, p)) =_{C(a, \mathrm{ind}_{A \to B}(f, a), b, \mathrm{ind}_{A \to B}(f, b), p, \mathrm{ap}_{B}(f, a, b, p))} t}

Function extensionality

Function extensionality states that given functions f:ABf:A \to B and g:ABg:A \to B the dependent function type

x:Aind AB(f,x)= Bind AB(g,x)\prod_{x:A} \mathrm{ind}_{A \to B}(f, x) =_B \mathrm{ind}_{A \to B}(g, x)

behaves as an identity system.

Γ,f:AB,g:AB,h: x:Aind AB(f,x)= Bind AB(g,x)C(f,g,h)Γ,t: k:ABC(k,k,ap B(k)),f:AB,g:AB,h: x:Aind AB(f,x)= Bind AB(g,x)J(t,f,g,h):C(f,g,h)\frac{\Gamma, f:A \to B, g:A \to B, h:\prod_{x:A} \mathrm{ind}_{A \to B}(f, x) =_B \mathrm{ind}_{A \to B}(g, x) \vdash C(f, g, h)}{\Gamma, t:\prod_{k:A \to B} C(k, k, \mathrm{ap}_B(k)), f:A \to B, g:A \to B, h:\prod_{x:A} \mathrm{ind}_{A \to B}(f, x) =_B \mathrm{ind}_{A \to B}(g, x) \vdash J(t, f, g, h):C(f, g, h)}
Γ,f:AB,g:AB,h: x:Aind AB(f,x)= Bind AB(g,x)C(f,g,h)Γ,t: k:ABC(k,k,ap B(k)),f:ABβ(t,f):J(t,f,f,ap B(f))= C(f,f,ap B(f))ind k:ABC(k,k,ap B(k))(t,f)\frac{\Gamma, f:A \to B, g:A \to B, h:\prod_{x:A} \mathrm{ind}_{A \to B}(f, x) =_B \mathrm{ind}_{A \to B}(g, x) \vdash C(f, g, h)}{\Gamma, t:\prod_{k:A \to B} C(k, k, \mathrm{ap}_B(k)), f:A \to B \vdash \beta(t, f):J(t, f, f, \mathrm{ap}_B(f)) =_{C(f, f, \mathrm{ap}_B(f))} \mathrm{ind}_{\prod_{k:A \to B} C(k, k, \mathrm{ap}_B(k))}(t, f)}

isEquiv types

The rules for isEquiv types are as follows:

Formation rules for isEquiv:

ΓAtypeΓBtypeΓ,f:ABΓisEquiv(f)type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B}{\Gamma \vdash \mathrm{isEquiv}(f) \; \mathrm{type}}

Introduction rules for isEquiv:

ΓAtypeΓBtypeΓ,f:ABΓa:AΓb: y:Bf(a)= By Γτ A: x:A y:B(f(x)= By)(a= Ax)Γτ B: x:A y:B z:f(x)= Byb(y)= B τ A(x,y,z)zΓwitn(a,b,τ A,τ B):isEquiv(f)\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B \quad \Gamma \vdash a:A \quad \Gamma \vdash b:\prod_{y:B} f(a) =_B y \\ \Gamma \vdash \tau_A:\prod_{x:A} \prod_{y:B} (f(x) =_B y) \to (a =_A x) \quad \Gamma \vdash \tau_B:\prod_{x:A} \prod_{y:B} \prod_{z:f(x) =_B y} b(y) =_B^{\tau_A(x, y, z)} z \end{array} }{\Gamma \vdash \mathrm{witn}(a, b, \tau_A, \tau_B):\mathrm{isEquiv}(f)}

Elimination rules for isEquiv:

ΓAtypeΓBtypeΓ,f:ABΓp:isEquiv(f) Γ,y:BC(y)typeΓc f: x:AC(f(x))Γb:BΓind isEquiv(f) C(f,p,c f,b):C(b)\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B \quad \Gamma \vdash p:\mathrm{isEquiv}(f) \\ \Gamma, y:B \vdash C(y) \; \mathrm{type} \quad \Gamma \vdash c_f:\prod_{x:A} C(f(x)) \quad \Gamma \vdash b:B \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{isEquiv}(f)}^C(f, p, c_f, b):C(b)}

Computation rules for isEquiv:

ΓAtypeΓBtypeΓ,f:ABΓp:isEquiv(f) Γ,y:BC(y)typeΓc f: x:AC(f(x))Γa:AΓβ isEquiv(f)(f,p,c f,a):ind isEquiv(f) C(f,p,c f,f(a))= C(f(a))c f(a)\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B \quad \Gamma \vdash p:\mathrm{isEquiv}(f) \\ \Gamma, y:B \vdash C(y) \; \mathrm{type} \quad \Gamma \vdash c_f:\prod_{x:A} C(f(x)) \quad \Gamma \vdash a:A \end{array} }{\Gamma \vdash \beta_{\mathrm{isEquiv}(f)}(f, p, c_f, a):\mathrm{ind}_{\mathrm{isEquiv}(f)}^C(f, p, c_f, f(a)) =_{C(f(a))} c_f(a)}

Uniqueness rules for isEquiv:

ΓAtypeΓBtypeΓ,f:ABΓp:isEquiv(f) Γ,y:BC(y)typeΓc: y:BC(y)Γb:BΓη isEquiv(f)(f,p,c,b):c(b)= C(b)ind isEquiv(f) C(f,p,c,b)\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B \quad \Gamma \vdash p:\mathrm{isEquiv}(f) \\ \Gamma, y:B \vdash C(y) \; \mathrm{type} \quad \Gamma \vdash c:\prod_{y:B} C(y) \quad \Gamma \vdash b:B \end{array} }{\Gamma \vdash \eta_{\mathrm{isEquiv}(f)}(f, p, c, b):c(b) =_{C(b)} \mathrm{ind}_{\mathrm{isEquiv}(f)}^C(f, p, c, b)}

Structural rules for definitions

Now that we have finally defined identification types, we can define the structural rules for term definitions. The structural rules for term definitions say that given a term a:Aa:A and a term definition ba:Ab \coloneqq a:A, one could derive that bb is a term of AA, and that there is an identification between bb and aa:

Γa:AΓba:AΓb:AΓa:AΓba:AΓδ A(a,b):a= Ab\frac{\Gamma \vdash a:A \quad \Gamma \vdash b \coloneqq a:A}{\Gamma \vdash b:A} \qquad \frac{\Gamma \vdash a:A \quad \Gamma \vdash b \coloneqq a:A}{\Gamma \vdash \delta_A(a, b):a =_A b}

Similarly, now that we have finally defined function types and isEquiv types, we can define the structural rules for type definitions. The structural rules for type definitions say that given a type AA and a type definition BAtypeB \coloneqq A \; \mathrm{type}, one could derive that BB is a type, that there is a function between AA and BB, and that function is an equivalence:

ΓAtypeΓBAtypeΓBtypeΓAtypeΓBAtypeΓδ A,B:ABΓAtypeΓBAtypeΓϵ A,B:isEquiv(δ A,B)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \coloneqq A \; \mathrm{type}}{\Gamma \vdash B \; \mathrm{type}} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \coloneqq A \; \mathrm{type}}{\Gamma \vdash \delta_{A, B}:A \to B} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \coloneqq A \; \mathrm{type}}{\Gamma \vdash \epsilon_{A, B}:\mathrm{isEquiv}(\delta_{A, B})}

Dependent heterogeneous identification types

Now that we have identification types and dependent product types, we can define dependent heterogeneous identification types, which are important for defining the rules for higher inductive types.

Formation rule for dependent heterogeneous identification types:

ΓAtypeΓ,x:AB(x)type Γa:AΓb:AΓp:a= AbΓy:B(a)Γz:B(b)Γy= x:A.B(x) pztype\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \quad \Gamma \vdash y:B(a) \quad \Gamma \vdash z:B(b) \end{array} }{\Gamma \vdash y =_{x:A.B(x)}^{p} z \; \mathrm{type}}

Introduction rule for dependent heterogeneous identification types:

ΓAtypeΓ,x:AB(x)type Γf: x:AB(x)Γa:AΓb:AΓp:a= AbΓapd x:A.B(x)(f,a,b,p):f(a)= x:A.B(x) pf(b)\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma \vdash f:\prod_{x:A} B(x) \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \end{array} }{\Gamma \vdash \mathrm{apd}_{x:A.B(x)}(f, a, b, p):f(a) =_{x:A.B(x)}^{p} f(b)}

Elimination rule for dependent heterogeneous identification types:

ΓAtypeΓ,x:AB(x)type Γ,a:A,b:A,p:a= Ab,y:B(a),z:B(b),q:y= x:A.B(x) pzC(a,b,p,y,z,q)type Γt: f: x:AB(x) a:A b:A p:a= AbC(a,b,p,f(a),f(b),apd x:A.B(x)(f,a,b,p)) Γa:AΓb:AΓp:a= AbΓy:B(a)Γz:B(b)Γq:y= x:A.B(x) pzΓJ x:A.B(x) p(t,a,y,b,z,p,q):C(a,y,b,z,p,q)\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma, a:A, b:A, p:a =_A b, y:B(a), z:B(b), q:y =_{x:A.B(x)}^p z \vdash C(a, b, p, y, z, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{f:\prod_{x:A} B(x)} \prod_{a:A} \prod_{b:A} \prod_{p:a =_A b} C(a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p)) \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \quad \Gamma \vdash y:B(a) \quad \Gamma \vdash z:B(b) \quad \Gamma \vdash q:y =_{x:A.B(x)}^p z \end{array} }{\Gamma \vdash J_{x:A.B(x)}^p(t, a, y, b, z, p, q):C(a, y, b, z, p, q)}

Computation rules for dependent heterogeneous identification types:

ΓAtypeΓ,x:AB(x)type Γ,a:A,b:A,p:a= Ab,y:B(a),z:B(b),q:y= x:A.B(x) pzC(a,b,p,y,z,q)type Γt: f: x:AB(x) a:A b:A p:a= AbC(a,b,p,f(a),f(b),apd x:A.B(x)(f,a,b,p)) Γf: x:AB(x)Γa:AΓb:AΓp:a= AbΓβ = x:A.B(x) p(t,f,a,b,p):J x:A.B(x)(t,a,f(a),b,f(b),p,apd x:A.B(x)(f,a,b,p))= C(a,f(a),b,f(b),p,apd x:A.B(x)(f,a,b,p))t\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma, a:A, b:A, p:a =_A b, y:B(a), z:B(b), q:y =_{x:A.B(x)}^p z \vdash C(a, b, p, y, z, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{f:\prod_{x:A} B(x)} \prod_{a:A} \prod_{b:A} \prod_{p:a =_A b} C(a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p)) \\ \Gamma \vdash f:\prod_{x:A} B(x) \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \end{array} }{\Gamma \vdash \beta_{=_{x:A.B(x)}^p}(t, f, a, b, p):J_{x:A.B(x)}(t, a, f(a), b, f(b), p, \mathrm{apd}_{x:A.B(x)}(f, a, b, p)) =_{C(a, f(a), b, f(b), p, \mathrm{apd}_{x:A.B(x)}(f, a, b, p))} t}

Pair types

Formation rules for pair types:

ΓAtypeΓBtypeΓA×Btype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \times B \; \mathrm{type}}

Introduction rules for pair types:

ΓAtypeΓBtypeΓ,x:A,y:Bin(x,y):A×B\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, x:A, y:B \vdash \mathrm{in}(x, y):A \times B}

Elimination rules for pair types:

ΓAtypeΓBtypeΓ,z:A×Bind A×B A(z):AΓAtypeΓBtypeΓ,z:A×Bind A×B B(z):B\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, z:A \times B \vdash \mathrm{ind}_{A \times B}^A(z):A} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, z:A \times B \vdash \mathrm{ind}_{A \times B}^B(z):B}

Computation rules for pair types:

ΓAtypeΓBtypeΓ,x:A,y:Bβ A×B A(x,y):ind A×B A(in(x,y))= Ax\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, x:A, y:B \vdash \beta_{A \times B}^A(x, y):\mathrm{ind}_{A \times B}^A(\mathrm{in}(x, y)) =_A x}
ΓAtypeΓBtypeΓ,x:A,y:Bβ A×B B(x,y):ind A×B B(in(x,y))= By\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, x:A, y:B \vdash \beta_{A \times B}^B(x, y):\mathrm{ind}_{A \times B}^B(\mathrm{in}(x, y)) =_B y}

Uniqueness rules for pair types:

ΓAtypeΓBtypeΓ,z:A×Bη A×B(z):z= A×Bin(ind A×B A(z),ind A×B B(z))\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, z:A \times B \vdash \eta_{A \times B}(z):z =_{A \times B} \mathrm{in}(\mathrm{ind}_{A \times B}^A(z), \mathrm{ind}_{A \times B}^B(z))}

Dependent pair types

Formation rules for dependent pair types:

ΓAtypeΓ,x:AB(x)typeΓ x:AB(x)type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \sum_{x:A} B(x) \; \mathrm{type}}

Introduction rules for dependent pair types:

ΓAtypeΓ,x:AB(x)typeΓ,x:A,y:B(x)in(x,y): x:AB(x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, x:A, y:B(x) \vdash \mathrm{in}(x, y):\sum_{x:A} B(x)}

Elimination rules for dependent pair types:

ΓAtypeΓ,x:AB(x)typeΓind x:AB(x) A:( x:AB(x))AΓAtypeΓ,x:AB(x)typeΓind x:AB(x) B: z: x:AB(x)B(ind x:AB(x) A(z))\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{ind}_{\sum_{x:A} B(x)}^A:\left(\sum_{x:A} B(x)\right) \to A} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{ind}_{\sum_{x:A} B(x)}^B:\prod_{z:\sum_{x:A} B(x)} B(\mathrm{ind}_{\sum_{x:A} B(x)}^A(z))}

Computation rules for dependent pair types:

ΓAtypeΓ,x:AB(x)typeΓ,x:A,y:B(x)β x:AB(x) A(x,y):ind x:AB(x) A(in(x,y))= Ax\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, x:A, y:B(x) \vdash \beta_{\sum_{x:A} B(x)}^A(x, y):\mathrm{ind}_{\sum_{x:A} B(x)}^A(\mathrm{in}(x, y)) =_A x}
ΓAtypeΓ,x:AB(x)typeΓ,x:A,y:B(x)β Σ(x:A).B(x) B(x,y):ind x:AB(x) B(in(x,y))= B(ind x:AB(x) A(in(x,y)))y\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, x:A, y:B(x) \vdash \beta_{\Sigma(x:A).B(x)}^B(x, y):\mathrm{ind}_{\sum_{x:A} B(x)}^B(\mathrm{in}(x, y)) =_{B(\mathrm{ind}_{\sum_{x:A} B(x)}^A(\mathrm{in}(x, y)))} y}

Uniqueness rules for dependent pair types:

ΓAtypeΓ,x:AB(x)typeΓ,z: x:AB(x)η x:AB(x)(z):z= x:AB(x)in(ind x:AB(x)) A(z),ind x:AB(x) B(z))\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, z:\sum_{x:A} B(x) \vdash \eta_{\sum_{x:A} B(x)}(z):z =_{\sum_{x:A} B(x)} \mathrm{in}(\mathrm{ind}_{\sum_{x:A} B(x))}^A(z), \mathrm{ind}_{\sum_{x:A} B(x)}^B(z))}

Positive types

Now that we have identification types, dependent heterogeneous identification types, equivalence types, dependent sum types, and dependent product types, we can use that to define the equivalence type, the isContr modality, the uniqueness quantifier

AB f:ABisEquiv(f)A \simeq B \coloneqq \sum_{f:A \to B} \mathrm{isEquiv}(f)
isContr(A) y:A z:Ay= Az\mathrm{isContr}(A) \coloneqq \sum_{y:A} \prod_{z:A} y =_{A} z
!x:A.B(x)isContr( x:AB(x))\exists!x:A.B(x) \coloneqq \mathrm{isContr}\left(\sum_{x:A} B(x)\right)

and combine the elimination rule, the computation rule, and the uniqueness rule for any positive type into one rule, the universal property rule. In addition, every type has an extensionality rule.

Unit type

Formation rules for the unit type:

ΓctxΓ𝟙type\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{1} \; \mathrm{type}}

Introduction rules for the unit type:

ΓctxΓpt:𝟙\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{pt}:\mathbb{1}}

Universal property rule for the unit type:

Γ,x:𝟙C(x)typeΓc pt:C(pt)Γup 𝟙 C(c pt):!c: x:𝟙C(x).(c(pt)= C(pt)c pt)\frac{\Gamma, x:\mathbb{1} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_\mathrm{pt}:C(\mathrm{pt})}{\Gamma \vdash \mathrm{up}_\mathbb{1}^C(c_\mathrm{pt}):\exists!c:\prod_{x:\mathbb{1}} C(x).(c(\mathrm{pt}) =_{C(\mathrm{pt})} c_\mathrm{pt})}

Extensionality rule for the unit type:

ΓctxΓext 𝟙 pt,pt:(pt= 𝟙pt)𝟙\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{ext}_{\mathbb{1}}^{\mathrm{pt}, \mathrm{pt}}:(\mathrm{pt} =_{\mathbb{1}} \mathrm{pt}) \simeq \mathbb{1}}

Empty type

Formation rules for the empty type:

ΓctxΓ𝟘type\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{0} \; \mathrm{type}}

Universal property rule for the empty type:

Γ,x:𝟘C(x)typeΓup 𝟘 C:!c: x:𝟘C(x).𝟙\frac{\Gamma, x:\mathbb{0} \vdash C(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{up}_\mathbb{0}^C:\exists!c:\prod_{x:\mathbb{0}} C(x).\mathbb{1}}

Interval type

Formation rules for the interval type:

ΓctxΓ𝕀type\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{I} \; \mathrm{type}}

Introduction rules for the interval type:

ΓctxΓ0:𝕀ΓctxΓ1:𝕀ΓctxΓp:0= 𝕀1\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{I}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 1:\mathbb{I}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash p:0 =_{\mathbb{I}} 1}

Universal property rule for the interval type:

Γ,x:𝟚C(x)typeΓc 0:C(0)Γc 1:C(1)Γc p:c 0= C pc 1Γup 𝕀 C(c 0,c 1,c p):!c: x:𝕀C(x).(c(0)= C(0)c 0)×(c(1)= C(1)c 1)×(apd x:𝕀.C(x)(c,c 0,c 1,c p)= c 0= C pc 1c p)\frac{\Gamma, x:\mathbb{2} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_1:C(1) \quad \Gamma \vdash c_p:c_0 =_C^p c_1}{\Gamma \vdash \mathrm{up}_\mathbb{I}^C(c_0, c_1, c_p):\exists!c:\prod_{x:\mathbb{I}} C(x).(c(0) =_{C(0)} c_0) \times (c(1) =_{C(1)} c_1) \times (\mathrm{apd}_{x:\mathbb{I}.C(x)}(c, c_0, c_1, c_p) =_{c_0 =_C^p c_1} c_p)}

Extensionality rules for the interval type:

ΓctxΓext 𝕀 0,0:(0= 𝕀0)𝟙ΓctxΓext 𝕀 0,1:(0= 𝕀1)𝟙\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{ext}_{\mathbb{I}}^{0, 0}:(0 =_{\mathbb{I}} 0) \simeq \mathbb{1}} \quad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{ext}_{\mathbb{I}}^{0, 1}:(0 =_{\mathbb{I}} 1) \simeq \mathbb{1}}
ΓctxΓext 𝕀 1,0:(1= 𝕀0)𝟙ΓctxΓext 𝕀 1,1:(1= 𝕀1)𝟙\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{ext}_{\mathbb{I}}^{1, 0}:(1 =_{\mathbb{I}} 0) \simeq \mathbb{1}} \quad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{ext}_{\mathbb{I}}^{1, 1}:(1 =_{\mathbb{I}} 1) \simeq \mathbb{1}}

Copy types

Formation rules for copy types:

ΓAtypeΓCopy(A)type\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{Copy}(A) \; \mathrm{type}}

Introduction rules for copy types:

ΓAtypeΓcopy A:ACopy(A)\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{copy}_A:A \to \mathrm{Copy}(A)}

Universal property rule for copy types:

ΓAtypeΓ,x:Copy(A)C(x)typeΓc copy A: x:AC(copy A(x))Γup Copy(A) C(c copy A):!c: x:Copy(A)C(x). a:Ac(copy A(a))= C(copy A(a))c copy A(a)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:\mathrm{Copy}(A) \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_{\mathrm{copy}_A}:\prod_{x:A} C(\mathrm{copy}_A(x))}{\Gamma \vdash \mathrm{up}_{\mathrm{Copy}(A)}^C(c_{\mathrm{copy}_A}):\exists!c:\prod_{x:\mathrm{Copy}(A)} C(x).\prod_{a:A} c(\mathrm{copy}_A(a)) =_{C(\mathrm{copy}_A(a))} c_{\mathrm{copy}_A}(a)}

Extensionality rules for the copy type:

ΓAtypeΓext Copy(A) copy A: a:A b:A(copy A(a)= Copy(A)copy A(b))(a= Ab)\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{ext}_{\mathrm{Copy}(A)}^{\mathrm{copy}_A}:\prod_{a:A} \prod_{b:A} (\mathrm{copy}_A(a) =_{\mathrm{Copy}(A)} \mathrm{copy}_A(b)) \simeq (a =_A b)}

Booleans type

Formation rules for the booleans type:

ΓctxΓ𝟚type\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{2} \; \mathrm{type}}

Introduction rules for the booleans type:

ΓctxΓ0:𝟚ΓctxΓ1:𝟚\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{2}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 1:\mathbb{2}}

Universal property rule for the booleans type:

Γ,x:𝟚C(x)typeΓc 0:C(0)Γc 1:C(1)Γup 𝟚 C(c 0,c 1):!c: x:𝟚C(x).(c(0)= C(0)c 0)×(c(1)= C(1)c 1)\frac{\Gamma, x:\mathbb{2} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_1:C(1)}{\Gamma \vdash \mathrm{up}_\mathbb{2}^C(c_0, c_1):\exists!c:\prod_{x:\mathbb{2}} C(x).(c(0) =_{C(0)} c_0) \times (c(1) =_{C(1)} c_1)}

Extensionality rules for the booleans type:

ΓctxΓext 𝟚 0,0:(0= 𝟚0)𝟙ΓctxΓext 𝟚 0,1:(0= 𝟚1)𝟘\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{ext}_{\mathbb{2}}^{0, 0}:(0 =_{\mathbb{2}} 0) \simeq \mathbb{1}} \quad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{ext}_{\mathbb{2}}^{0, 1}:(0 =_{\mathbb{2}} 1) \simeq \mathbb{0}}
ΓctxΓext 𝟚 1,0:(1= 𝟚0)𝟘ΓctxΓext 𝟚 1,1:(1= 𝟚1)𝟙\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{ext}_{\mathbb{2}}^{1, 0}:(1 =_{\mathbb{2}} 0) \simeq \mathbb{0}} \quad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{ext}_{\mathbb{2}}^{1, 1}:(1 =_{\mathbb{2}} 1) \simeq \mathbb{1}}

Circle type

Formation rules for the circle type:

ΓctxΓS 1type\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash S^1 \; \mathrm{type}}

Introduction rules for the circle type:

ΓctxΓbase:S 1ΓctxΓloop:base= S 1base\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{base}:S^1} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{loop}:\mathrm{base} =_{S^1} \mathrm{base}}

Universal property rule for the circle type:

Γ,x:𝟚C(x)typeΓc base:C(base)Γc loop:c base= C loopc baseΓup 𝕀 C(c base,c loop):!c: x:S 1C(x).(c(base)= C(base)c base)×(apd C(c,c base,c base,c loop)= c base= x:S 1.C(x) loopc basec loop)\frac{\Gamma, x:\mathbb{2} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_\mathrm{base}:C(\mathrm{base}) \quad \Gamma \vdash c_\mathrm{loop}:c_\mathrm{base} =_C^\mathrm{loop} c_\mathrm{base}}{\Gamma \vdash \mathrm{up}_\mathbb{I}^C(c_\mathrm{base}, c_\mathrm{loop}):\exists!c:\prod_{x:S^1} C(x).(c(\mathrm{base}) =_{C(\mathrm{base})} c_\mathrm{base}) \times (\mathrm{apd}_C(c, c_\mathrm{base}, c_\mathrm{base}, c_\mathrm{loop}) =_{c_\mathrm{base} =_{x:S^1.C(x)}^\mathrm{loop} c_\mathrm{base}} c_\mathrm{loop})}

Extensionality rules for the circle type:

ΓctxΓext S 1 base:(base= S 1base)+𝟙+\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{ext}_{S^1}^{\mathrm{base}}:(\mathrm{base} =_{S^1} \mathrm{base}) \simeq \mathbb{N} + \mathbb{1} + \mathbb{N}}

Sum types

Formation rules for sum types:

ΓAtypeΓBtypeΓA+Btype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A + B \; \mathrm{type}}

Introduction rules for sum types:

ΓAtypeΓBtypeΓin A:AA+BΓAtypeΓBtypeΓin B:BA+B\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash \mathrm{in}_A:A \to A + B} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash \mathrm{in}_B:B \to A + B}

Universal property rule for sum types:

ΓAtypeΓBtypeΓ,x:A+BC(x)typeΓc in A: x:AC(in A(x))Γc in B: y:BC(in B(y))Γup A+B C(c in A,c in B):!c: x:A+BC(x).( a:A(c(in A(a))= C(in A(a))c in A(a)))×( b:B(c(in B(b))= C(in B(b))c in B(b)))\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, x:A + B \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_{\mathrm{in}_A}:\prod_{x:A} C(\mathrm{in}_A(x)) \quad \Gamma \vdash c_{\mathrm{in}_B}:\prod_{y:B} C(\mathrm{in}_B(y))}{\Gamma \vdash \mathrm{up}_{A + B}^C(c_{\mathrm{in}_A}, c_{\mathrm{in}_B}):\exists!c:\prod_{x:A + B} C(x).\left(\prod_{a:A} (c(\mathrm{in}_A(a)) =_{C(\mathrm{in}_A(a))} c_{\mathrm{in}_A}(a))\right) \times \left(\prod_{b:B} (c(\mathrm{in}_B(b)) =_{C(\mathrm{in}_B(b))} c_{\mathrm{in}_B}(b))\right)}

Extensionality rules for the sum type:

ΓAtypeΓBtypeΓext A+B in A,in A: a:A b:A(in A(a)= A+Bin A(b))(a= Ab)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash \mathrm{ext}_{A + B}^{\mathrm{in}_A, \mathrm{in}_A}:\prod_{a:A} \prod_{b:A} (\mathrm{in}_A(a) =_{A + B} \mathrm{in}_A(b)) \simeq (a =_A b)}
ΓAtypeΓBtypeΓext A+B in A,in B: a:A b:B(in A(a)= A+Bin B(b))𝟘\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash \mathrm{ext}_{A + B}^{\mathrm{in}_A, \mathrm{in}_B}:\prod_{a:A} \prod_{b:B} (\mathrm{in}_A(a) =_{A + B} \mathrm{in}_B(b)) \simeq \mathbb{0}}
ΓAtypeΓBtypeΓext A+B in B,in A: a:B b:A(in B(a)= A+Bin A(b))𝟘\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash \mathrm{ext}_{A + B}^{\mathrm{in}_B, \mathrm{in}_A}:\prod_{a:B} \prod_{b:A} (\mathrm{in}_B(a) =_{A + B} \mathrm{in}_A(b)) \simeq \mathbb{0}}
ΓAtypeΓBtypeΓext A+B in B,in B: a:B b:B(in B(a)= A+Bin B(b))(a= Bb)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash \mathrm{ext}_{A + B}^{\mathrm{in}_B, \mathrm{in}_B}:\prod_{a:B} \prod_{b:B} (\mathrm{in}_B(a) =_{A + B} \mathrm{in}_B(b)) \simeq (a =_B b)}

Natural numbers type

Formation rules for the natural numbers type:

ΓctxΓtype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{N} \; \mathrm{type}}

Introduction rules for the natural numbers type:

ΓctxΓ0:ΓctxΓs:\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{N}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash s:\mathbb{N} \to \mathbb{N}}

Universal property rule for the natural numbers type:

Γ,x:C(x)typeΓc 0:C(0)Γc s: x:C(x)C(s(x))Γup C(c 0,c s):!c: x:C(x).(c(0)= C(0)c 0)× x:c(s(x))= C(s(x))c s(c(x))\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{N}} C(x) \to C(s(x))}{\Gamma \vdash \mathrm{up}_\mathbb{N}^C(c_0, c_s):\exists!c:\prod_{x:\mathbb{N}} C(x).(c(0) =_{C(0)} c_0) \times \prod_{x:\mathbb{N}} c(s(x)) =_{C(s(x))} c_s(c(x))}

Integers type

Formation rules for the integers type:

ΓctxΓtype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{Z} \; \mathrm{type}}

Introduction rules for the integers type:

ΓctxΓ0:ΓctxΓs:\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{Z}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash s:\mathbb{Z} \simeq \mathbb{Z}}

Universal property rule for the integers type:

Γ,x:C(x)typeΓc 0:C(0)Γc s: x:C(x)C(s(x))Γup C(c 0,c s):!c: x:C(x).(c(0)= C(0)c 0)× x:c(s(x))= C(s(x))c s(c(x))\frac{\Gamma, x:\mathbb{Z} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{Z}} C(x) \simeq C(s(x))}{\Gamma \vdash \mathrm{up}_\mathbb{Z}^C(c_0, c_s):\exists!c:\prod_{x:\mathbb{Z}} C(x).(c(0) =_{C(0)} c_0) \times \prod_{x:\mathbb{Z}} c(s(x)) =_{C(s(x))} c_s(c(x))}

Localizations

The localization of a type AA at a type BB is the (higher) inductive type L B(A)L_B(A) generated by a function AL B(A)A \to L_B(A) and an equivalence L B(A)(BL B(A))L_B(A) \simeq (B \to L_B(A)):

Formation rules for localizations:

ΓAtypeΓBtypeΓL B(A)type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash L_B(A) \; \mathrm{type}}

Introduction rules for localizations:

ΓAtypeΓBtypeΓtolocal:AL B(A)ΓAtypeΓconst L B(A),B:L B(A)(BL B(A))\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash \mathrm{tolocal}:A \to L_B(A)} \qquad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{const}_{L_B(A), B}:L_B(A) \simeq (B \to L_B(A))}

Disjunctions

The disjunction of a type AA and a type BB is the (higher) inductive type ABA \vee B generated by functions AABA \to A \vee B and BABB \to A \vee B and an equivalence AB(𝟚AB)A \vee B \simeq (\mathbb{2} \to A \vee B):

Formation rules for disjunctions:

ΓAtypeΓBtypeΓABtype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \vee B \; \mathrm{type}}

Introduction rules for disjunctions:

ΓAtypeΓBtypeΓin A:AABΓAtypeΓBtypeΓin B:BABΓAtypeΓBtypeΓconst 𝟚:AB(𝟚AB)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash \mathrm{in}_A:A \to A \vee B} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash \mathrm{in}_B:B \to A \vee B} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash \mathrm{const}_\mathbb{2}:A \vee B \simeq (\mathbb{2} \to A \vee B)}

Propositional truncations and set truncations

The propositional truncation [A][A] of a type AA is localization of AA at the booleans type 𝟚\mathbb{2}, [A]L 𝟚(A)[A] \coloneqq L_\mathbb{2}(A). The set truncation [A] 0[A]_0 of a type AA is localization of AA at the circle type S 1S^1, [A] 0L S 1(A)[A]_0 \coloneqq L_{S^1}(A).

 Categorical semantics

The fragment of objective type theory consisting of only identity types and dependent product types can be interpreted in any path category with weak homotopy Π\Pi-types.

Open problems

There are plenty of questions which are currently unresolved in objective type theory. Van der Berg and Besten in particular listed the following problems in their article:

Other problems include

See also open problems in homotopy type theory

See also

 References

Last revised on January 30, 2023 at 15:41:27. See the history of this page for a list of all contributions to it.