Homotopy Type Theory propositional logic > history (Rev #2, changes)

\tableofcontents

\section{Idea}

Propositional logic could be represented in dependent type theory.

\section{Presentation}

The model of dependent type theory we shall be presenting here is the objective type theory version of dependent type theory. There are multiple reasons for this:

• Since objective type theory lacks definitional equality,

  • The ruleset is simpler in the objective type theory model of homotopy type theory than other models such as Martin-Löf type theory, cubical type theory, or higher observational type theory

  • The results in objective type theory are more general than in models which use definitional equality

  • It 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, which is propositional equality in both objective type theory and set theory, and uses propositional equality to define terms and types.

• From a more practical standpoint, objective type theory not only has decidable type checking, it has polynomial (quadratic) time type checking, which makes it efficient from a computational standpoint.

\subsection{Judgments and contexts}

The objective type theory model of propositional logic consists of three judgments: proposition judgments $A \; \mathrm{prop}$, where we judge $A$ to be a proposition, proof judgments, where we judge $a$ to be a proof of $A$, $a:A$, and context judgments, where we judge $\Gamma$ to be a context, $\Gamma \; \mathrm{ctx}$. Contexts are lists of proof judgments $a:A$, $b:B$, $c:C$, et cetera, and are formalized by the rules for the empty context and extending the context by a proof judgment

\subsection{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 proof judgment if the proof judgment is in the context already:

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

The weakening rule:

The substitution rule:

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

\subsection{Predicates and dependent proof}

A predicate is a proposition $B$ in the context of the variable judgment $x:A$, $x:A \vdash B \; \mathrm{prop}$, they are usually written as $B(x)$ to indicate its dependence upon $x$.

A dependent proof is a proof $b:B$ in the context of the variable judgment $x:A$, $x:A \vdash b:B$. dependent proofs are likewise usually written as $b(x)$ to indicate its dependence upon $x$.

\subsection{Equality}

Equality of proofs of a proposition is represented by a proposition known as the equality proposition. The elements of the equality proposition are called equalities.

Equality comes with a formation rule, an introduction rule, an elimination rule, and a computation rule:

Formation rule for equality propositions:

Introduction rule for equality propositions:

Elimination rule for equality propositions:

Computation rules for equality propositions:

\subsection{Propositional truncation}

One also adds the propositional truncation rule for propositions:

which ensures that every proposition behaves like an h-proposition in dependent type theory.

\section{See also}

• dependent type theory