Chapter 153Optional

Setoid and PER Models of Type Theory

Prerequisites. Direct starred prerequisites: none. Chapter 54 supplies the semantic interface and chapter 55 the first model. No later core chapter depends on this route.

Write $Z$ as pairs of naturals: $(m, n)$ stands for $m - n$ , and $(m, n) \sim (m^{'}, n^{'})$ means $m + n^{'} = m^{'} + n$ . A function out of the integers must not depend on the representative, so to define, say, negation one gives $ν (m, n) : = (n, m)$ together with a proof that $ν$ respects $\sim$ . In the set model of chapter 55 nothing forces this: a family over the set of pairs may take different values at $(0, 0)$ and $(1, 1)$ , and the interpretation accepts it. The type theory can be made to force it only by carrying the respect proof by hand in every construction — the coherence burden that quotient-free intensional theories are known for.

The remedy is to change what a type is. Let a type carry its own equality, let a function be a pair of a raw function and a proof that it respects the two equalities, and let the interpretation of the identity type be that carried equality. The obligation then becomes part of the data, and the model validates rules — extensionality, quotient formation — that the set model does not even state. Two versions of this idea are developed here: setoids in an intensional metatheory, and partial equivalence relations over a model of untyped computation.

Setoids, extensional maps, and levels

Definition 153.1 — Setoid ¶

A setoid $A$ is a pair $(| A |, =_{A})$ of a type $| A |$ of the ambient intensional metatheory and a family $=_{A}$ of types over $| A | \times | A |$ together with proofs of reflexivity, symmetry and transitivity. An extensional map $f : A \to B$ is a pair $(| f |, {ext}_{f})$ of a function $| f | : | A | \to | B |$ and a proof of $(\forall x, y : | A |) [x =_{A} y \Rightarrow | f | (x) =_{B} | f | (y)] .$ Two extensional maps are equal, $f =_{A \to B} g$ , when $(\forall x : | A |) | f | (x) =_{B} | g | (x)$ . We write $a : A$ for $a : | A |$ and $f (x)$ for $| f | (x)$ .

Referenced from 3 locations

Setoid and PER Models of Type Theory

Definition 153.2 — Product and exponent ¶

$| A \times B | : = | A | \times | B |$ with $(a, b) =_{A \times B} (c, d)$ iff $a =_{A} c$ and $b =_{B} d$ . The exponent $[A \to B]$ has $| [A \to B] | : = \sum_{f : | A | \to | B |} (\forall x, y : | A |) (x =_{A} y \Rightarrow f (x) =_{B} f (y)),$ with $(f, p) =_{[A \to B]} (g, q)$ iff $(\forall x : | A |) f (x) =_{B} g (x)$ .

Referenced from 3 locations

Setoid and PER Models of Type Theory

The equality of $[A \to B]$ is pointwise and forgets the proof component; that single choice is what will make function extensionality hold and proof irrelevance available.

Definition 153.3 — Levels ¶

Let $U_{0}, U_{1}, \dots$ be the cumulative universes of the metatheory. An $(m, n)$ -setoid is a setoid with $| A | \in U_{m}$ and $=_{A}$ valued in $U_{n}$ . An $(n, n)$ -setoid is an $n$ -setoid; an $(n + 1, n)$ -setoid is an $n$ -classoid.

Referenced from 3 locations

Setoid and PER Models of Type Theory

Example 153.4 — Three setoids and two classoids ¶

(1) Every type $A \in U_{n}$ is an $n$ -setoid under its identity type. (2) $Ω_{n} : = (U_{n}, \leftrightarrow)$ , propositions under logical equivalence, is an $n$ -classoid: its carrier lives one level up while its equality stays at level $n$ . (3) The integers $Z : = (N \times N, \sim)$ with $(m, n) \sim (m^{'}, n^{'})$ iff $m + n^{'} = m^{'} + n$ is a $0$ -setoid, and negation $ν (m, n) : = (n, m)$ is extensional because $m + n^{'} = m^{'} + n$ gives $n + m^{'} = n^{'} + m$ . (4) For an $n$ -setoid $A$ , the setoid $P_{n} (A) : = [A \to Ω_{n}]$ of extensional predicates is an $n$ -classoid. (5) If $A$ is an $(m, n)$ -setoid and $B$ an $(m^{'}, n^{'})$ -setoid, then $[A \to B]$ is an $(max (m, m^{'}, n, n^{'}), max (m, n^{'}))$ -setoid; in particular $(m, n)$ -setoids are closed under exponents.

Referenced from 5 locations

Setoid and PER Models of Type Theory

Proposition 153.5 — Replacement ¶

Let $f : A \to B$ be extensional with $A$ an $m$ -setoid and $B$ an $m$ -classoid. Then the image $Im (f)$ , that is the subsetoid of $B$ with carrier $| A |$ and equality $x \approx y$ iff $f (x) =_{B} f (y)$ , is an $m$ -setoid.

Referenced from 3 locations

Setoid and PER Models of Type Theory

Proof of Proposition 153.5 — Replacement

Proof. The carrier is $| A | \in U_{m}$ and the relation $f (x) =_{B} f (y)$ is valued in $U_{m}$ because $B$ is an $m$ -classoid, whose equality is at level $m$ . It is an equivalence relation because $=_{B}$ is. Thus both components sit at level $m$ . The point is that the carrier of $B$ may live at level $m + 1$ while the image does not. ◻

Families of setoids

Definition 153.6 — Proof-irrelevant family ¶

A family $F$ over a setoid $A$ assigns a setoid $F (a)$ to each $a : A$ and an extensional map $F (p) : F (a) \to F (b)$ to each proof $p : a =_{A} b$ , subject to

proof irrelevance: $F (p) = F (q)$ for all $p, q : a =_{A} b$ ;
identity: $F (r_{a}) = {id}_{F (a)}$ for the chosen reflexivity proof $r_{a}$ ;
composition: $F (p \cdot q) = F (p) \circ F (q)$ for $q : a =_{A} b$ and $p : b =_{A} c$ , where $\cdot$ is the chosen transitivity.

Write $Ty (A)$ for the families over $A$ .

Referenced from 9 locations

Setoid and PER Models of Type Theory

Lemma 153.7 — Transports are isomorphisms ¶

For every $p : a =_{A} b$ the map $F (p)$ is an isomorphism of setoids with inverse $F (p^{- 1})$ , where $p^{- 1}$ is the chosen symmetry proof.

Referenced from 4 locations

Setoid and PER Models of Type Theory

Proof of Lemma 153.7 — Transports are isomorphisms

Proof. $F (p) \circ F (p^{- 1}) = F (p^{- 1} \cdot p)$ by clause (3), and $p^{- 1} \cdot p$ and $r_{b}$ are two proofs of $b =_{A} b$ , so by clause (1) and then clause (2) the composite is ${id}_{F (b)}$ . Symmetrically on the other side. Nothing here requires $p^{- 1} \cdot p$ and $r_{b}$ to be equal as proofs; only the transports along them are compared. ◻

Definition 153.8 — Global elements, sum and product ¶

A global element of $F \in Ty (A)$ is a family $g (x) : F (x)$ indexed by $x : A$ with $(\forall p : x =_{A} y) F (p) (g (x)) =_{F (y)} g (y) .$ Write $Tm (A, F)$ for the setoid of global elements, with pointwise equality. Define the dependent sum $Σ (A, F)$ by $\begin{aligned} | Σ (A, F) | & : = \sum_{x : | A |} | F (x) |, \\ (x, y) \sim (u, v) & iff (\exists p : x =_{A} u) F (p) (y) =_{F (u)} v, \end{aligned}$ and the dependent product $Π (A, F)$ by $\begin{aligned} | Π (A, F) | & : = \sum_{f : \prod_{x : | A |} | F (x) |} E (f), \\ E (f) & : = (\forall x, y : | A |) (\forall p : x =_{A} y) F (p) (f (x)) =_{F (y)} f (y), \\ f \sim g & iff (\forall x : A) f (x) =_{F (x)} g (x) . \end{aligned}$ Reindexing along an extensional $h : B \to A$ is $F [h] (x) : = F (h (x))$ and $F [h] (p) : = F ({ext}_{h} (p))$ .

Referenced from 6 locations

Setoid and PER Models of Type Theory

Lemma 153.9 — on Σ is an equivalence relation ¶

The relation displayed for $Σ (A, F)$ is reflexive, symmetric and transitive.

Referenced from 3 locations

Setoid and PER Models of Type Theory

Proof of Lemma 153.9 — on Σ is an equivalence relation

Proof. Reflexivity: take $p = r_{x}$ and use clause (2) of definition 153.6. Symmetry: from $p : x =_{A} u$ with $F (p) (y) = v$ , take $p^{- 1}$ and apply $F (p^{- 1})$ , using lemma 153.7. Transitivity: from $p : x =_{A} u$ , $p^{'} : u =_{A} w$ with $F (p) (y) = v$ and $F (p^{'}) (v) = z$ , take $p^{'} \cdot p$ and use clause (3): $F (p^{'} \cdot p) (y) = F (p^{'}) (F (p) (y)) = F (p^{'}) (v) = z$ . Proof irrelevance is what makes the existential quantifier harmless: the truth of the relation does not depend on which $p$ is chosen. ◻

Proposition 153.10 — Reindexing is strictly functorial ¶

For extensional $h : B \to A$ and $k : C \to B$ , $F [{id}_{A}] = F$ and $F [h \circ k] = F [h] [k]$ , and the same equations hold for global elements.

Referenced from 6 locations

Setoid and PER Models of Type Theory

Proof of Proposition 153.10 — Reindexing is strictly functorial

Proof. On carriers both sides are given by composition of the underlying functions, which is strictly associative and unital. On proofs, the transport component of $F [h \circ k]$ at $p$ is $F ({ext}_{h \circ k} (p))$ while that of $F [h] [k]$ is $F ({ext}_{h} ({ext}_{k} (p)))$ ; these are transports along two proofs of the same equation, hence equal by clause (1) of definition 153.6. This is the first place where proof irrelevance is not a convenience but a requirement: without it the model would satisfy the substitution laws only up to isomorphism. ◻

Theorem 153.11 — The setoid model ¶

Let $Std$ have as contexts the setoids, as substitutions the extensional maps, $Ty$ and $Tm$ as in definition 153.6, definition 153.8, and comprehension $A . F : = Σ (A, F)$ with $p_{F} (x, y) : = x$ and $q_{F} (x, y) : = y$ . Then $Std$ is a category with families in the sense of definition 54.16.

Referenced from 4 locations

Setoid and PER Models of Type Theory

Proof of Theorem 153.11 — The setoid model

Proof. Setoids and extensional maps form a category: identities and composites are extensional, and the equations hold because equality of extensional maps is pointwise. A one-element setoid is terminal. Reindexing is strictly functorial by proposition 153.10. For comprehension, $p_{F}$ is extensional because $\sim$ on $Σ (A, F)$ implies $x =_{A} u$ , and $q_{F}$ is a global element of $F [p_{F}]$ because $\sim$ supplies exactly the required transport equation. Given $h : B \to A$ and $b \in Tm (B, F [h])$ , put $⟨ h, b ⟩ (z) : = (h (z), b (z))$ ; it is extensional since $z =_{B} z^{'}$ gives ${ext}_{h}$ a proof $p : h (z) =_{A} h (z^{'})$ and the global-element condition on $b$ gives $F (p) (b (z)) = b (z^{'})$ , which is $\sim$ . The two comprehension equations hold on the nose, and uniqueness holds because an element of $Σ (A, F)$ is a pair whose components are recovered by $p_{F}$ and $q_{F}$ . ◻

The type formers, and what becomes of equality

Proposition 153.12 — Π - and Σ -structure ¶

The operations of definition 153.8 give $Std$ the $Π$ - and $Σ$ -structure of definition 54.21, definition 54.22, with $λ$ , application, pairing and projections defined on carriers as usual and extensionality proofs supplied by the displayed conditions.

Referenced from 4 locations

Setoid and PER Models of Type Theory

Proof of Proposition 153.12 — Π - and Σ -structure

Proof. Abstraction: from $b \in Tm (A . F, G)$ define $λ (b) (x)$ to be the function $y \mapsto b (x, y)$ together with the proof that it satisfies $E$ , which is the global-element condition of $b$ restricted to arrows of the form $(r_{x}, q)$ . That $λ (b)$ is itself a global element is the same condition at arrows $(p, q)$ with $p$ arbitrary. Application is evaluation, and the $β$ -equation holds because both sides are the same underlying element. The $η$ -equation holds because equality of $Π$ is pointwise, so a function is equal to its expansion without any further argument. $Σ$ : pairing is pairing, and the surjective-pairing equation holds because $\sim$ on $Σ (A, F)$ is implied by componentwise equality, taking $p = r_{x}$ . Stability under reindexing is proposition 153.10 together with the observation that all four operations are defined without mentioning the index setoid. ◻

Proposition 153.13 — Natural numbers and sums ¶

Let $N_{s} : = (N, Id)$ and, for setoids $A, B$ , let $A + B$ have carrier $| A | + | B |$ and equality relating $inl$ to $inl$ by $=_{A}$ , $inr$ to $inr$ by $=_{B}$ , and no left injection to a right injection. These carry the introduction, elimination and computation structure of chapter 28 in $Std$ .

Referenced from 4 locations

Setoid and PER Models of Type Theory

Proof of Proposition 153.13 — Natural numbers and sums

Proof. For $N_{s}$ the recursor is the metatheoretic recursor; it is extensional because the equality is the identity type, and its two computation rules are the metatheoretic ones. For $A + B$ the case operator is defined by the metatheoretic case; extensionality is checked on the three shapes of the equality relation, and the impossible shape gives the vacuous case. Stability holds because both constructions are pointwise in the index. ◻

Proposition 153.14 — The equality type is the carried equality ¶

For $F \in Ty (A)$ and $a, b \in Tm (A, F)$ define ${Eq}_{F} (a, b) \in Ty (A)$ to have carrier the type $a (x) =_{F (x)} b (x)$ at $x$ , with equality the total relation. Then $Eq$ is a family, it is inhabited exactly when $a = b$ in $Tm (A, F)$ , and $Std$ validates both equality reflection and uniqueness of identity proofs.

Referenced from 7 locations

Setoid and PER Models of Type Theory

Proof of Proposition 153.14 — The equality type is the carried equality

Proof. Familyhood: transport along $p : x =_{A} y$ is the map induced by $F (p)$ together with the global-element conditions of $a$ and $b$ ; proof irrelevance holds because the target equality is total, which also makes clauses (2) and (3) automatic. Inhabitation: a global element of ${Eq}_{F} (a, b)$ is exactly a pointwise proof of $a (x) =_{F (x)} b (x)$ , which is the definition of $a = b$ in $Tm (A, F)$ ; that is equality reflection. Uniqueness: the equality of ${Eq}_{F} (a, b)$ is total, so any two of its elements are equal. ◻

Remark 153.15 — The price of prop:setoid-eq ¶

Both principles that chapter 55 could not refute are here validated, and validated by construction rather than by accident: the identity type is not a new former but a projection of the data every type already carries. Two consequences follow at once. The model cannot separate $J$ from $K$ , so it settles nothing that chapter 152 settled. And the theory it models is extensional, so a type-checking algorithm for it cannot decide the judgments by comparing normal forms alone; deciding $Γ ⊢ A \equiv B type$ would require deciding inhabitation of arbitrary equality types.

Referenced from 3 locations

Setoid and PER Models of Type Theory

Definition 153.16 — Bracket types ¶

For a setoid $A$ let $Br (A)$ have carrier $| A |$ and equality the total relation. Introduction is the identity on carriers, and the eliminator sends $k : Br (A)$ , a family $G$ over the ambient context, and a global element $b$ of $G$ over $A .$ that provably does not depend on its $A$ -argument, to the common value of $b$ .

Referenced from 4 locations

Setoid and PER Models of Type Theory

Proposition 153.17 — Bracket structure ¶

$Br (A)$ is a setoid; it is inhabited exactly when $A$ is; any two of its elements are equal; and the eliminator of definition 153.16 is well defined and satisfies its computation rule.

Referenced from 4 locations

Setoid and PER Models of Type Theory

Proof of Proposition 153.17 — Bracket structure

Proof. The total relation is an equivalence relation, and the carrier is unchanged, so the first two claims are immediate. For the eliminator, the hypothesis on $b$ says exactly that $b (x) = b (y)$ for all $x, y : | A |$ ; hence the value $b (k)$ does not depend on which element of $| A |$ the element $k$ is, and the assignment is extensional because the equality of $Br (A)$ is total. The computation rule at $k = br (a)$ returns $b (a)$ by definition. ◻

Example 153.18 — A quotient and a transport, computed ¶

Take $A : = Z$ of example 153.4(3) and let $F \in Ty (A)$ be the family with $F (m, n) : = Br (Fin (m + n + 1))$ , the bracket of a finite type whose size depends on the representative. For $p : (m, n) \sim (m^{'}, n^{'})$ the transport $F (p)$ must be an extensional map $Br (Fin (m + n + 1)) \to Br (Fin (m^{'} + n^{'} + 1))$ ; since both equalities are total, the map sending everything to a fixed element is extensional, and proof irrelevance holds because any two maps into a setoid with the total equality are equal. So $F$ is a family even though the carrier sizes differ.

By contrast the assignment $G (m, n) : = Fin (m + n + 1)$ with its identity equality is not a family: a transport along the proof $(0, 0) \sim (1, 1)$ would be a map $Fin (1) \to Fin (3)$ , and composing it with a transport back along the symmetric proof must give the identity by lemma 153.7, which is impossible since the carriers have different cardinality. The obstruction that opened this chapter is thus visible inside the model: a family must respect the equality, and the model refuses the assignments that do not.

Finally, negation on $Z$ is the extensional map $ν (m, n) : = (n, m)$ of example 153.4(3), and $ν \circ ν = {id}_{Z}$ holds in $Std$ because equality of extensional maps is pointwise and $(m, n) \sim (m, n)$ . In the set model the corresponding statement would be an equation between representatives.

Referenced from 4 locations

Setoid and PER Models of Type Theory

Exercise 153.1 ¶

★★☆ Continue example 153.18. Give a family $H$ over $Z$ whose fibres are not all isomorphic to a bracket, and prove it is a family by exhibiting the transports and checking the three clauses of definition 153.6. Then show that your $H$ has a global element if and only if a certain statement about representatives holds.

Referenced from 2 locations

Setoid and PER Models of Type Theory

Exercise 153.2 ¶

★☆☆ Prove that $Std$ validates function extensionality directly from definition 153.2, and identify the exact clause of the definition that does the work.

Referenced from 2 locations

Setoid and PER Models of Type Theory

The setoid universe from iterative sets

A universe of setoids cannot be the collection of all setoids at a fixed level: that collection has a carrier one level up, so it is a classoid, and a type of the object theory must be a setoid. The construction that resolves this builds a single carrier of codes whose decoding is a setoid.

Definition 153.19 — Iterative sets ¶

Let $U_{0}$ be the first metatheoretic universe with decoding $T_{0}$ . Define $| V | : = W_{X : U_{0}} T_{0} (X)$ , the type of well-founded trees whose branching types are codes of $U_{0}$ , with constructor $\sup (X, f)$ for $X : U_{0}$ and $f : T_{0} (X) \to | V |$ . Write $# \sup (X, f) : = X$ and $\sup (X, f) ▹ a : = f (a)$ . Define $=_{V}$ by the mutual recursion $α =_{V} β : = (\prod_{a : # α} \sum_{b : # β} α ▹ a =_{V} β ▹ b) \times (\prod_{b : # β} \sum_{a : # α} α ▹ a =_{V} β ▹ b),$ and membership by $γ \in_{V} α : = \sum_{a : # α} γ =_{V} α ▹ a$ . Then $V : = (| V |, =_{V})$ is a $0$ -classoid.

Referenced from 5 locations

Setoid and PER Models of Type Theory

Lemma 153.20 — =_V is an equivalence relation valued in _0 ¶

The relation of definition 153.19 is reflexive, symmetric and transitive, and $α =_{V} β$ is an element of $U_{0}$ for all $α, β$ .

Referenced from 2 locations

Setoid and PER Models of Type Theory

Proof of Lemma 153.20 — =_V is an equivalence relation valued in _0

Proof. Reflexivity is proved by $W$ -induction: given the statement for every $α ▹ a$ , take $b : = a$ in both components. Symmetry exchanges the two components. Transitivity composes the two witnesses, again by $W$ -induction on the first argument. For the level: the two components are $Π$ - and $Σ$ -types over $# α, # β : U_{0}$ with recursive occurrences at $U_{0}$ , so the whole relation stays in $U_{0}$ ; this is the reason $V$ is a classoid and not a $1$ -setoid. ◻

Definition 153.21 — Decoding a code to a setoid ¶

For $α : | V |$ let $κ (α)$ be the setoid with carrier $# α$ and equality $a \approx a^{'}$ iff $α ▹ a =_{V} α ▹ a^{'}$ . For $p : α =_{V} β$ let $κ (p) : κ (α) \to κ (β)$ send $a$ to the $b$ named by the first component of $p$ .

Referenced from 2 locations

Setoid and PER Models of Type Theory

Proposition 153.22 — κ is a family over V ¶

$κ$ satisfies the three clauses of definition 153.6: each $κ (p)$ is extensional, transports along two proofs of the same equation agree, and identity and composition are respected.

Referenced from 2 locations

Setoid and PER Models of Type Theory

Proof of Proposition 153.22 — κ is a family over V

Proof. Extensionality: if $α ▹ a =_{V} α ▹ a^{'}$ then the first component of $p$ produces $b, b^{'}$ with $α ▹ a =_{V} β ▹ b$ and $α ▹ a^{'} =_{V} β ▹ b^{'}$ , and transitivity and symmetry of $=_{V}$ give $β ▹ b =_{V} β ▹ b^{'}$ , which is $b \approx b^{'}$ . Proof irrelevance: two proofs $p, q$ give $b$ and $b^{'}$ with $β ▹ b =_{V} α ▹ a =_{V} β ▹ b^{'}$ , hence $b \approx b^{'}$ ; equality of extensional maps is pointwise, so $κ (p) = κ (q)$ . Identity and composition follow from the same computation applied to the chosen reflexivity and transitivity proofs, using proof irrelevance to discard the particular witnesses. ◻

Theorem 153.23 — The universe of small setoids ¶

Interpret $U$ by $V$ and $El (-)$ by $κ$ . Then $U \in Ty (A)$ for every context $A$ by constant reindexing, $El (-)$ is strictly stable, and $V$ is closed under the operations of proposition 153.12, proposition 153.13, proposition 153.14, proposition 153.17; in particular there are codes $\hat{Π}$ , $\hat{Σ}$ , $\hat{Eq}$ , $\hat{Br}$ and $\hat{N}$ with $κ (\hat{Π} (α, β))$ isomorphic to $Π (κ (α), κ \circ β)$ , and similarly for the others.

Referenced from 8 locations

Setoid and PER Models of Type Theory

Proof of Theorem 153.23 — The universe of small setoids

Proof. Constancy and stability are as in proposition 151.16. For closure, each code is built by one application of $\sup$ whose branching type is the metatheoretic $Π$ - or $Σ$ -type of the branching types of the arguments, which is again in $U_{0}$ because $U_{0}$ is closed under those formers. The bracket code is $\hat{Br} (α) : = \sup (# α, λ x . \sup (0,!))$ , the “squashed” tree: it has an element exactly when $α$ does, and all its elements are $=_{V}$ -equal because they are all the empty tree. Decoding these codes gives setoids isomorphic to the corresponding constructions, and the isomorphisms are the evident renamings of branches. ◻

Remark 153.24 — Isomorphic, not equal ¶

Theorem 153.23 asserts isomorphism of setoids, not equality of families. For the interpretation of a Russell-style universe this suffices only because the object theory’s universe rules are stated up to the carried equality; a Tarski presentation with strict decoding equations would require choosing the codes so that decoding is literally the operation, which the $\sup$ -based codes above do not achieve.

Referenced from 4 locations

Setoid and PER Models of Type Theory

Theorem 153.25 — Soundness for the listed rules ¶

Let $T_{Std}$ be the theory whose rules are: the structural and substitution rules of definition 54.2; the $Π$ -, $Σ$ -, $N$ -, sum-, equality- and bracket-rules verified in proposition 153.12, proposition 153.13, proposition 153.14, proposition 153.17; equality reflection and uniqueness of identity proofs; and the universe rules of theorem 153.23. Then every derivable judgment of $T_{Std}$ holds in $Std$ under the interpretation sending contexts to setoids, types to families, terms to global elements, and each of the four equality judgments to the corresponding equality of the interpreting data.

Referenced from 5 locations

Setoid and PER Models of Type Theory

Proof of Theorem 153.25 — Soundness for the listed rules

Proof. $Std$ is a CwF by theorem 153.11 and supports each listed former by the propositions named in the statement, with all substitution laws strict by proposition 153.10. Interpretation of derivations is then the induction of theorem 54.28, whose only requirements are those two facts. The two extensional rules are proposition 153.14, and the universe rules are theorem 153.23 read through remark 153.24. ◻

Remark 153.26 — Reconstruction against the mechanized development ¶

Palmgren’s model [Pal22] is accompanied by an Agda development in which each rule above appears as a checked constant. The correspondence to check by hand is exact for one rule at a time; the $Π$ -elimination rule, for instance, appears with the context, the two families, the function term, its typing proof, the argument and its typing proof as explicit and implicit arguments, and its conclusion is the typing of the application at the substituted family. Two cautions belong with any such replay. The dated snapshot of the development was written for an older Agda release, so a modern typecheck is a compatibility question and not a mathematical one; and the development checks the listed closure rules in an intensional metatheory, which is not a conservativity theorem for extensional type theory.

Referenced from 2 locations

Setoid and PER Models of Type Theory

Partial equivalence relations

The setoid model carries an equality alongside a type. A second model carries an equality alongside a computation: the carrier is fixed once and for all, and a type is a relation on it that is symmetric and transitive but need not be reflexive. The elements of the type are then exactly the computations related to themselves.

Definition 153.27 — Applicative structure and PERs ¶

Let $(Λ, \cdot)$ be a set with a partial binary operation $\cdot$ and distinguished elements $k, s$ satisfying $k \cdot a \cdot b = a$ and $s \cdot a \cdot b \cdot c = (a \cdot c) \cdot (b \cdot c)$ whenever the right-hand sides are defined. A partial equivalence relation (PER) on $Λ$ is a relation $R$ that is symmetric and transitive. Its domain is $| R | : = {a ∣ a R a}$ , and $R$ restricted to $| R |$ is an equivalence relation.

Referenced from 4 locations

Definition 153.28 — The category of PERs ¶

$PER$ has as objects the PERs on $Λ$ , and as arrows $R \to S$ the equivalence classes of elements $e \in Λ$ such that $a R b ⟹ e \cdot a and e \cdot b are defined and e \cdot a S e \cdot b,$ two such $e, e^{'}$ being identified when $e \cdot a S e^{'} \cdot a$ for all $a \in | R |$ . Composition is application of the combinator $s (k e^{'}) (\dots)$ realizing the composite, with identity realized by $i : = s k k$ .

Referenced from 4 locations

Setoid and PER Models of Type Theory

Lemma 153.29 — PER is a category with finite products ¶

Composition is well defined on equivalence classes, associative and unital, and $R \times S$ defined by pairing combinators is a product.

Referenced from 3 locations

Setoid and PER Models of Type Theory

Proof of Lemma 153.29 — PER is a category with finite products

Proof. Well-definedness: if $e$ and $e^{'}$ are identified and $f, f^{'}$ likewise, then for $a \in | R |$ the elements $f \cdot (e \cdot a)$ and $f^{'} \cdot (e^{'} \cdot a)$ are related in the target, using that $f$ maps related arguments to related results and that $e \cdot a$ and $e^{'} \cdot a$ are related. Associativity and unit laws hold because both sides are realized by combinators computing the same function on $| R |$ , and arrows are compared extensionally. Products use the standard pairing $⟨ a, b ⟩ : = λ z . z a b$ with projections; the required equations again hold extensionally on the domain. ◻

Definition 153.30 — Families of PERs and their formers ¶

A family over a PER $R$ is an assignment $S$ of a PER $S (a)$ to each $a \in | R |$ such that $a R b$ implies $S (a) = S (b)$ as relations. Put $\begin{aligned} e Π (R, S) e^{'} & iff (\forall a, b) a R b \Rightarrow e \cdot a S (a) e^{'} \cdot b, \\ ⟨ a, x ⟩ Σ (R, S) ⟨ b, y ⟩ & iff a R b and x S (a) y . \end{aligned}$

Referenced from 5 locations

Setoid and PER Models of Type Theory

Proposition 153.31 — The PER model ¶

Let $Per$ have contexts the PERs, substitutions the arrows of definition 153.28, $Ty (R)$ the families of definition 153.30, $Tm (R, S)$ the equivalence classes of realizers $e$ with $a R b \Rightarrow e \cdot a S (a) e \cdot b$ , comprehension $Σ$ , and reindexing by composition. Then $Per$ is a CwF with $Π$ - and $Σ$ -structure, and its interpretation of the equality type by ${Eq}_{S} (u, v) (a) : = {(x, y) ∣ u \cdot a S (a) v \cdot a}$ validates equality reflection and uniqueness of identity proofs.

Referenced from 4 locations

Proof of Proposition 153.31 — The PER model

Proof. The category laws are lemma 153.29. Reindexing is composition of realizers, strictly functorial because composition of the underlying partial functions is. Comprehension: given $h : Q \to R$ and $b \in Tm (Q, S [h])$ the pairing combinator realizes $⟨ h, b ⟩$ , and the two equations hold because the projections invert pairing on the domain; uniqueness holds extensionally. $Π$ : abstraction is realized by the combinator that curries, and the $β$ - and $η$ -equations hold extensionally on domains, which is the equality of arrows. Equality: the displayed relation is either empty or the total relation on a one-point set, so it is a PER; it is inhabited exactly when the two terms are equal as arrows, which is reflection, and it has at most one element up to the relation, which is uniqueness. ◻

Theorem 153.32 — The shared fragment ¶

Let $Λ$ be as in definition 153.27 and regard $Λ$ as a type of the metatheory of section 153.1. The assignment $Φ (R) : = (| R |, R)$ sending a PER to the setoid on its domain is a functor $PER \to Std$ that preserves finite products, the operations $Π$ and $Σ$ of definition 153.30, definition 153.8 up to isomorphism of setoids, and the equality type of proposition 153.14, proposition 153.31 on the nose. It does not preserve the universe of theorem 153.23, and it is not full.

Referenced from 5 locations

Setoid and PER Models of Type Theory

Proof of Theorem 153.32 — The shared fragment

Proof. Functoriality: an arrow $R \to S$ is a class of realizers, and applying a realizer is an extensional map $Φ (R) \to Φ (S)$ because related arguments give related results; two identified realizers give pointwise equal maps, hence equal extensional maps. Identity and composition are preserved because they are realized by combinators computing the identity and the composite. Products: $Φ (R \times S)$ and $Φ (R) \times Φ (S)$ have the same carrier up to the pairing bijection and the same equality. $Π$ : an element of $| Π (R, S) |$ is a realizer taking related arguments to related results, which is exactly an element of $| Π (Φ R, Φ \circ S) |$ carrying its extensionality proof, and the two equalities are both “pointwise related”; the comparison is a bijection, not an identity, because the setoid version pairs a function with a proof. $Σ$ likewise. Equality: both models interpret it by the carried relation, and the two relations are literally the same.

Failure of fullness: an extensional map $Φ (R) \to Φ (S)$ need not be realized by any element of $Λ$ . Take $Λ$ the untyped $λ$ -terms modulo convertibility, $R$ the PER relating exactly the numerals to themselves and $S$ the PER on ${true, false}$ ; the setoid map deciding a non-computable predicate of numerals is extensional but has no realizer. Failure for the universe: $Φ$ has no action on codes, because $V$ of definition 153.19 is built from $U_{0}$ and has no counterpart among PERs on a fixed $Λ$ ; a universe of PERs must be constructed separately and is not the image of this functor. ◻

Remark 153.33 — What the comparison is not ¶

Theorem 153.32 compares the two models only at the operations both sources define. It is not an equivalence of models, not a statement about universes, and not a conservativity result relating extensional and intensional type theory. In particular the PER model has a decidability profile of its own: its equality of arrows quantifies over the domain of a PER, so it is in general undecidable, and its inhabitation problems are recursion-theoretic rather than proof-theoretic.

Referenced from 2 locations

Setoid and PER Models of Type Theory

Boundary and seminar

Five boundaries govern everything above. Proof irrelevance is a hypothesis of definition 153.6, and proposition 153.10 shows it is used: without it the substitution laws hold only up to isomorphism. Reflection is validated (proposition 153.14), so the modelled theory is extensional and the model settles no question about intensional identity; in particular remark 153.15 records that it cannot separate $J$ from $K$ , which chapter 152 does. Decidability is lost with reflection: conversion in $T_{Std}$ is not decided by comparing normal forms, and no claim to the contrary follows from theorem 153.25. Universes are interpreted only up to isomorphism of setoids (remark 153.24), so a Tarski presentation with strict decoding is not modelled here. Large elimination is available only through the codes of theorem 153.23: an elimination of $V$ into the classoid of all setoids leaves the object theory, and nothing above licenses it.

The sources divide cleanly. The dependent setoid model, its universe from iterative sets, the listed closure rules and the accompanying mechanization are Palmgren’s [Pal22]; the intensional construction with a proof-irrelevant universe of propositions and its treatment of large eliminations is Altenkirch’s; the surrounding extensional-model development and the careful statement of what conservativity does and does not give is Hofmann’s [Hof95]. The realizability side is standard: the fibrational reading of definition 153.30 follows [Jac99] and the categorical background for theorem 153.32 is [AL91]. Lecture-note treatments of the passage between type theory and setoids are collected in [Pal14, Pal98].

[4]

Suggested first pass.

Begin with exercise 153.3, then exercise 153.4, and finish with exercise 153.7.

Exercise 153.3 ¶

★★☆ Let $A$ be a setoid and $\approx$ an extensional equivalence relation on it, that is a family over $A \times A$ with total fibre equalities satisfying the three laws. Define the quotient setoid $A / \approx$ and prove that it satisfies the expected universal property in $Std$ : extensional maps out of $A / \approx$ correspond to extensional maps out of $A$ that respect $\approx$ . Then show that the bracket type of definition 153.16 is the special case where $\approx$ is total.

Referenced from 3 locations

Setoid and PER Models of Type Theory

Exercise 153.4 ¶

★★★ Theorem 153.32 shows $Φ$ is not full. Show that it is also not faithful in general by exhibiting a PER $R$ and two arrows $R \to S$ that are distinct in $PER$ but equal after applying $Φ$ , or prove that no such pair exists and identify the clause of definition 153.28 responsible.

Referenced from 3 locations

Setoid and PER Models of Type Theory

Exercise 153.5 ¶

★★☆ Using definition 153.3, proposition 153.5, determine the level of $Σ (A, F)$ and of $Π (A, F)$ when $A$ is an $(m, n)$ -setoid and each $F (x)$ is an $(m^{'}, n^{'})$ -setoid. Then explain why $V$ of definition 153.19 must be a classoid and cannot be arranged to be a $0$ -setoid.

Referenced from 2 locations

Setoid and PER Models of Type Theory

Exercise 153.6 ¶

★★★ Exhibit a context $Γ$ and types $A, B$ of $T_{Std}$ such that $Γ ⊢ A \equiv B type$ holds in $Std$ if and only if a given equality type is inhabited, and conclude that any conversion algorithm for the theory of theorem 153.25 must decide inhabitation of that type. Say explicitly which of the five boundaries above your example exercises.

Referenced from 2 locations

Setoid and PER Models of Type Theory

Exercise 153.7 — Practical: a finite setoid model checker ¶

★★★ Practical project.setoid-family-checker Implement the finite fragment of $Std$ : a setoid is a finite carrier with a relation table, checked to be an equivalence relation; an extensional map is a function table, checked against definition 153.1; a family is a table assigning a setoid to each carrier element and a transport to each related pair, checked against the three clauses of definition 153.6; a global element is a choice per fibre, checked against definition 153.8. The invariant the program must maintain is that no table is accepted unless every clause it is checked against holds at every relevant tuple. The program must print, for each named input, the verdict on the input tables, the computed transport of a named element along a named proof, and the carrier and equality of a computed $Σ$ or $Π$ . The acceptance test is: the integer setoid of example 153.4(3), truncated to representatives with $m, n \leq 3$ , is accepted and $ν$ is accepted as extensional; the bracket family of example 153.18 is accepted; the assignment $G (m, n) = Fin (m + n + 1)$ of the same example is rejected, with the report naming the pair $(0, 0) \sim (1, 1)$ and the clause it violates; and the computed $Σ$ of the accepted family has the equality predicted by lemma 153.9 on the named tuples. Exhaustive table checking is evidence on these finite inputs only; it does not prove theorem 153.11 or theorem 153.25, and it says nothing about the universe of theorem 153.23, which is infinite.

Referenced from 3 locations