Questions tagged [type-theory]

For questions about type theory, including normalization, dependent types, identity types, inductive types, universe types, functional programming languages, proofs as programs in simply-typed lambda-calculi, Martin-Löf's intuitionistic type theory or related.Consider using one of the following tags: (lambda-calculus), (logic), (constructive-mathematics),(homotopy-type-theory) if related.

Filter by
Sorted by
Tagged with
2
votes
1answer
55 views

Type theory and constructivist mathematics with paraconsistent logic?

Type theory, together with the Curry-Howard correspondence is a formal system for stating formal proofs of intuitionistic logic, which is used in constructive mathematics. Intuitionistic logic differs ...
0
votes
2answers
48 views

Intuitionistic “atomic” proof of negation?

In the view of logic in terms of type theory (cf. the Curry-Howard correspondence), the type $\neg P$ is defined as $P\to False$, and a proof of $\neg P$ is therefore a function that takes a proof of $...
2
votes
0answers
47 views

Translating developments over different foundations

More and more often, different foundations of mathematics emerging. In some cases, they even rebuild classical theorems (e.g. number theory, Cartan geometry [1].. etc) on top of it. Some foundations ...
2
votes
2answers
60 views

How does the “proofs as programs” correspondence work for equality?

The equality relation $=$ can be represented as a type, just as any other propostion in the Curry-Howard correspondence. I understand the sense in which the basic logical symbols $\land,\lor,\to, \...
2
votes
1answer
78 views

Strongly constructive proofs: Proofs that don't make use of decidability?

I was thinking about counting argumens from the perspective of constructivist / intuitionistic logic: A typical counting argument might have the following pattern: Suppose we have a finite set $S$ ...
4
votes
1answer
76 views

Rigorous definition of a type

What is a type in type theory? I tried to find a rigorous definition without luck. And that makes me wonder.. maybe there isn't any rigorous definition? My aim is to see how homotopy type theory ...
3
votes
0answers
40 views

''Relax Type'' in Computational Logical Framework

I am reading a nlab article about Matt Oliveri's computational logical framework. It introduces new type constructors such as $\textsf{Relax}$. I tried to read the author's justification for the ...
4
votes
1answer
53 views

''$\Gamma\vdash A\ \textrm{true}$'' in Martin-Löf type theory

I have a basic question about the notation ''$\Gamma\vdash A\ \textrm{true}$'' in Martin-Löf type theory. In his 1984 book, Martin-Löf says that if we have $\Gamma\vdash a:A$ and we do not care about ...
2
votes
0answers
54 views

Dependent tensor product in the category of abelian groups

In the category of set (or more generally an arbitrary locally cartesian closed category), we can think of a dependent product $\prod_{I}X$ of a "type family'' $X\to I$ index over $I$. For ...
7
votes
2answers
476 views

What theory of logic or types considers the “category of propositions”?

Was wondering if there was a theory already out there that considers the "category $\text{Prop}$ of propositions". It is a preorder (at most one arrow between two propositions), in which $A ...
2
votes
1answer
65 views

What is an example of constructive vs. nonconstructive type theory?

I am trying to get some basic terminology down related to type theory, and am currently on understanding the difference between "constructive type theories" and "nonconstructive type ...
1
vote
1answer
69 views

Why is intuitionistic type theory without dependent types more powerful than Martin-Löf type theory?

In the preface of Introduction to higher order categorical logic, Lambek and Scott write (emphasis mine): [L]ogicians have made three attempts to formulate higher order logic, in increasing power: ...
0
votes
1answer
35 views

Curry-Howard correspondence in CIC/propositional logic?

I am trying to understand how the type theory of the COQ theorem prover (calculus of constructions or CIC) works. Wikipedia states that it can be considered an extension of the Curry-Howard ...
0
votes
1answer
57 views

Is it possible to add computational facilities to otherwise “mathematical” formal systems by adjoining identities to types?

The following thought has been on my mind for years. Think of $\mathbb{N}$ as the type of all well-formed expressions representing natural numbers. And think of $$\tilde{\mathbb{N}} := \frac{\mathbb{N}...
3
votes
0answers
65 views

Moving between expressions in the typed lambda calculus and sentences in higher order logic.

In 'An Introduction to Mathematical Logic through Type Theory', Andrews describes a way of translating sentences in higher order logic into lambda terms in his version of the typed lambda calculus (...
1
vote
0answers
22 views

Denoting an argument-dependent range (co-domain) of a function

I would like to define a function whose co-domain depends on its argument, i.e. $\forall x \in X\colon f(x) \in A[x]$ where $X$ is the domain of $f$ and $A[x]$ is the value of a set-valued function. A ...
3
votes
0answers
75 views

types which behave like sets

I'm reading the homotopy type theory book and this sentence is giving me trouble. "We can define a class of types which behave like sets. Homotopically, these can be thought of as spaces in which ...
1
vote
1answer
48 views

Simply typed type theory and computability.

Assume that atomic types of simply typed lambda calculus($\lambda\to$) are interpreted as sets. Does every (total) computable function can be written as term in such calculus? If no, please give ...
7
votes
1answer
136 views

Computational Type Theory For Topos Logic

My question is basically, what approaches have been made to make computer proof assistants which can handle the internal logic of a topos ? To explain: while learning topos theory I was struck by the ...
2
votes
2answers
82 views

λ-cube: Why are dependent types and dependent functions on the same axis?

The lambda cube seems to unify the concepts of dependent types (types that depend on terms) with dependent functions (functions whose return type depends on an argument) into a single axis. But what ...
4
votes
1answer
76 views

Proof-irrelevance of identity types

In constructive type theories, we make a distinction between extensional and intensional identity types. It's trivial that extensional identity types are proof-irrelevant as the inhabitant of an ...
3
votes
1answer
70 views

Do “time points” and “durations” have an algebraic structure?

The C++ programming language has two types that are used to represent time: time_point and duration. As the name suggests: <...
6
votes
0answers
70 views

Why are there two sets of rules for set equality in intensional intuitionistic type theory?

In Martin-Löf's "Intuitionistic Type Theory", we can judge two sets are "equal" if the following are true: $$ membership\ rules: \frac{a \in A}{a \in B} and \frac{a \in B}{a \in ...
3
votes
1answer
87 views

How to prove $\sqrt{2}$ is irrational in Type Theory?

Using Intuitionistic Type Theory, how would one go about proving $\sqrt{2}$ is irrational? I read that we can not use law of excluded middle. (So does this mean we cannot use proof by contradiction). ...
4
votes
1answer
73 views

Converse of Deduction Theorem in Type Theory

I have a question about the way to express the converse of the deduction theorem in type theory. In simple type theory, the deduction theorem can be easily expressed by the introduction rule for $\...
1
vote
1answer
40 views

Do types and Curry-Howard correspondence belong to some kind of semantics of programming languages?

Is it correct that types belong to semantics of programming languages? In what kind of semantics are types studied: operational, denotational, and/or axiomatic semantics? Does the Curry-Howard ...
1
vote
0answers
53 views

Path induction for homotopies between functions

Consider a version of HoTT where every type former specifies the "shape" of its identity type definitionally (e.g. an equality of pairs is a pair of equalities, equality of types is ...
3
votes
2answers
70 views

Missing (important?) substitution rule

I am reading The HoTT Book and I noticed that there is an extensive use of a very reasonable principle: if we have $b \equiv c : A$ then we can conclude $(a =_A b) \equiv (a =_A c) : \mathcal{U}$, for ...
6
votes
2answers
143 views

Propositional truncation $||$-$||$ and double negation $\neg\neg$

I have a basic question about propositional truncation $||$-$||$ and double negation $\neg\neg$. According to the recursion rule of $||$-$||$, $A\rightarrow B=||A||\rightarrow B$ as long as $B$ is a ...
2
votes
1answer
80 views

$\neg\neg$-Stability

I see that some authors say that there are sets, for example, $\mathbb{N}$ and $\mathsf{Bool}$, that are $\neg\neg$-stable (i.e., satisfying $\neg\neg X\rightarrow X$). I understand what it means when ...
2
votes
1answer
89 views

$\textsf{isStable}(A)\rightarrow\textsf{isProp}(A)$?

I meet both $\neg\neg$-stable and proof-irrelevant types in Harper's handouts on homotopy type theory. I know clearly that proof irrelevance does not imply stability, but does stability imply proof ...
0
votes
1answer
17 views

Universe of all Types

Suppose we have a universe of all types $U_{\infty}$ that includes itself. Can someone explain why it is unsound -- in particular that we can deduce that every type, including the empty type, is ...
1
vote
1answer
104 views

Is category theory just type theory with different words?

According this this category theory provides a semantics for type theory. To me this means that category theory and type theory are essentially the same system just with different words. In fact this ...
2
votes
1answer
135 views

Proof-irrelevant $\exists$

Under the principle of propositions-as-types, existential propositions in logic are compared to $\Sigma$-types, and we have two projection rules $\pi_1$ and $\pi_2$ to make proof extraction. If we ...
2
votes
1answer
34 views

In what sense is $\Pi x: A.B$ the same as $B[x := a_1] \times B[x := a_2]$ when A is a finite type with two elements $a_1$ and $a_2$

This is in the context of the Type Theory system $\lambda P$ as presented in Chapter 5 of "Type Theory and Formal Proof: An Introduction" by Rob Nederpelt and Herman Guevers. Since I am ...
1
vote
0answers
26 views

Comparison of type theory based on relations vs logic based on functions

As it has been mentioned in Type Theory article at Stanford Encyclopedia of Philosophy, type theories fall into two classes, one in which functions are not primitive but functional relations which I ...
0
votes
1answer
40 views

How do you do construct a proof in type theory?

I am reading about Type Theory and trying to understand how proofs work. The idea seems like, to prove something, you build up the type using the semantic construction rules. So I want to prove that 2 ...
1
vote
1answer
49 views

Propositional truncation and information hiding

I have a question regarding propositional truncation $||$-$||$ in homotopy type theory. According to the introduction rule of $||$-$||$, if $a:A$, then $|a|:||A||$. My question is, if $||A||$ is ...
0
votes
0answers
22 views

Strongly Dependent-type languages (running on windows)

What are the best dépendent-type programming languages to learn about type-theory ? I heard about coq, agda, epigram and idris; are there any other ? And most importantly: wich one of these can easily ...
0
votes
0answers
25 views

Proof that the type of homotopy equivalence is not a proposition

I've seen in The HoTT Book that assuming univalence for homotopy equivalences is inconsistent (this is Exercise 4.6). On some page, I've read that this is because without this "qinv-univalence&...
5
votes
1answer
65 views

Actual and potential truth for neo-verificationists

Neo-verificationists such as Martin-Löf and Prawitz make a distinction between actual and potential truth of a proposition, roughly defined as follows: ... that a proposition A is actually true means ...
0
votes
1answer
49 views

What are the consequences of alternative type-theoretic definition of homotopy equivalence?

The standard definition of homotopy equivalence in HoTT is a quadruple of: $f: A \rightarrow B$ $g: B \rightarrow A$ $p: \operatorname{id} A = g \circ f$ $q: \operatorname{id} B = f \circ g$ ... ...
0
votes
2answers
28 views

Extension of a Signature

I came across the following rule about signature extension in Harper's 1993 classical paper on LF (see page 5, Figure 1). $$\frac{\Sigma:sig\quad\vdash_\Sigma A:Type\quad c\not\in dom(\Sigma)}{\Sigma,...
2
votes
0answers
48 views

Context and Variable Declaration

I am a beginner in type theories. I have a basic question about the notion of context. It is commonly found in a textbook on type theories that a context (sometimes also called an environment) is ...
3
votes
1answer
43 views

Signature and Environment in Type Theory

Signature and Environment are both related to the description of constants. I feel confused about the two notions in type theory. Could anyone explain their main difference? Thanks!
3
votes
1answer
52 views

$a:A$ in $\Gamma$

I am taking an introductory course on type theory. I find the following sentence in my handout: ''$a:A$ in $\Gamma$'' or ''$\Gamma\vdash a:A$'' is equivalent to the following judgment ''$a(x_1,...x_n)...
1
vote
0answers
44 views

Can Cantor's theorem survive this kind of parametric type predicative restriction on set formation?

Language: mono-sorted first order logic with equality Extra-logical primitives: $T, \in, <$; the first signifies "the type of" and its a total one place function symbol, the second is set ...
1
vote
0answers
56 views

Necessity of decidable type checking for formalizing mathematics

If a type theory such as Martin-Löf's dependent type theory (MLTT) is to be used as a foundation for mathematics, decidable type checking is certainly nice to have: it guarantees that for every proof ...
5
votes
0answers
93 views

Dual of the fact that equalizers are dependent sums over the identity type

An equalizer of $A$ along two morphisms $f, g : A \to B$ can be thought of as a dependent sum over an identity type (see nLab): $$A|_{f = g} = \sum_{a : A} (f(a) = g(a))$$ Does this idea have a dual?...
1
vote
1answer
58 views

Context in Type Theory

I am reading a book on type theory. On page 105, the author says that If one views valid contexts as theories (in the sense of ordinary logics) a consistent context corresponds to a consistent ...

1
2 3 4 5
10