An intuitionistic set-theoretical model of fully dependent CC^ω

Aczel, P. 1998. On relating type theories and set theories. In Proceedings of Types, volume 1657 of Springer LNCS, pp. 1–18.

Aczel, P. and Rathjen, M. 2008. Notes on constructive set theory.

Arenas, F. G. 1999. Alexandroff spaces. Acta Math. Univ. Comenianae, 68(1):17–25.

Barendregt, H. 1991. Introduction to generalized type systems. Journal of Functional Programming, 1(2):125–154.

Barendregt, H. 1992. Handbook of Logic in Computer Science, volume 2, chapter 2: Lambda calculus with types. Oxford

University Press.

Barras, B. 2010. Sets in coq, coq in sets. Journal of Formalized Reasoning, 3(1):29–48.

Coquand, T. and Huet, G. 1988. The calculus of constructions. Information and computation, 76(2):95–120.

Dybjer, P. 2000. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic

Logic, 65(2):525–549.

Forster, Y. 2021. Church’s thesis and related axioms in Coq’s type theory. In 29th EACSL Annual Conference on Computer

Science Logic (CSL 2021), volume 183 of LIPIcs, pp. 21:1–21:19.

Geuvers, H. 2001. Induction is not derivable in second order dependent type theory. In Types for Proofs and Programs.

Girard, J.-Y. 1989. Proofs and types. Cambridge University Press.

Jacobs, B. 2001. Categorical Logic and Type Theory, volume 141 of Studies in Logic and the Foundations of Mathematics.

Elsevier.

24

M. Sato, J. Garrigue

Jim´enez, B. C. R. 1999. Condensing lemmas for pure type systems with universes. In Algebraic Methodology and Software

Technology, volume 1548 of Springer LNCS, pp. 422–437.

Lee, G. and Werner, B. 2011. Proof-irrelevant model of CC with predicative induction and judgemental equality. Logical

Methods in Computer Science, 7(4:5).

Luo, Z. 1991. A higher-order calculus and theory abstraction. Information and Computation, 90(1):107–137.

MacLane, S. and Moerdijk, I. 1992. Sheaves in geometry and logic: A first introduction to topos theory. Springer.

Miquel, A. and Werner, B. 2003. The not so simple proof-irrelevant model of CC. In Types for Proof and Programs, volume

2426 of Springer LNCS, pp. 240–258.

Reynolds, J. 1984. Polymorphism is not set-theoretic. In Semantics of Data Types, volume 173 of Springer LNCS, pp.

145–156.

Sato, M. and Garrigue, J. 2016. An intuitionistic set-theoretical model of CCω¯ . Journal of Information Processing,

24(4):711–720.

Stefanova, M. and Geuvers, H. 1995. A simple model construction for the calculus of constructions. In International

Workshop on Types for Proofs and Programs.

Streicher, T. 1991. Semantics of Type Theory: Correctness, Completeness and Independence Results. Birk¨auser.

Timany, A. and Sozeau, M. 2017. Consistency of the predicative calculus of cumulative inductive constructions (pCuIC).

coRR. arXiv preprint arXiv:1710.03912.

Univalent Foundations Program 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. http://

homotopytypetheory.org/book, Institute for Advanced Study.

van Dalen, D. 1984. Intuitionistic logic. In Handbook of Philosophical Logic, volume III, pp. 225–339. Springer.

van den Berg, B. 2007. Diaconescu’s theorem and the principle of propositional extensionality.

Werner, B. 1997. Sets in types, types in sets. In Theoretical aspects of computer software, volume 1281 of Springer LNCS,

pp. 530–546.

Werner, B. 2008. On the strength of proof-irrelevant type theories. Logical Methods in Computer Science, 4(3:13):1–20.

Appendix A. Proof of Weakening

Lemma 29. The proof is by induction on t, using Lemma 13.

• t = x (case of variable)

It is clear since t is not a proof term.

• t = λ x : A.t ′

By Lemma 10, t ′ is also not a proof term for Γ1 ; (x′ : A′ ); Γ2 ; (x : A). Therefore

[ Γ1 ; Γ2 ⊢ λ x : A.t ′ ] (γ1 , γ2 )

= {(α, [ Γ1 ; Γ2 ; (x : A) ⊢ t ′ ] (γ1 , γ2 , α) |

α ∈ [ Γ1 ; Γ2 ⊢ A]](γ1 , γ2 )}

= {(α, [ Γ1 ; (x′ : A′ ); Γ2 ; (x : A) ⊢ t ′ ] (γ1 , α ′ , γ2 , α) |

α ∈ [ Γ1 ; (x′ : A′ ); Γ2 ⊢ A]](γ1 , α ′ , γ2 )}

= [ Γ1 ; (x′ : A′ ); Γ2 ⊢ λ x : A.t ′ ] (γ1 , α ′ , γ2 )

holds.

• t = t1 t2

By Lemma 10, t1 is also not a proof term for Γ1 ; (x′ : A′ ); Γ2 . If t2 is a proof term for Γ1 ; (x′ :

A′ ); Γ2 , then

[ Γ1 ; Γ2 ⊢ t1 t2 ] (γ1 , γ2 )

= [ Γ1 ; Γ2 ⊢ t1 ] (γ1 , γ2 ) (⊥X )

= [ Γ1 ; (x′ : A′ ); Γ2 ⊢ t1 ] (γ1 , α ′ , γ2 ) (⊥X )

= [ Γ1 ; (x′ : A′ ); Γ2 ⊢ t1 t2 ] (γ1 , α ′ , γ2 )

holds. If t2 is not a proof term, then it is proved similarly.

An Intuitionistic Set-theoretical Model of Fully Dependent CCω

25

• t = ∀x : A.B

By Lemma 15

PTΓ1 ;Γ2 ,x (A, B) = PTΓ1 ;(x′ :A′ );Γ2 ,x (A, B)

holds. Hence we can only prove in the case of PTΓ1 :Γ2 ,x (A, B).

• t = Prop or Typei

Clear.

Appendix B. Proof of Substitution

Lemma 30. We define the predicates P(∆) and Q(∆, t) as follows.

P(∆) ≡ ∀δ , (γ, [ Γ ⊢ u]](γ), δ ) ∈ [ Γ; (x : u); ∆)]]

⇒ (γ, δ ) ∈ [ Γ; ∆[x\u]]],

Q(∆, t) ≡ ∀δ , [ Γ; (x : U); ∆ ⊢ t]](γ, [ Γ ⊢ u]](γ), δ ) is well defined

[ Γ; ∆[x\u] ⊢ t[x\u]]](γ, δ ) is well-defined

and [ Γ; x : U; ∆ ⊢ t]](γ, [ Γ ⊢ u]](γ), δ )

= [ Γ; ∆[x\u] ⊢ t[x\u]]](γ, δ ) .

We prove this lemma in three steps (i)P([]), (ii)P(∆) ⇒ ∀t, Q(∆, t), (iii)(∀t, Q(∆, t)) ⇒

∀T, P(∆; y : T ).

(i) P([])

Clear

(ii) P(∆) ⇒ ∀t, Q(∆, t)

If t is a proof term for Γ; (x : U); ∆, then t[x\u] is also a proof term for Γ; ∆[x\u] by

Lemma 12. Therefore

[ Γ; (x : U); ∆ ⊢ t]](γ, [ Γ ⊢ u]](γ), δ ) = ⌊γ, [ Γ ⊢ u]](γ), δ ⌋

[ Γ; ∆ ⊢ t[x\u]]](γ, δ ) = ⌊γ, δ ⌋

hold. Hence we must prove that

⌊γ, [ Γ ⊢ u]](γ), δ ⌋ = ⌊γ, δ ⌋.

If u is not a proof term for Γ, it is clear. If u is a proof term then [ Γ ⊢ u]](γ) = ⌊γ⌋ holds,

therefore it also hold.

Next, if t is not a proof term for Γ; (x : U); ∆, then t[x\u] is also not a proof term for Γ; ∆[x\u]

by Lemma 12. We prove by induction on the term t.

– t = Prop or Typei

It is clear.

– t = ∀a : A.B

We assume that

[ Γ; (x : U); ∆ ⊢ ∀a : A.B]](γ, [ Γ ⊢ u]](γ), δ )

is well defined, therefore

[ Γ; (x : U); ∆ ⊢ A]](γ, [ Γ ⊢ u]](γ), δ ),

[ Γ; (x : U); ∆; (a : A) ⊢ B]](γ, [ Γ ⊢ u]](γ), δ , α)

26

M. Sato, J. Garrigue

are also well defined. By induction hypothesis, Q(∆, A) and Q(∆; (a : A), B) are assumed.

By Lemma 15, the value of PT is invariant. Hence the statement holds in this case.

– t = λ a : A.t

We assume that

[ Γ; (x : U); ∆ ⊢ λ a : A.t]](γ, [ Γ ⊢ u]](γ), δ )

is well defined, therefore

[ Γ; (x : U); ∆; (a : A) ⊢ t]](γ, [ Γ ⊢ t]](γ), δ , α)

[ Γ; (x : U); ∆ ⊢ A]](γ, [ Γ ⊢ u]](γ), δ )

are also well defined. By induction hypothesis, Q(∆; (a : A), t) and Q(∆, A) are assumed.

Hence the statement holds in this case.

– t =ab

We assume that

[ Γ; (x : U); ∆ ⊢ a b]](γ, [ Γ ⊢ u]](γ), δ )

is well defined, therefore

[ Γ; (x : U); ∆ ⊢ a]](γ, [ Γ ⊢ u]](γ), δ )

is well defined and a function whose domain contains

[ Γ; (x : U); ∆ ⊢ b]](γ, [ Γ ⊢ u]](γ), δ ).

By induction hypothesis, Q(∆, a) and Q(∆, b) are assumed. By Lemma 12, if b is a (resp.

not) proof term for Γ; (x : U); ∆, then b[x\u] is also a (resp. not) proof term for Γ; ∆[x\u].

Hence the statement holds in this case.

– t = y (case of variable)

We prove in three cases as follows.

– The variable y occur in Γ.

In this case, we have

[ Γ; (x : U); ∆ ⊢ y]](γ, [ Γ ⊢ u]](γ), δ ) = γi ,

[ Γ; ∆[x\u] ⊢ y[x\u]]](γ, δ ) = γi .

for some i. Hence the statement holds in this case.

– The case y = x.

We have

[ Γ; (x : U); ∆ ⊢ x]](γ, [ Γ ⊢ u]](γ), δ ) = [ Γ ⊢ u]](γ),

[ Γ; ∆[x\u] ⊢ x[x\u]]](γ, δ ) = [ Γ; ∆[x\u] ⊢ u]](γ).

By Lemma 29, the statement holds in this case.

– The variable y occur in ∆.

In this case, we have

[ Γ; (x : U); ∆ ⊢ y]](γ, [ Γ ⊢ u]](γ), δ ) = δi

for some i. Since (γ, δ ) ∈ [ Γ; ∆[x\u]]] by hypothesis P(∆), hence following equation is

well defined.

[ Γ; ∆[x\u] ⊢ y]](γ, δ ) = δi

Hence the statement holds in this case.

(iii) (∀t, Q(∆, t)) ⇒ ∀T, P(∆; y : T )

We assume that

(γ, [ Γ ⊢ u]](γ), δ , ε) ∈ [ Γ; (x : U); ∆; (y : T )]].

An Intuitionistic Set-theoretical Model of Fully Dependent CCω

27

By definition of the interpretation of contexts, we have

(γ, [ Γ ⊢ u]](γ), δ ) ∈ [ Γ; (x : U); ∆]]

ε ∈ [ Γ; (x : U); ∆ ⊢ T ] (γ, [ Γ ⊢ u]](γ), δ )

Since Q(∆, T ) holds, hence following equations hold.

(γ, δ ) ∈ [ Γ; ∆[x\u]]],

ε ∈ [ Γ; ∆[x\u] ⊢ T [x\u]]](γ, δ ).

Therefore we have

(γ, δ , ε) ∈ [ Γ; ∆[x\u] ⊢ T [x\u]]](γ, δ ).

Appendix C. Proof of semantic proof irrelevance

Lemma 31. The proof is by induction on t.

• t = x (case of variable)

Since t is not a proof term for Γ; (x′ : A′ ); ∆, therefore we have t ̸= x′ , hence the statement

holds in this case.

• t = λ x : A.t ′

By Lemma 10, t is also not a proof term for Γ; (x′ : A′ ); ∆; (x : A). Therefore

[ Γ; (x′ : A′ ); ∆ ⊢ λ x : A.t ′ ] (γ, p1 , δ )

= {(α, [ Γ; (x′ : A′ ); ∆; (x : A) ⊢ t ′ ] (γ, p1 , δ , α)) |

α ∈ [ Γ; (x′ : A′ ); ∆ ⊢ A]](γ, p1 , δ )}

= {(α, [ Γ; (x′ : A′ ); ∆; (x : A) ⊢ t ′ ] (γ, p2 , δ , α)) |

α ∈ [ Γ; (x′ : A′ ); ∆ ⊢ A]](γ, p2 , δ )}

= [ Γ; (x′ : A′ ); ∆ ⊢ λ x : A.t ′ ] (γ, p2 , δ )

holds.

• t = t1 t2

By Lemma 10, t1 is also not a proof term for Γ; (x′ : A′ ); ∆. If t2 is a proof term for Γ; (x′ :

A′ ); ∆, then

[ Γ; (x′ : A′ ); ∆ ⊢ t1 t2 ] (γ, p1 , δ )

= [ Γ; (x′ : A′ ); ∆ ⊢ t1 ] (γ, p1 , δ )(⊥X )

= [ Γ; (x′ : A′ ); ∆ ⊢ t1 ] (γ, p2 , δ )(⊥X )

= [ Γ; (x′ : A′ ); ∆ ⊢ t1 t2 ] (γ, p2 , δ )

holds. If t2 is not a proof term for Γ; (x′ : A′ ); ∆, then similarly.

• t = ∀x : A.B

Similarly.

Appendix D. Proof of Soundness

Theorem 33. The proof is by induction on the typing derivation.

28

M. Sato, J. Garrigue

(1) Case of Axiom

[ Prop] ∈ [ Typei ] is holds by the condition of (X, O(X)).

(2) Case of Weakening

It holds by Lemma 29.

(3) Case of Subsumption

It holds by (iv) of Lemma 25.

(4) Case of PI-Type

We will show the fact that

∀γ, α, [ Γ ⊢ A]](γ) ∈ [ Γ ⊢ s1 ] (γ)

[ Γ; (x : A) ⊢ B]](γ, α) ∈ [ Γ; (x : A) ⊢ s2 ] (γ, α)

(∀γ, [ Γ ⊢ ∀x : A.B]](γ) ∈ [ Γ ⊢ s3 ] (γ)).

There are four cases as follows.

– PTΓ,x (A, B) = TT

By definition of the interpretation of judgment, the following equation

[ Γ ⊢ ∀x : A.B]](γ) =

[ Γ; (x : A) ⊢ B]](γ, α)

α∈[[Γ⊢A]](γ)

holds. Since [ Γ ⊢ A]](γ) ∈ Ui , [ Γ; (x : A) ⊢ B]](γ, α) ∈ Ui for any γ, α and Lemma 25 (ii),

we have

[ Γ; (x : A) ⊢ B]](γ, α) ∈ Ui .

α∈[[Γ⊢A]](γ)

– PTΓ,x (A, B) = PT

By definition of the interpretation of judgment, the following equation

[ Γ ⊢ ∀x : A.B]](γ) =

f∈

Γ;

(x

A)

B]

(γ,

α)

is

constant

function

α∈[[Γ⊢A]](γ)

holds. Since [ Γ ⊢ A]](γ) ∈ Ui , [ Γ; (x : A) ⊢ B]](γ, α) ∈ Ui for any γ, α and Lemma 25 (ii),

the statement holds.

– PTΓ,x (A, B) = TP

It is clear since [ Γ ⊢ ∀x : A.B]](γ) is an open set by definition of the interpretation of

judgment.

– PTΓ,x (A, B) = PP

It is clear since [ Γ ⊢ ∀x : A.B]](γ) is an open set by definition of the interpretation of

judgment.

(5) Case of Abstraction

We will show the fact that

∀γ, α, [ Γ; (x : A) ⊢ t]](γ, α) ∈ [ Γ; (x : A) ⊢ B]](γ, α)

∀γ, [ Γ ⊢ λ x : A.t]](γ) ∈ [ Γ ⊢ ∀x : A.B]](γ) .

There are four cases as follows.

An Intuitionistic Set-theoretical Model of Fully Dependent CCω

29

– PTΓ,x (A, B) = TT

By definition of the interpretation, we have the following equations:

[ Γ ⊢ λ x : A.t]](γ) =

α, [ Γ; (x : A) ⊢ t]](γ, α) | α ∈ [ Γ ⊢ A]](γ) ,

[ Γ ⊢ ∀x : A.B]](γ) =

[ Γ; (x : A) ⊢ B]](γ, α).

α∈[[Γ⊢A]](γ)

Then, we must prove the following equation:

α, [ Γ; (x : A) ⊢ t]](γ, α) | α ∈ [ Γ ⊢ A]](γ)

[ Γ; (x : A) ⊢ B]](γ, α).

α∈[[Γ⊢A]](γ)

But it is clearb by induction hypothesis.

– PTΓ,x (A, B) = PT

It is similar the case of PTΓ,x (A, B) = TT. We must prove that

[ Γ ⊢ λ x : A.t]](γ) =

α, [ Γ; (x : A) ⊢ t]](γ, α) | α ∈ [ Γ ⊢ A]](γ)

is a constant function. Since A is a propositional term for Γ, this is a consequence of

Lemma 31.

– PTΓ,x (A, B) = TP

Since λ x : A.t is a proof term, we have following equations

[ Γ ⊢ λ x : A.t]](γ) = ⌊γ⌋.

Hence, the fact we must prove that

⌊γ⌋ ∈ [ Γ ⊢ ∀x : A.B]](γ).

By definition we have the following equation.

[ Γ ⊢ ∀x : A.B]](γ) =

{[[Γ; (x : A) ⊢ B]](γ, α) | α ∈ [ Γ ⊢ A]](γ)}.

If [ Γ ⊢ A]](γ) is the empty set, then the statement holds since [ Γ ⊢ ∀x : A.B]](γ) = X. We

assume that [ Γ ⊢ A]](γ) is a non-empty set. We have

∀α ∈ [ Γ ⊢ A]](γ), ⌊γ⌋ ∈ [ Γ; (x : A) ⊢ B]](γ, α)

by induction hypothesis and [ Γ; (x : A) ⊢ t]](γ, α) = ⌊γ, α⌋ = ⌊γ⌋. Therefore, we have the

following equation

{[[Γ; (x : A) ⊢ B]](γ, α) | α ∈ [ Γ ⊢ A]](γ)}.

⌊γ⌋ ∈

Hence the statement holds in this case.

– PTΓ,x (A, B) = PP

Since λ x : A.B is a proof term, we have the following equation

[ Γ ⊢ λ x : A.t]](γ) = ⌊γ⌋.

b If

[ Γ ⊢ A]](γ) is the empty set, then [ Γ ⊢ ∀x : A.B]](γ) = {∅} and [ Γ ⊢ λ x : A.t]](γ) = ∅ hold.

30

M. Sato, J. Garrigue

Hence, the fact we must prove that

⌊γ⌋ ∈ [ Γ ⊢ ∀x : A.B]](γ).

To prove it, we show that

↓ ⌊γ⌋ ⊂ [ Γ ⊢ ∀x : A.B]](γ).

This fact is equivalent to the following equation

↓ ⌊γ⌋ ∩ [ Γ ⊢ A]](γ) ⊂

[ Γ; (x : A) ⊢ B]](γ, α)

α∈[[Γ⊢A]](γ)

since definition of interpretation and Heyting Algebra. We assume ε ∈↓ ⌊γ⌋ ∩ [ Γ ⊢ A]](γ).

By Lemma 31, we have

[ Γ; (x : A) ⊢ B]](γ, α) = [ Γ; (x : A) ⊢ B]](γ, ε)

α∈[[Γ⊢A]](γ)

holds; since ε ∈ [ Γ ⊢ A]](γ) holds, right side of this equation is well defined. Here, we also

have

⌊γ, ε⌋ ∈ [ Γ; (x : A) ⊢ B]](γ, ε)

by induction hypothesis. Now, we prove that ⌊γ, ε⌋ = ε holds. Since ε ∈↓ ⌊γ⌋ holds,

therefore we have ε ≤ ⌊γ⌋. Hence we have ε = ⌊γ, ε⌋, and the statement holds in this

case.

(6) Case of Apply

We will show the fact that

∀γ, [ Γ ⊢ u]](γ) ∈ [ Γ ⊢ ∀x : A.B]](γ)

∧ [ Γ ⊢ v]](γ) ∈ [ Γ ⊢ A]](γ)

∀γ, [ Γ ⊢ u v]](γ) ∈ [ Γ ⊢ B[x\v]]](γ) .

There are four cases as follows.

– PTΓ,x (A, B) = TT

By definition of the interpretation of judgment and induction hypothesis, the following

equation

[ Γ ⊢ u v]](γ) = [ Γ ⊢ u]](γ) [ Γ ⊢ v]](γ)

[ Γ ⊢ u]](γ) ∈

[ Γ; (x : A) ⊢ B]](γ, α)

α∈[[Γ⊢A]](γ)

[ Γ ⊢ v]](γ) ∈ [ Γ ⊢ A]](γ)

hold. Therefore, we have

[ Γ ⊢ u v]](γ) ∈ [ Γ; (x : A) ⊢ B]](γ, [ Γ ⊢ v]](γ)).

By Lemma 30, we have

[ Γ; (x : A) ⊢ B]](γ, [ Γ ⊢ v]](γ)) = [ Γ ⊢ B[x\v]]](γ).

Hence, the statement holds in this case.

– PTΓ,x (A, B) = PT

By definition of the interpretation of judgment and indcution hypothesis, the following

An Intuitionistic Set-theoretical Model of Fully Dependent CCω

31

equation

[ Γ ⊢ u v]](γ) = [ Γ ⊢ u]](γ) ⊥X

[ Γ ⊢ u]](γ) ∈ f ∈

∏ [ Γ; (x : A) ⊢ B]](γ, α) |

α∈[[Γ⊢A]](γ)

f is a constant function

[ Γ ⊢ v]](γ) ∈ [ Γ ⊢ A]](γ)

hold. Therefore, we have

[ Γ ⊢ u v]](γ) ∈ [ Γ; (x : A) ⊢ B]](γ, ⊥X )

= [ Γ; (x : A) ⊢ B]](γ, [ Γ ⊢ v]](γ))

by Lemma 31. Moreover, the following equation

[ Γ; (x : A) ⊢ B]](γ, [ Γ ⊢ v]](γ)) = [ Γ ⊢ B[x\v]]](γ).

holds by Lemma 30 Hence, the statement holds in this case.

– PTΓ,x (A, B) = TP

It suffices to show that ⌊γ⌋ ∈ [ Γ ⊢ B[x\v]]](γ), since [ Γ ⊢ u]](γ) = [ Γ ⊢ u v]](γ) = ⌊γ⌋ holds.

By induction hypothesis, we have the following equation

{[[Γ; (x : A) ⊢ B]](γ, α) | α ∈ [ Γ ⊢ A]](γ)}.

⌊γ⌋ ∈

This equation implies the fact that

∀α ∈ [ Γ ⊢ A]](γ), ⌊γ⌋ ∈ [ Γ; (x : A) ⊢ B]](γ, α).

By Lemma 30 and the fact [ Γ ⊢ v]](γ) ∈ [ Γ ⊢ A]](γ), we have

⌊γ⌋ ∈ [ Γ ⊢ B[x\v]]](γ).

Hence, the statement holds in this case.

– PTΓ,x (A, B) = PP

By induction hypothesis, we have

⌊γ⌋ ∈ [ Γ ⊢ ∀x : A.B]](γ),

⌊γ⌋ ∈ [ Γ ⊢ A]](γ)

since [ Γ ⊢ u]](γ) = [ Γ ⊢ v]](γ) holds. The following equation holds.

[ Γ⊢A]](γ)

[ Γ ⊢ ∀x : A.B]](γ) =

[ Γ; (x : A) ⊢ B]](γ, α)

α∈[[Γ⊢A]](γ)

By (8) in Lemma 19, we have

[ Γ ⊢ ∀x : A.B]](γ) ∩ [ Γ ⊢ A]](γ)

[ Γ; (x : A) ⊢ B]](γ, α).

α∈[[Γ⊢A]](γ)

Then we also have

⌊γ⌋ ∈

[ Γ; (x : A) ⊢ B]](γ, α).

α∈[[Γ⊢A]](γ)

Hence

⌊γ⌋ ∈ [ Γ; (x : A) ⊢ B]](γ, [ Γ ⊢ v]](γ))

holds. By Lemma 30 and [ Γ ⊢ u v]](γ) = ⌊γ⌋, the statement holds in this case.

32

M. Sato, J. Garrigue

(7) Case of Variable

We show that

∀α ∈ [ Γ ⊢ A]](γ), [ Γ; (x : A) ⊢ x]](γ, α) ∈ [ Γ; (x : A) ⊢ A]](γ, α).

By Lemma 29, we must prove that

∀α ∈ [ Γ ⊢ A]](γ), [ Γ; (x : A) ⊢ x]](γ, α) ∈ [ Γ ⊢ A]](γ).

If A is not a propositional term for Γ, the statement holds since [ Γ; (x : A) ⊢ x]](γ, α) = α. If

A is a propositional term for Γ, then

[ Γ; (x : A) ⊢ x]](γ, α) = ⌊γ, α⌋

holds. Since ⌊γ, α⌋ ∈ ↓ α ⊂ [ Γ ⊢ A]](γ),

[ Γ; (x : A) ⊢ x]](γ, α) ∈ [ Γ ⊢ A]](γ)

holds. Hence the statement holds in this case.

(8) Case of Beta Equality

We must show that

∀γ, [ Γ ⊢ t]](γ) ∈ [ Γ ⊢ A]](γ), [ Γ ⊢ B]](γ) ∈ [ Γ ⊢ s]](γ)

∧ A =β B

⇒ ∀γ, [ Γ ⊢ t]](γ) ∈ [ Γ ⊢ B]](γ).

It is clear by Theorem 33 (1).

Appendix E. Proof of interpretation of logical symbols

Theorem 34.

(i)

(ii)

(iii)

(iv)

(v)

(vi)

(vii)

Use Lemma 8 and 29.

Use (2) in Lemma 19.

Use (1) and (3) in Lemma 19.

Use (1), (3) and (4) in Lemma 19.

Use (i) in Theorem 34 and (1), (2), (3) and (6) in Lemma 19.

Use (i) in Theorem 34 and (3) and (5) in Lemma 19.

What we prove is the followingc .

[ Γ ⊢ x]](γ) = [ Γ ⊢ y]](γ)

[ Γ ⊢ x =A y]](γ) =

∅ [ Γ ⊢ x]](γ) ̸= [ Γ ⊢ y]](γ)

By using (i) in Theorem 34, we have

{π([[Γ ⊢ y]](γ))π([[Γ⊢x]](γ)) | π ∈ [ Γ ⊢ A → Prop] (γ)}.

[ Γ ⊢ x =A y]](γ) =

If [ Γ ⊢ x]](γ) ̸= [ Γ ⊢ y]](γ), we can choose π as the followings

π([[Γ ⊢ x]](γ)) ̸= ∅

π([[Γ ⊢ y]](γ)) = ∅

hold. By (9) in Lemma 19, we have [ Γ ⊢ x =A y]](γ) = ∅. Hence the statement holds in this

case.

c The

remaining propositions yield by contrapositions of this fact.

An Intuitionistic Set-theoretical Model of Fully Dependent CCω

33

Next, we assume [ Γ ⊢ x]](γ) = [ Γ ⊢ y]](γ). In this case,

π([[Γ ⊢ y]](γ))π([[Γ⊢x]](γ)) = X

(viii)

holds for any π by (7) in Lemma 19. Hence the statement also holds in this case.

a. The following equation

[ Γ ⊢ A ↔ B]](γ) = [ Γ ⊢ B]](γ)[ Γ⊢A]](γ) ⊓ [ Γ ⊢ A]](γ)[ Γ⊢B]](γ)

holds. If [ Γ ⊢ A]](γ) = [ Γ ⊢ B]](γ) holds, then

[ Γ ⊢ A ↔ B]](γ) = X

[ Γ ⊢ A =Prop B]](γ) = X

(by (vii) in Theorem 34)

holds. Hence the statement holds in this case. If [ Γ ⊢ A]](γ) ̸= [ Γ ⊢ B]](γ), then [ Γ ⊢

A =Prop B]](γ) = ∅ holds by. Hence, the statement also holds in this case.

b. Use (10) in Lemma 19 and (vii) in Theorem 34.

...