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
0 answers
65 views

2-categorical universal property of the classifying category of a type theory

For example let us say we are in the setting of cartesian closed categories and the simply typed $\lambda$-calculus. Let $\mathtt{strCCCat}$ denote the $2$-category of strict cartesian closed ...
user avatar
  • 1,368
2 votes
0 answers
61 views

Proofs and Types: Girard's remarks on Theoretical Computing

In the first chapter of Girard's Proofs and Types (1989) one finds the following remarks: Theoretical Computing is not yet a science. Many basic concepts have not been clarified, and current work in ...
user avatar
  • 1,707
0 votes
0 answers
46 views

Type Theory: solution to paradoxes?

It’s my understanding this causes Russell paradox: $L = \{x : \lnot( x \in x)\}$ ZFC solution is to restrict comprehension. I also understand that Russel created Type Theory to solve the paradox. How ...
user avatar
  • 939
2 votes
1 answer
56 views

Isomorphism vs. equivalence of types and homotopy vs. equality of functions

I am trying to build an understanding of the Univalence Axiom in HoTT and I am slightly confused about some definitions. If I was asked after reading of Chapter 1 of the HoTT book to formulate a ...
user avatar
  • 2,688
1 vote
0 answers
61 views

$\omega$ incompleteness of $\lambda$ calculus

In Plotkin's 'The $\lambda$-Calculus is $\omega$-Incomplete' (The Journal of Symbolic Logic Vol. 39, No. 2 (Jun., 1974), pp. 313-317), an example is given of two (untyped) $\lambda$-terms $M$ and $N$ ...
user avatar
1 vote
0 answers
65 views

Using the Calculus of Constructions as a metalogic

Usually the Calculus of Construction is used via the Curry-Howard isomorphism, which makes it equivalent to intuitionistic first order logic. But what I am interested in is to use CoC as a metalogic ...
user avatar
0 votes
0 answers
64 views

Is type theory complete by definition?

From my understanding, type theory is its own deductive system, meaning that types have propositional meanings. Therefore, an element of a type appears to be an evidence of the truth of the ...
user avatar
  • 23
2 votes
0 answers
75 views

Lean and inacessible cardinals

Here it is claimed that Lean's type theory is equiconsistent with ZFC + existence of $n$ inacessible cardinals for every natural $n$. This is a bit worrying if you just want to work with pure ZFC: how ...
user avatar
  • 41
4 votes
0 answers
97 views

The double negation of excluded middle in type theory

Context The following question concerns plain Martin-Löf type theory, under a propositions-as-types interpretation: in particular, proposition simply means type and not mere proposition, and ...
user avatar
  • 5,917
2 votes
1 answer
138 views

Is there a distinction between rules of inference and axioms in Homotopy Type Theory (HoTT)?

I'm taking rules of inference to be metalinguistic and to describe when you can write down a certain syntactic expression in the object-language given that you already have others written down (e.g. &...
user avatar
2 votes
0 answers
40 views

Typing context as a monad for multicategories

In some ways simple type theory matches up nicer with multicategories than with categories. A hom $$ f \colon o_1 ; \ldots o_n \rightarrow o'$$ Matches up nicely with a well typed term $$ x_1 \colon ...
user avatar
1 vote
0 answers
62 views

Modern Type Theory vs. Martin Löf Type Theory

I have been reading Martin Löf notes on type theory to get a historical feel for the subject and I find some of the terminology confusing (e.g. distinction judgements and propositions, between proofs ...
user avatar
  • 131
1 vote
1 answer
42 views

Prove: if Γ ⊢ L : σ, then Γ is a λ2-context.

This is exercise 3.19 from “Type Theory and Formal Proof” by Rob Nederpelt and Herman Geuvers. My faulty starting point: by the definition of a λ2-context we know that if Γ is a λ2-context such that L ...
user avatar
3 votes
1 answer
147 views

Mistake in B. Jacobs book Categorical Logic and Type Theory?

Lemma 1.8.9 in B. Jacobs book Categorical Logic and Type Theory describes how a collection of fibre-wise adjoints of a morphism of fibrations can be promoted to a global adjoint. Let $p: \mathbb E \...
user avatar
  • 1,368
1 vote
0 answers
54 views

Proof relevant relation

Let $$ac : \left( \prod_{(x:A)}\sum_{(y:B)}R(x,y) \right) \rightarrow\left( \sum_{(f : A \rightarrow B)}\prod_{(x:A)}R(x,f(x)) \right)$$ defined by $$ac(g) :\equiv \Big( \lambda x.pr_1(g(x)), \lambda ...
user avatar
  • 23
1 vote
1 answer
72 views

Recursor and induction functions in dependent type theory

I'm reading HoTT book and I'm not sure if I really understand how the recursor function is related to the induction function. It is stated that product types are said to be : a degenerate example of ...
user avatar
  • 23
5 votes
4 answers
326 views

Elimination rule for identity types in Martin-Lof Type Theory

The rule for identity type elimination still mystifies me, and I have not been able to find anything that satisfies me in any book. Consider, for example, the form of the rule on p. 112 of Thompson: \...
user avatar
3 votes
0 answers
70 views

If Cartesian product of sets becomes an internal hom in Rel what do functions become?

The category of relations between sets has an internal hom (Cartesian product). You have an isomorphism $$ \textbf{Rel}(A, B \times C) \sim \textbf{Rel}(A \times B, C) $$ However, Rel is closed ...
user avatar
2 votes
2 answers
92 views

theorem for free: relation cartesian product

I am digging through a paper Theorems for free and a bit confused on the source of some conjectures (page 5): Is it an axiom or it can be implied from some other axioms? UPD Question is about ...
user avatar
1 vote
2 answers
121 views

Type Theory: we cannot prove double negation, but can we prove it is unprovable?

I'm currently trying to learn type theory from the first chapter of HoTT. It is remarked that we cannot prove $\neg\neg A \rightarrow A$, when $A$ is interpreted as a proposition, or, equivalently, we ...
user avatar
1 vote
1 answer
66 views

Propositional Uniqueness for Coproduct Types?

I'm working through the HoTT book and have just finished the section on coproducts. In short, I am wondering if there is a uniqueness principle for coproduct types. I can not find mention of one in ...
user avatar
7 votes
1 answer
232 views

Object Classifier implies Univalence in Type Theory?

There is a correspondence between univalence in Type Theory and object classifiers in $\infty$-toposes. This, for example, is suggested in the article Univalent Foundations for Mathematics on nlab. ...
user avatar
  • 73
3 votes
2 answers
304 views

Impredicative Definitions (CZF)

CZF is touted as the predicative and constructive variant of ZF. This is because CZF avoids the fully impredicative axioms of powerset and full separation and alternatively because CZF has an ...
user avatar
  • 131
36 votes
3 answers
3k views

Under the Curry-Howard correspondence or loosely "proofs-as-programs", do we also have "programs-as-proofs" and what would some arb. program prove?

Curry-Howard Correspondence Now, pick any 5-30 line algorithm in some programming language of choice. What is the program proving? Or, do we not also have "programs-as-proofs"? Take the ...
user avatar
0 votes
0 answers
81 views

Is there a category-theoretic version of Girard's paradox?

Suppose, to approximate Girard's paradox, that we have a category whose collection of objects includes itself. Can we conclude that such a category has no initial object, or something similar? I don't ...
user avatar
  • 323
1 vote
1 answer
97 views

How to justify claims on the complexity of formal proofs without definitions, as described in "Type Theory and Formal Proof" by Nederpelt and Geuvers

In the chapter Definitions of "Type Theory and Formal Proof" by Nederpelt and Geuvers, they start with some motivating examples and then state (with my emphasis added) [T]here is also a ...
user avatar
1 vote
1 answer
67 views

What does this typed lambda-calculus notation mean?

In Definition 3.2 (page 12) of Gallier's 'Constructive Logics Part I: A Tutorial on Proof Systems and Typed Lambda-Calculi' he sets out the rules for his typed $\lambda^{\to, +, \times, \perp}$-...
user avatar
0 votes
0 answers
55 views

What is a correct way to prove the next propositional logic statement using Curry–Howard correspondence?

I am studying Curry–Howard correspondence. Given propositional logic statement: (¬p -> q) -> ((¬p -> ¬q) -> p). I need to define a type (as proposition) ...
user avatar
  • 387
0 votes
0 answers
56 views

Definition of ZFC2 (second order logic)

ZFC with 1st order logic is known. My question may be formulated either way What is the definition of ZFC2 (ZFC+second order logic)? (I assume that formulas also have quantifications of two kind over ...
user avatar
  • 704
4 votes
1 answer
94 views

Can you define functions which are not primitive recursive, yet total, in Type Theory? [closed]

Ackermann's function is total but not primitive recursive. Can one define Ackermann's function in Type Theory, ie: Can you define functions which are not primitive recursive, yet total, in Type Theory?...
user avatar
  • 143
1 vote
1 answer
161 views

Ordinary mathematical uses of Axiom K

Context. In what follows, we work in Martin-Löf type theory (MLTT). We denote dependent product types by $\forall$, the identity type over a type $T$ by $\equiv_T$, and let $U$ stand in for arbitrary ...
user avatar
  • 5,917
0 votes
0 answers
17 views

Inversions of a partition of a certain type

I am having trouble getting started on this problem as I'm not sure what partitions of type (2, 0, 3) refer to. I have been unable to research partitions of a "type" like this. Does anyone ...
user avatar
1 vote
2 answers
107 views

Translating the induction principle from verbal form into rigorous one

According to the HoTT book [6.9], the propositional truncation $||A||$ of a type $A$ can be viewed as a higher inductive type generated by A map $|-|: A \to ||A||$ A path in $x = y$ for any $x,y: ||A|...
user avatar
1 vote
1 answer
84 views

Generalization of Lawvere's fixed point for a bijection between $A$ and $(A\to B)\to B$

At the end of his paper about the set semantics of System F, Reynolds produces two sets $A,B$ and a bijection between $A$ and $(A\to B)\to B$. He concludes "since $(A\to B)\to B$ and $A$ are well-...
user avatar
1 vote
1 answer
51 views

What is a type equation? Could you link me to some sources? Does it have any other names?

I was reading about maybe in the haskell documentation and it mentioned a type equation. I have been reading a bit on type theory but I had never seen it before. It was not mentioned on the type ...
user avatar
  • 105
3 votes
1 answer
107 views

Confusion about quasi-inverses and equivalences in HoTT

I'm reading the HoTT book, section 2.4, where for $f : A \to B$, they define $$\mathsf{qinv}(f) = \sum_{g:B\to A} \big( (f \circ g \sim \mathrm{id}) \times (g \circ f \sim \mathrm{id}) \big)$$ $$\...
user avatar
0 votes
0 answers
60 views

Syntax independent presentation of Homotopy Type Theory

By "syntax independent" I mean no explicit reference to variables. For example, Lambda Calculus is syntax dependent because the notions of "variable", "variable renaming",...
user avatar
  • 97
2 votes
1 answer
67 views

Can function types be represented using $\Sigma$-types?

Fix types $A, B : \mathsf{Type}$, and let $\mathbf{2} = \{ 0, 1 \} : \mathsf{Type}$ be a two-element type. We define $B' : A \to \mathsf{Type}$ by $B'(a) = B$. $C : \mathbf{2} \to \mathsf{Type}$ by $...
user avatar
0 votes
1 answer
62 views

Can you have Type Theory without types?

Thinking about Type Theory, we define types such as the natural numbers: zero:Nat succ(n:Nat):Nat But I thought that this might be equivalent to having just 2 ...
user avatar
  • 3,981
0 votes
1 answer
143 views

Why isn't there an app that allows you to enter in all the rules of a given formal system so that the app supports all formal systems of math?

I'm jumping around between articles about ETCS to Simple TT to Calculus of Constructions wondering what my app should focus on. I'm wondering, why there isn't yet a software app in which you can ...
user avatar
3 votes
1 answer
89 views

Why isn't $\forall x \in X, P(x)$ the same thing as a map of types $P:X \to \text{TrueProp}$?

For example, $\forall x \in X, P(x)$ can be viewed as a map $P : X \to \text{TrueProp}$ the collection of true propositions. Why do we make the distinction in type theory, which seems to want to ...
user avatar
0 votes
0 answers
67 views

Why does a type of all types including itself create a paradox in Martin-Löf type theory?

In Per Martin-Löf (1998) "An Intuitionistic Theory of Types" in G Sambin and JM Smith (eds) Twenty-five years of constructive type theory Clarendon Press (original work written 1972 but ...
user avatar
1 vote
1 answer
93 views

How to derive $\prod x: \text{Nat}, Id(S(x), O) \to \bot$ in Intensional Type Theory

In HoTT Lecture, https://www.youtube.com/watch?v=VWmXF-P4-Z8&list=PL1-2D_rCQBarjdqnM21sOsx09CtFSVO6Z&index=7, Harper introduced a dependent form of recursion rule: $$ \Gamma \vdash M : Nat ~~~ ...
user avatar
0 votes
1 answer
88 views

In homotopy type theory, what is this "mechanical way to create a new expression F' now depending on t' and an equivalence between F(T) and F'(T')"? [closed]

I've read a few slides on the topic citing the following quotation from an email, which, according to these slides, defines the biggest advantage of homotopy lambda calculus over other caculi of ...
user avatar
  • 109
2 votes
1 answer
112 views

λP2, the Calculus of Constructions, and quantifying over propositions

In $\lambda P2$, we can write polymorphic functions like $\Lambda A. \lambda x. x: \Pi A. A \to A$. By Curry–Howard, this corresponds to the proposition "for all propositions $A$, $A$ implies $A$&...
user avatar
  • 123
2 votes
0 answers
78 views

Homotopy type theory: what is «path induction» useful for?

I am reading the HoTT book. At page 49 path induction is introduced. Let us recap it. Given a family $$ C: \displaystyle \prod_{(x,y:A)} x =_A y \rightarrow 𝓤 $$ and a function $$ c: \displaystyle \...
user avatar
7 votes
0 answers
148 views

Precise statement of the syntactic category of a logic/type theory, in maximum generality?

I've been trying to understand the notion of syntactic category for a type theory/logic. This entry in the ncatlab is the closest I've found to a clear explanation. It seems like a fairly good article,...
user avatar
  • 11.9k
1 vote
2 answers
97 views

Formalizing constant symbols as terms in type theory.

In type theory, we usually define each type with a constant symbol, e.g., the dependent product uses '$\Pi$', the dependent sum uses '$\Sigma$', the sum/coproduct uses '$+$'. I noticed that we could ...
user avatar
  • 171
1 vote
1 answer
70 views

Does the degree of impredicativity always matter in type theory?

My question here is actually about whether different degress of impredicativity matter? To show that, lets confine ourselves with the following predicative formalism. Language: multi-sorted first ...
user avatar
  • 3,553
2 votes
2 answers
163 views

judgmental and propositional statements in homotopy type theory

In homotopy type theory one has to distinguish between judgmental and propositional statements, eg in case of $a: A$ ("$a$ has type $A$") and equalities $a =_p b, a=_A b$. That is, are a ...
user avatar

1
2 3 4 5
13