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 axioms

Removing axioms

Contents

Idea

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

This means that in additon to being a weak type theory, where the computation and uniqueness rules (beta-reduction and eta-conversion) for each type in the type theory are all propositional computational and uniqueness rules using the identity type, 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.

Formalizations and syntax

Substitutions

There are two ways one could define substitutions in dependent type theory, either by explicit substitution or by showing that the substitution rule is an admissible rule. However, for objective type theory, only the latter approach is possible.

The problem with explicit substitutions is that with explicit substitution approaches, the contexts are usually formalized with judgmental equality of morphisms of contexts, such that the categorical semantics correspond to a functor from the category of contexts CC to the 2-category Cat\mathrm{Cat} which takes a context Γ:C\Gamma:C to the slice category C/ΓC/\Gamma. However, without judgmental equality, CC doesn’t form a category anymore, since the morphisms in CC don’t form a set anymore, and one can no longer express the unit and associatvity laws for composition of morphisms of contexts, which are needed for the unit and associativity laws of explicit substitution. The same holds for explicit substitution via telescopes; here, substitutions are elements of telescopes, and one has judgmental equalities of the substitutions themselves.

Alternatively, one can try to define structure indicating that the collection of contexts CC forms an ( , 1 ) (\infty, 1) -category, avoiding the need for judgmental equality entirely, but one quickly runs into coherence issues, since the structure of an (,1)(\infty, 1)-category cannot be expressed from nothing using a finite amount of structure. This is similar to the issues in defining an (,1)(\infty, 1)-category in dependent type theory without using pre-existing simplicial or cubical structure or modalities. Thus, it is currently unknown how to avoid this use of judgmental equality for explicit substitution and/or telescopes in dependent type theory, rendering it impossible for those to formulate objective type theory.

The other approach involving an admissible substitution rule doesn’t suffer from this issue because the analogue in admissible substitution approaches of the judgmental equality in explicit substitution approaches resides in the metatheory rather than the actual theory itself, so the type theory itself can genuinely be said to not contain any judgmental equalities.

Definitions in objective type theory

In section 9 of Winterhalter2020, Theo Winterhalter indicates that there are many ways to formalize dependent type theory. One important aspect is whether to use Russell universes or a separate type judgment to denote types: van der Berg & den Besten 2021 and UPF 2013 both use Russell universes in their formal presentation of dependent type theory, while Rijke 2022 uses a separate type judgment to denote types.

In the context of objective type theory, there is no judgmental equality in the type theory in the traditional sense, so there is the question of how to define aliases of terms and types in the type theory. For the case of terms, that is easily resolved by using identity types. For example, to define 22 as the successor of the succcessor of zero in the natural numbers type, one could postulate an identification def2:2= Ns(s(0))\mathrm{def}2:2 =_{\mathrm{N}} s(s(0)). On the other hand, the situation for types is a bit more complicated. For example, the isContr modality isContr(A)\mathrm{isContr}(A) in dependent type theory indicating whether the type AA is a contractible type is usually defined to be x:A y:AId A(x,y)\sum_{x:A} \prod_{y:A} \mathrm{Id}_A(x, y). But without judgmental equality, one cannot simply write

isContr(A) x:A y:AId A(x,y)\mathrm{isContr}(A) \equiv \sum_{x:A} \prod_{y:A} \mathrm{Id}_A(x, y)

When presenting dependent type theory using Russell universes, the answer is as simple as that for terms: one simply uses typal equality instead, because every type is an element of a Russell universe, and so one could write

defisContr A:isContr(A)= Type i x:A y:AId A(x,y)\mathrm{defisContr}_A:\mathrm{isContr}(A) =_{\mathrm{Type}_i} \sum_{x:A} \prod_{y:A} \mathrm{Id}_A(x, y)

for types isContr(A):Type i\mathrm{isContr}(A):\mathrm{Type}_i and x:A y:AId A(x,y):Type i\sum_{x:A} \prod_{y:A} \mathrm{Id}_A(x, y):\mathrm{Type}_i. On the other hand, when using a separate type judgment, types are not elements of other types, and thus one cannot compare them for typal equality. Instead, one has to use equivalences of types instead:

defisContr A:isContr(A) a:A b:AId A(a,b)\mathrm{defisContr}_A:\mathrm{isContr}(A) \simeq \sum_{a:A} \prod_{b:A} \mathrm{Id}_A(a, b)

This poses another problem: the equivalence type ABA \simeq B has not yet been defined yet.

When expanded out using dependent sum types and function types, one gets

f:ABisEquiv(f)\sum_{f:A \to B} \mathrm{isEquiv}(f)

UPF 2013 says that the type family f:ABisEquiv(f)f:A \to B \vdash \mathrm{isEquiv}(f) comes with

  • a family of functions

    f:ABqinvtoisEquiv(f): g:BA( y:BId B(f(g(y)),y))×( x:AId A(g(f(x)),x))isEquiv(f)f:A \to B \vdash \mathrm{qinvtoisEquiv}(f):\sum_{g:B \to A} \left(\prod_{y:B} \mathrm{Id}_B(f(g(y)), y)\right) \times \left(\prod_{x:A} \mathrm{Id}_A(g(f(x)), x)\right) \to \mathrm{isEquiv}(f)
  • a family of functions

    f:ABisEquivtoqinv(f):isEquiv(f) g:BA( y:BId B(f(g(y)),y))×( x:AId A(g(f(x)),x))f:A \to B \vdash \mathrm{isEquivtoqinv}(f):\mathrm{isEquiv}(f) \to \sum_{g:B \to A} \left(\prod_{y:B} \mathrm{Id}_B(f(g(y)), y)\right) \times \left(\prod_{x:A} \mathrm{Id}_A(g(f(x)), x)\right)
  • a family of identifications

    f:AB,p:isEquiv(f),q:isEquiv(f)proptruncisEquiv(f,p,q):Id isEquiv(f)(p,q)f:A \to B, p:\mathrm{isEquiv}(f), q:\mathrm{isEquiv}(f) \vdash \mathrm{proptruncisEquiv}(f, p, q):\mathrm{Id}_{\mathrm{isEquiv}(f)}(p, q)

This could be made into inference rules

ΓAtypeΓBtypeΓ,f:ABisEquiv(f)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:A \to B \vdash \mathrm{isEquiv}(f)}
ΓAtypeΓBtypeΓ,f:ABqinvtoisEquiv(f): g:BA( y:BId B(f(g(y)),y))×( x:AId A(g(f(x)),x))isEquiv(f)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:A \to B \vdash \mathrm{qinvtoisEquiv}(f):\sum_{g:B \to A} \left(\prod_{y:B} \mathrm{Id}_B(f(g(y)), y)\right) \times \left(\prod_{x:A} \mathrm{Id}_A(g(f(x)), x)\right) \to \mathrm{isEquiv}(f)}
ΓAtypeΓBtypeΓ,f:ABisEquivtoqinv(f):isEquiv(f) g:BA( y:BId B(f(g(y)),y))×( x:AId A(g(f(x)),x))\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:A \to B \vdash \mathrm{isEquivtoqinv}(f):\mathrm{isEquiv}(f) \to \sum_{g:B \to A} \left(\prod_{y:B} \mathrm{Id}_B(f(g(y)), y)\right) \times \left(\prod_{x:A} \mathrm{Id}_A(g(f(x)), x)\right)}
ΓAtypeΓBtypeΓ,f:AB,p:isEquiv(f),q:isEquiv(f)proptruncisEquiv(f,p,q):Id isEquiv(f)(p,q)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:A \to B, p:\mathrm{isEquiv}(f), q:\mathrm{isEquiv}(f) \vdash \mathrm{proptruncisEquiv}(f, p, q):\mathrm{Id}_{\mathrm{isEquiv}(f)}(p, q)}

Breaking the functions down, the inference rules become

ΓAtypeΓBtypeΓ,f:ABisEquiv(f)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:A \to B \vdash \mathrm{isEquiv}(f)}
ΓAtypeΓBtypeΓ,f:AB,g:BA,G: y:BId B(f(g(y)),y),H: x:AId A(g(f(x)),x)qinvtoisEquiv(f,g,G,H):isEquiv(f)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:A \to B, g:B \to A, G:\prod_{y:B} \mathrm{Id}_B(f(g(y)), y), H:\prod_{x:A} \mathrm{Id}_A(g(f(x)), x) \vdash \mathrm{qinvtoisEquiv}(f, g, G, H):\mathrm{isEquiv}(f)}
ΓAtypeΓBtypeΓ,f:AB,p:isEquiv(f)isEquivtoqinv(f,p): g:BA( y:BId B(f(g(y)),y))×( x:AId A(g(f(x)),x))\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:A \to B, p:\mathrm{isEquiv}(f) \vdash \mathrm{isEquivtoqinv}(f, p):\sum_{g:B \to A} \left(\prod_{y:B} \mathrm{Id}_B(f(g(y)), y)\right) \times \left(\prod_{x:A} \mathrm{Id}_A(g(f(x)), x)\right)}
ΓAtypeΓBtypeΓ,f:AB,p:isEquiv(f),q:isEquiv(f)proptruncisEquiv(f,p,q):Id isEquiv(f)(p,q)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:A \to B, p:\mathrm{isEquiv}(f), q:\mathrm{isEquiv}(f) \vdash \mathrm{proptruncisEquiv}(f, p, q):\mathrm{Id}_{\mathrm{isEquiv}(f)}(p, q)}

One could postulate a single equality judgment between types ABtypeA \equiv B \; \mathrm{type} which reflects into an equivalence:

ΓBAtypeΓdef A,B: f:ABisEquiv(f)\frac{\Gamma \vdash B \equiv A \; \mathrm{type}}{\Gamma \vdash \mathrm{def}_{A, B}:\sum_{f:A \to B} \mathrm{isEquiv}(f)}

A similar equality judgment could be made for terms, with a similar rule to reflect it into an identification:

Γba:AΓdef A,a,b:Id A(a,b)\frac{\Gamma \vdash b \equiv a:A}{\Gamma \vdash \mathrm{def}_{A, a, b}:\mathrm{Id}_A(a, b)}

These equalities, while judgmental, are different from the judgmental equality found in other dependent type theories like Martin-Löf type theory and cubical type theory in that they have neither the structural rules nor the congruence rules found in those theories: they are only a formalization of a notational representation of definitional equality and definitional equivalence otherwise represented by identity types and equivalence types.

Without a separate type judgment

In this section, we describe a formalization of objective type theory using an infinite hierarchy of Russell universes with cumulativity, in the style of UPF 2013.

Judgments, contexts, and universes

This presentation of objective type theory consists of the following judgments:

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

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

In addition, we have a countably infinite number of inference rules for the countably infinite number of Russell universes Type 0,Type 1,Type 2,\mathrm{Type}_0, \mathrm{Type}_1, \mathrm{Type}_2, \ldots in the theory, here represented by a natural numbers metavariable for conciseness:

ΓctxΓType i:Type i+1\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Type}_i:\mathrm{Type}_{i + 1}}

as well as inference rules for either cumulativity, that any type in a universe is also in the next universe of the hierarchy, or lifting, that any type in a universe can be lifted to the next universe of the hierarchy:

ΓA:Type iΓA:Type i+1cumulΓA:Type iΓLift(A):Type i+1lifting\frac{\Gamma \vdash A:\mathrm{Type}_i}{\Gamma \vdash A:\mathrm{Type}_{i + 1}}\mathrm{cumul} \qquad \frac{\Gamma \vdash A:\mathrm{Type}_i}{\Gamma \vdash \mathrm{Lift}(A):\mathrm{Type}_{i + 1}}\mathrm{lifting}

Contexts are lists of element judgments a:Aa:A, b:Bb:B, c:Cc:C, et cetera, and are formalized by the inference rules for the empty context and extending the context by a element judgment

()ctxΓctxΓA:Type i(Γ,a:A)ctx\frac{}{() \; \mathrm{ctx}} \qquad \frac{\Gamma \; \mathrm{ctx} \quad \Gamma \vdash A:\mathrm{Type}_i}{(\Gamma, a:A) \; \mathrm{ctx}}

Variable rule

There is one additional structural rule in objective type theory, the variable 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}

Admissible structural rules

The weakening rule and the substitution rule 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.

Let 𝒥\mathcal{J} be any arbitrary judgment. Then the weakening rule is

Γ,Δ𝒥ΓA:Type iΓ,a:A,Δ𝒥\frac{\Gamma, \Delta \vdash \mathcal{J} \quad \Gamma \vdash A:\mathrm{Type}_i}{\Gamma, a:A, \Delta \vdash \mathcal{J}}

and the substitution rule is

Γ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)}

Families of types and elements

A family of elements is an element b:Bb:B in the context of the variable judgment x:Ax:A, x:Ab:Bx:A \vdash b:B. They are 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.

Since types are elements of universe, a family of types is simply a family of elements of universes.

Identity types

Formation rules for identity types:

ΓA:Type iΓ,a:A,b:Aa= Ab:Type i\frac{\Gamma \vdash A:\mathrm{Type}_i}{\Gamma, a:A, b:A \vdash a =_A b:\mathrm{Type}_i}

Introduction rules for identity types:

ΓA:Type iΓ,a:Arefl A(a):a= Aa\frac{\Gamma \vdash A:\mathrm{Type}_i}{\Gamma, a:A \vdash \mathrm{refl}_A(a) : a =_A a}

Elimination rule for identity types:

Γ,x:A,y:A,p:x= Ay,Δ(x,y,p)C(x,y,p):Type iΓ,x:A,t:C(x,x,refl A(x),y:A,p:x= Ay,Δ(x,t,y,p)ind = A(x,t,y,p):C(x,y,p)\frac{\Gamma, x:A, y:A, p:x =_A y, \Delta(x, y, p) \vdash C(x, y, p):\mathrm{Type}_i}{\Gamma, x:A, t:C(x, x, \mathrm{refl}_A(x), y:A, p:x =_A y, \Delta(x, t, y, p) \vdash \mathrm{ind}_{=_A}(x, t, y, p):C(x, y, p)}

Computation rules for identity types:

Γ,x:A,y:A,p:x= Ay,Δ(x,y,p)C(x,y,p):Type iΓ,x:A,t:C(x,x,refl A(x),Δ(x,t,x,refl A(x))β = A(x,t):ind = A(x,t,x,refl A(x))= C(x,x,refl A(x))t\frac{\Gamma, x:A, y:A, p:x =_A y, \Delta(x, y, p) \vdash C(x, y, p):\mathrm{Type}_i}{\Gamma, x:A, t:C(x, x, \mathrm{refl}_A(x), \Delta(x, t, x, \mathrm{refl}_A(x)) \vdash \beta_{=_A}(x, t):\mathrm{ind}_{=_A}(x, t, x, \mathrm{refl}_A(x)) =_{C(x, x, \mathrm{refl}_A(x))} t}

Definitions

Definitions of a symbol bb for the element a:Aa:A are made by using identity types between the symbol and element: def a,b:a= Ab\mathrm{def}_{a, b}:a =_A b. Definitions of a symbol BB for the type A:Type iA:\mathrm{Type}_i are made in the same way, as def A,B:A= Type iB\mathrm{def}_{A, B}:A =_{\mathrm{Type}_i} B. Thus, the identity type behaves very similarly to explicit conversion as discussed in section 9.2 of Winterhalter2020.

Dependent function types

Formation rules for dependent function types:

ΓA:Type iΓ,x:AB(x):Type iΓ x:AB(x):Type i\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma, x:A \vdash B(x):\mathrm{Type}_i}{\Gamma \vdash \prod_{x:A} B(x):\mathrm{Type}_i}

Introduction rules for dependent function types:

ΓA:Type iΓ,x:AB(x):Type iΓ,x:Ab(x):B(x)Γλ(x:A).b(x): x:AB(x)\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma, x:A \vdash B(x):\mathrm{Type}_i \quad \Gamma, x:A \vdash b(x):B(x)}{\Gamma \vdash \lambda(x:A).b(x):\prod_{x:A} B(x)}

Elimination rules for dependent function types:

ΓA:Type iΓ,x:AB(x):Type iΓ,f: x:AB(x),a:Aind x:AB(x)(f,a):B(a)\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma, x:A \vdash B(x):\mathrm{Type}_i}{\Gamma, f:\prod_{x:A} B(x), a:A \vdash \mathrm{ind}_{\prod_{x:A} B(x)}(f, a):B(a)}

Computation rules for dependent function types

ΓA:Type iΓ,x:AB(x):Type iΓ,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}_i \quad \Gamma, x:A \vdash B(x):\mathrm{Type}_i \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)}

Uniqueness rules for dependent function types:

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

Function types

Formation rules for function types:

ΓA:Type iΓB:Type iΓAB:Type i\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:\mathrm{Type}_i}{\Gamma \vdash A \to B:\mathrm{Type}_i}

Introduction rules for function types:

ΓA:Type iΓB:Type iΓ,x:Ab(x):BΓλ(x:A).b(x):AB\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:\mathrm{Type}_i \quad \Gamma, x:A \vdash b(x):B}{\Gamma \vdash \lambda(x:A).b(x):A \to B}

Elimination rules for function types:

ΓA:Type iΓB:Type iΓ,f:AB,a:Aind AB(f,a):B\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:\mathrm{Type}_i}{\Gamma, f:A \to B, a:A \vdash \mathrm{ind}_{A \to B}(f, a):B}

Computation rules for function types

ΓA:Type iΓB:Type iΓ,x:Ab(x):BΓ,a:Aβ AB(a):ind AB(λ(x:A).b(x),a)= Bb(a)\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:\mathrm{Type}_i \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:

ΓA:Type iΓB:Type iΓ,f:ABη AB(f):f= ABλ(x:A).ind AB(f,x)\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:\mathrm{Type}_i}{\Gamma, f:A \to B \vdash \eta_{A \to B}(f):f =_{A \to B} \lambda(x:A).\mathrm{ind}_{A \to B}(f, x)}

Pair types

Formation rules for pair types:

ΓA:Type iΓB:Type iΓA×B:Type i\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:\mathrm{Type}_i}{\Gamma \vdash A \times B:\mathrm{Type}_i}

Introduction rules for pair types:

ΓA:Type iΓB:Type iΓ,x:A,y:Bin(x,y):A×B\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:\mathrm{Type}_i}{\Gamma, x:A, y:B \vdash \mathrm{in}(x, y):A \times B}

Elimination rules for pair types:

ΓA:Type iΓB:Type iΓ,z:A×Bind A×B A(z):AΓA:Type iΓB:Type iΓ,z:A×Bind A×B B(z):B\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:\mathrm{Type}_i}{\Gamma, z:A \times B \vdash \mathrm{ind}_{A \times B}^A(z):A} \qquad \frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:\mathrm{Type}_i}{\Gamma, z:A \times B \vdash \mathrm{ind}_{A \times B}^B(z):B}

Computation rules for pair types:

ΓA:Type iΓB:Type iΓ,x:A,y:Bβ A×B A(x,y):ind A×B A(in(x,y))= Ax\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:\mathrm{Type}_i}{\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}
ΓA:Type iΓB:Type iΓ,x:A,y:Bβ A×B B(x,y):ind A×B B(in(x,y))= By\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:\mathrm{Type}_i}{\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:

ΓA:Type iΓB:Type iΓ,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}_i \quad \Gamma \vdash B:\mathrm{Type}_i}{\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:

ΓA:Type iΓ,x:AB(x):Type iΓ x:AB(x):Type i\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma, x:A \vdash B(x):\mathrm{Type}_i}{\Gamma \vdash \sum_{x:A} B(x):\mathrm{Type}_i}

Introduction rules for dependent pair types:

ΓA:Type iΓ,x:AB(x):Type iΓ,x:A,y:B(x)in(x,y): x:AB(x)\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma, x:A \vdash B(x):\mathrm{Type}_i}{\Gamma, x:A, y:B(x) \vdash \mathrm{in}(x, y):\sum_{x:A} B(x)}

Elimination rules for dependent pair types:

ΓA:Type iΓ,x:AB(x):Type iΓ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}_i \quad \Gamma, x:A \vdash B(x):\mathrm{Type}_i}{\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:

ΓA:Type iΓ,x:AB(x):Type iΓ,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}_i \quad \Gamma, x:A \vdash B(x):\mathrm{Type}_i}{\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}
ΓA:Type iΓ,x:AB(x):Type iΓ,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}_i \quad \Gamma, x:A \vdash B(x):\mathrm{Type}_i}{\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:

ΓA:Type iΓ,x:AB(x):Type iΓ,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}_i \quad \Gamma, x:A \vdash B(x):\mathrm{Type}_i}{\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))}

isContr, uniqueness quantifiers, isEquiv, and equivalence types

Now that we have identity types, dependent sum types, and dependent product types, we can use that to define

ΓA:Type iΓisContr(A):Type iΓA:Type iΓdefisContr(A):isContr(A)= Type i y:A z:Ay= Az\frac{\Gamma \vdash A:\mathrm{Type}_i}{\Gamma \vdash \mathrm{isContr}(A):\mathrm{Type}_i} \qquad \frac{\Gamma \vdash A:\mathrm{Type}_i}{\Gamma \vdash \mathrm{defisContr}(A):\mathrm{isContr}(A) =_{\mathrm{Type}_i} \sum_{y:A} \prod_{z:A} y =_{A} z}
ΓA:Type iΓ,x:AB(x):Type iΓ!x:A.B(x):Type iΓA:Type iΓ,x:AB(x):Type iΓdef! x:A.B(x):!x:A.B(x)= Type iisContr( x:AB(x))\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma, x:A \vdash B(x):\mathrm{Type}_i}{\Gamma \vdash \exists!x:A.B(x):\mathrm{Type}_i} \qquad \frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma, x:A \vdash B(x):\mathrm{Type}_i}{\Gamma \vdash \mathrm{def}\exists!_{x:A.B(x)}:\exists!x:A.B(x) =_{\mathrm{Type}_i} \mathrm{isContr}\left(\sum_{x:A} B(x)\right)}
ΓA:Type iΓB:Type iΓ,f:ABisEquiv(f):Type iΓA:Type iΓB:Type iΓ,f:ABdefisEquiv A,B(f):isEquiv(f)= Type i y:B!x:A.f(x)= By\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:\mathrm{Type}_i}{\Gamma, f:A \to B \vdash \mathrm{isEquiv}(f):\mathrm{Type}_i} \qquad \frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:\mathrm{Type}_i}{\Gamma, f:A \to B \vdash \mathrm{defisEquiv}_{A, B}(f):\mathrm{isEquiv}(f) =_{\mathrm{Type}_i} \prod_{y:B} \exists!x:A.f(x) =_{B} y}
ΓA:Type iΓB:Type iΓAB:Type iΓA:Type iΓB:Type iΓdef AB:(AB)= Type i f:ABisEquiv(f)\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:\mathrm{Type}_i}{\Gamma \vdash A \simeq B:\mathrm{Type}_i} \qquad \frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:\mathrm{Type}_i}{\Gamma \vdash \mathrm{def}_{A \simeq B}:(A \simeq B) =_{\mathrm{Type}_i} \sum_{f:A \to B} \mathrm{isEquiv}(f)}

Univalence

The univalence axiom states that the identity type between two types of a universe is equivalent to the equivalence type between said types:

ΓA:Type iΓB:Type iΓua i(A,B):(A= Type iB)(AB)\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:\mathrm{Type}_i}{\Gamma \vdash \mathrm{ua}_i(A, B):(A =_{\mathrm{Type}_i} B) \simeq (A \simeq B)}

Positive types

Now that we have the uniqueness quantifier we can combine the elimination rule, the computation rule, and the uniqueness rule for any positive type into one rule, the induction rule.

Unit type

Formation rules for the unit type:

ΓctxΓ𝟙:Type i\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{1}:\mathrm{Type}_i}

Introduction rules for the unit type:

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

Induction rule for the unit type:

Γ,x:𝟙C(x):Type iΓ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}_i \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})}
Empty type

Formation rules for the empty type:

ΓctxΓ𝟘:Type i\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{0}:\mathrm{Type}_i}

Induction rule for the empty type:

Γ,x:𝟘C(x):Type iΓup 𝟘 C:isContr( x:𝟘C(x))\frac{\Gamma, x:\mathbb{0} \vdash C(x):\mathrm{Type}_i}{\Gamma \vdash \mathrm{up}_\mathbb{0}^C:\mathrm{isContr}\left(\prod_{x:\mathbb{0}} C(x)\right)}
Booleans type

Formation rules for the booleans type:

ΓctxΓ𝟚:Type i\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{2}:\mathrm{Type}_i}

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}}

Induction rule for the booleans type:

Γ,x:𝟚C(x):Type iΓ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}_i \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)}
Natural numbers type

Formation rules for the natural numbers type:

ΓctxΓ:Type i\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{N}:\mathrm{Type}_i}

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}}

Induction rule for the natural numbers type:

Γ,x:C(x):Type iΓ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}_i \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 i\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{Z}:\mathrm{Type}_i}

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}}

Induction rule for the integers type:

Γ,x:C(x):Type iΓ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}_i \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))}

With a separate type judgment

In this section, we describe a formalization of objective type theory using a type judgment, in the style of Rijke 2022.

Judgments and contexts

This presentation of objective type theory consists of the following judgments:

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

  • Element judgments, where we judge aa to be an element of AA, a:Aa: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}}

Variable rule

There is one additional structural rule in objective type theory, the variable 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}

Admissible structural rules

The weakening rule and the substitution rule 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.

Let 𝒥\mathcal{J} be any arbitrary judgment. Then the weakening rule is

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

and the substitution rule is

Γ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)}

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.

Identity types

Formation rules for identity types:

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

Introduction rules for identity types:

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

Elimination rule for identity types:

Γ,x:A,y:A,p:x= AyC(x,y,p)typeΓ,x:A,t:C(x,x,refl A(x),y:A,p:x= Ay,Δ(x,t,y,p)ind = A(x,t,y,p):C(x,y,p)\frac{\Gamma, x:A, y:A, p:x =_A y \vdash C(x, y, p) \; \mathrm{type}}{\Gamma, x:A, t:C(x, x, \mathrm{refl}_A(x), y:A, p:x =_A y, \Delta(x, t, y, p) \vdash \mathrm{ind}_{=_A}(x, t, y, p):C(x, y, p)}

Computation rules for identity types:

Γ,x:A,y:A,p:x= Ay,Δ(x,y,p)C(x,y,p)typeΓ,x:A,t:C(x,x,refl A(x)β = A(x,t):ind = A(x,t,x,refl A(x))= C(x,x,refl A(x))t\frac{\Gamma, x:A, y:A, p:x =_A y, \Delta(x, y, p) \vdash C(x, y, p) \; \mathrm{type}}{\Gamma, x:A, t:C(x, x, \mathrm{refl}_A(x) \vdash \beta_{=_A}(x, t):\mathrm{ind}_{=_A}(x, t, x, \mathrm{refl}_A(x)) =_{C(x, x, \mathrm{refl}_A(x))} t}

Dependent function types

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 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 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 dependent function types

ΓAtypeΓ,x:AB(x)typeΓ,x:Ab(x):B(x)Γβ x:AB(x) x:A.b(x): a:Aind 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 \vdash \beta_{\prod_{x:A} B(x)}^{x:A.b(x)}:\prod_{a:A} \mathrm{ind}_{\prod_{x:A} B(x)}(\lambda(x:A).b(x), a) =_{B(a)} b(a)}

Uniqueness rules for dependent function types:

ΓAtypeΓ,x:AB(x)typeΓ,f: x:AB(x)η x:AB(x)(f):f= x:AB(x)λ(x:A).ind x:AB(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:A).\mathrm{ind}_{\prod_{x:A} B(x)}(f, x)}

Equivalence types

Formation rules for equivalence types:

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

Introduction rules for equivalence types:

ΓAtypeΓBtypeΓf: x:ABΓg: y:BA ΓG: x:Ag(f(x))= AxΓH: y:Bf(g(y))= By ΓK: x:AH(f(x))= f(g(f(x))= Bf(x)ap f(f(g(x)),x,G(x))cΓtoEquiv(f,g,G,H,K):AB\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:\prod_{x:A} B \quad \Gamma \vdash g:\prod_{y:B} A \\ \Gamma \vdash G:\prod_{x:A} g(f(x)) =_{A} x \quad \Gamma \vdash H:\prod_{y:B} f(g(y)) =_{B} y \\ \Gamma \vdash K:\prod_{x:A} H(f(x)) =_{f(g(f(x)) =_{B} f(x)} \mathrm{ap}_f(f(g(x)), x, G(x)) \end{array}{c} }{\Gamma \vdash \mathrm{toEquiv}(f, g, G, H, K):A \simeq B}

Elimination rules for equivalence types:

ΓAtypeΓBtypeΓe:ABΓfunc(e): x:AB\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B}{\Gamma \vdash \mathrm{func}(e):\prod_{x:A} B}
ΓAtypeΓBtypeΓe:ABΓfinv(e): y:BA\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B}{\Gamma \vdash \mathrm{finv}(e):\prod_{y:B} A}
ΓAtypeΓBtypeΓe:ABΓsec(e): x:Afinv(e)(func(e)(x))= Ax\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B}{\Gamma \vdash \mathrm{sec}(e):\prod_{x:A} \mathrm{finv}(e)(\mathrm{func}(e)(x)) =_A x}
ΓAtypeΓBtypeΓe:ABΓret(e): y:Bfunc(e)(finv(e)(y)= By\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B}{\Gamma \vdash \mathrm{ret}(e):\prod_{y:B} \mathrm{func}(e)(\mathrm{finv}(e)(y) =_{B} y}
ΓAtypeΓBtypeΓe:ABΓcoh(e): x:AH(f(x))= f(g(f(x))= Bf(x)ap f(f(g(x)),x,G(x))\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B}{\Gamma \vdash \mathrm{coh}(e):\prod_{x:A} H(f(x)) =_{f(g(f(x)) =_{B} f(x)} \mathrm{ap}_f(f(g(x)), x, G(x))}

Computation rules for equivalence types:

ΓAtypeΓBtypeΓf: x:ABΓg: y:BA ΓG: x:Ag(f(x))= AxΓH: y:Bf(g(y))= By ΓK: x:AH(f(x))= f(g(f(x))= Bf(x)ap f(f(g(x)),x,G(x))Γβ AB func(f,g,G,H,K):func(toEquiv(f,g,G,H,K))= x:ABf\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:\prod_{x:A} B \quad \Gamma \vdash g:\prod_{y:B} A \\ \Gamma \vdash G:\prod_{x:A} g(f(x)) =_{A} x \quad \Gamma \vdash H:\prod_{y:B} f(g(y)) =_{B} y \\ \Gamma \vdash K:\prod_{x:A} H(f(x)) =_{f(g(f(x)) =_{B} f(x)} \mathrm{ap}_f(f(g(x)), x, G(x)) \end{array} }{\Gamma \vdash \beta_{A \simeq B}^\mathrm{func}(f, g, G, H, K):\mathrm{func}(\mathrm{toEquiv}(f, g, G, H, K)) =_{\prod_{x:A} B} f}
ΓAtypeΓBtypeΓf: x:ABΓg: y:BA ΓG: x:Ag(f(x))= AxΓH: y:Bf(g(y))= By ΓK: x:AH(f(x))= f(g(f(x))= Bf(x)ap f(f(g(x)),x,G(x))Γβ AB finv(f,g,G,H,K):finv(toEquiv(f,g,G,H,K))= y:BAg\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:\prod_{x:A} B \quad \Gamma \vdash g:\prod_{y:B} A \\ \Gamma \vdash G:\prod_{x:A} g(f(x)) =_{A} x \quad \Gamma \vdash H:\prod_{y:B} f(g(y)) =_{B} y \\ \Gamma \vdash K:\prod_{x:A} H(f(x)) =_{f(g(f(x)) =_{B} f(x)} \mathrm{ap}_f(f(g(x)), x, G(x)) \end{array} }{\Gamma \vdash \beta_{A \simeq B}^\mathrm{finv}(f, g, G, H, K):\mathrm{finv}(\mathrm{toEquiv}(f, g, G, H, K)) =_{\prod_{y:B} A} g}
ΓAtypeΓBtypeΓf: x:ABΓg: y:BA ΓG: x:Ag(f(x))= AxΓH: y:Bf(g(y))= By ΓK: x:AH(f(x))= f(g(f(x))= Bf(x)ap f(f(g(x)),x,G(x))Γβ AB sec(f,g,G,H,K):sec(toEquiv(f,g,G,H,K))= y:Bf(g(y))= ByG\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:\prod_{x:A} B \quad \Gamma \vdash g:\prod_{y:B} A \\ \Gamma \vdash G:\prod_{x:A} g(f(x)) =_{A} x \quad \Gamma \vdash H:\prod_{y:B} f(g(y)) =_{B} y \\ \Gamma \vdash K:\prod_{x:A} H(f(x)) =_{f(g(f(x)) =_{B} f(x)} \mathrm{ap}_f(f(g(x)), x, G(x)) \end{array} }{\Gamma \vdash \beta_{A \simeq B}^\mathrm{sec}(f, g, G, H, K):\mathrm{sec}(\mathrm{toEquiv}(f, g, G, H, K)) =_{\prod_{y:B} f(g(y)) =_{B} y} G}
ΓAtypeΓBtypeΓf: x:ABΓg: y:BA ΓG: x:Ag(f(x))= AxΓH: y:Bf(g(y))= By ΓK: x:AH(f(x))= f(g(f(x))= Bf(x)ap f(f(g(x)),x,G(x))Γβ AB ret(f,g,G,H,K):ret(toEquiv(f,g,G,H,K))= x:Ag(f(x))= AxH\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:\prod_{x:A} B \quad \Gamma \vdash g:\prod_{y:B} A \\ \Gamma \vdash G:\prod_{x:A} g(f(x)) =_{A} x \quad \Gamma \vdash H:\prod_{y:B} f(g(y)) =_{B} y \\ \Gamma \vdash K:\prod_{x:A} H(f(x)) =_{f(g(f(x)) =_{B} f(x)} \mathrm{ap}_f(f(g(x)), x, G(x)) \end{array} }{\Gamma \vdash \beta_{A \simeq B}^\mathrm{ret}(f, g, G, H, K):\mathrm{ret}(\mathrm{toEquiv}(f, g, G, H, K)) =_{\prod_{x:A} g(f(x)) =_{A} x} H}
ΓAtypeΓBtypeΓf: x:ABΓg: y:BA ΓG: x:Ag(f(x))= AxΓH: y:Bf(g(y))= By ΓK: x:AH(f(x))= f(g(f(x))= Bf(x)ap f(f(g(x)),x,G(x))Γβ AB coh(f,g,G,H,K):coh(toEquiv(f,g,G,H,K))= x:AH(f(x))= f(g(f(x))= Bf(x)ap f(f(g(x)),x,G(x))K\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:\prod_{x:A} B \quad \Gamma \vdash g:\prod_{y:B} A \\ \Gamma \vdash G:\prod_{x:A} g(f(x)) =_{A} x \quad \Gamma \vdash H:\prod_{y:B} f(g(y)) =_{B} y \\ \Gamma \vdash K:\prod_{x:A} H(f(x)) =_{f(g(f(x)) =_{B} f(x)} \mathrm{ap}_f(f(g(x)), x, G(x)) \end{array} }{\Gamma \vdash \beta_{A \simeq B}^\mathrm{coh}(f, g, G, H, K):\mathrm{coh}(\mathrm{toEquiv}(f, g, G, H, K)) =_{\prod_{x:A} H(f(x)) =_{f(g(f(x)) =_{B} f(x)} \mathrm{ap}_f(f(g(x)), x, G(x))} K}

Uniqueness rules for equivalence types:

ΓAtypeΓBtypeΓe:ABΓη AB(e):toEquiv(func(e),finv(e),sec(e),ret(e),coh(e))= ABe\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B}{\Gamma \vdash \eta_{A \simeq B}(e):\mathrm{toEquiv}(\mathrm{func}(e), \mathrm{finv}(e), \mathrm{sec}(e), \mathrm{ret}(e), \mathrm{coh}(e)) =_{A \simeq B} e}

Definitions

Definitions of a symbol bb for the element a:Aa:A are made by using identity types between the symbol and element: def a,b:a= Ab\mathrm{def}_{a, b}:a =_A b. Definitions of a symbol BB for the type AtypeA \; \mathrm{type} are made by using equivalence types between the symbol and the type: def A,B:AB\mathrm{def}_{A, B}:A \simeq B.

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Γβ AB x:A.b(x): a:Aind 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 \vdash \beta_{A \to B}^{x:A.b(x)}:\prod_{a:A} \mathrm{ind}_{A \to B}(\lambda(x:A).b(x), a) =_{B} b(a)}

Uniqueness rules for function types:

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

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))}

isContr and uniqueness quantifiers

Now that we have equivalence types, identity types, dependent sum types, and dependent product types, we can use that to define

ΓAtypeΓisContr(A)typeΓAtypeΓdefisContr(A):isContr(A) y:A z:Ay= Az\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{isContr}(A) \; \mathrm{type}} \qquad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{defisContr}(A):\mathrm{isContr}(A) \simeq \sum_{y:A} \prod_{z:A} y =_{A} z}
ΓAtypeΓ,x:AB(x)typeΓ!x:A.B(x)typeΓAtypeΓ,x:AB(x)typeΓdef! x:A.B(x):!x:A.B(x)isContr( x:AB(x))\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \exists!x:A.B(x) \; \mathrm{type}} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{def}\exists!_{x:A.B(x)}:\exists!x:A.B(x) \simeq \mathrm{isContr}\left(\sum_{x:A} B(x)\right)}

Positive types

Now that we have the uniqueness quantifier we can combine the elimination rule, the computation rule, and the uniqueness rule for any positive type into one rule, the induction rule.

Empty type

Formation rules for the empty type:

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

Recursion rule for the empty type:

ΓCtypeΓup 𝟘 C:isContr(𝟘C)\frac{\Gamma \vdash C \; \mathrm{type}}{\Gamma \vdash \mathrm{up}_\mathbb{0}^C:\mathrm{isContr}\left(\mathbb{0} \to C\right)}

Induction rule for the empty type:

Γ,x:𝟘C(x)typeΓdup 𝟘 C:isContr( x:𝟘C(x))\frac{\Gamma, x:\mathbb{0} \vdash C(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{dup}_\mathbb{0}^C:\mathrm{isContr}\left(\prod_{x:\mathbb{0}} C(x)\right)}
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}}

Recursion rule for the unit type:

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

Induction rule for the unit type:

Γ,x:𝟙C(x)typeΓc pt:C(pt)Γdup 𝟙 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{dup}_\mathbb{1}^C(c_\mathrm{pt}):\exists!c:\prod_{x:\mathbb{1}} C(x).(c(\mathrm{pt}) =_{C(\mathrm{pt})} c_\mathrm{pt})}
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}}

Recursion rule for the booleans type:

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

Induction rule for the booleans type:

Γ,x:𝟚C(x)typeΓc 0:C(0)Γc 1:C(1)Γdup 𝟚 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{dup}_\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)}
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}}

Recursion rule for the natural numbers type:

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

Induction rule for the natural numbers type:

Γ,x:C(x)typeΓc 0:C(0)Γc s: x:C(x)C(s(x))Γdup 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{dup}_\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}}

Recursion rule for the integers type:

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

Induction 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))}

 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.

See also

 References

The original paper on this topic:

General dependent type theory references used for the formalizations of objective type theory in this article:

Last revised on February 6, 2024 at 23:36:50. See the history of this page for a list of all contributions to it.