Questions tagged [type-theory]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
4
votes
0answers
84 views

Minimization of second-order unifiers

We know that first-order unification is decidable. More generally, if there exists a unifier for a first-order unification problem, then there exists a most general unifier. I'm interested in the ...
4
votes
0answers
122 views

Can every true type be reached from the unit type in small steps?

We are playing a game where you start at the unit type and the goal is to reach a given true type. You can go from your current location to another by writing down a (non-dependent) function of length ...
9
votes
1answer
805 views

Why are W-types called "W"?

Why are W-types called "W"? Probably "W" means either "wellordered" or "wellfounded". (Martin-Löf uses the term "wellorder".) But these are notions ...
6
votes
1answer
226 views

Does simple theory of types + ambiguity prove axiom of infinity?

Does simple theory of types + ambiguity prove axiom of infinity? The simple theory of types known as $\sf TST$ is a multi-sorted first order theory, syntactical restrictions include $\in$ being a ...
0
votes
0answers
133 views

Can ∞-category be defined in proof assistants?

Can ∞-category be defined in proof assistants? For example, we can directly consider a function such as ...
4
votes
1answer
308 views

What structure do all kinds of theories, models, interpretations, proofs and all that form?

This is a question about a structure that can be used to investigate all kind of structures that can be investigated. Many years ago with Joseph Gubeladze we discussed something similar but I only ...
3
votes
0answers
86 views

What is the connection between these proofs of strong normalization in $\lambda^\to$ and LK?

In Ralph Loader's lecture notes on lambda calculus (section 3.3), he states that a combinatorial proof of the SN of simply typed lambda calculus uses a technique that is "in essence that used by ...
6
votes
1answer
478 views

Practical Benefits of HTT/univalent foundations for assisted proofs

I'm trying to understand what the claimed practical benefits of HTT/univalent foundations are for doing computer assisted proofs and while I've seen a lot of claims of benefits they all seem to be ...
5
votes
1answer
154 views

Criterion for the consistency of pure type systems

Pure type systems are characterized in an almost combinatorial way: a set of axioms $\star_i : \star_j$, and a set of triples $(\star_i, \star_j, \star_k)$ saying when the dependent product $\prod_{x :...
2
votes
1answer
143 views

In cubical type theory, can we insist that "constant" compositions are the identity?

$\DeclareMathOperator{\comp}{comp}\DeclareMathOperator{\refl}{refl}\DeclareMathOperator{\transp}{transp}$I've been reading about Cubical Type Theory and playing around with the Agda implementation of ...
6
votes
0answers
168 views

Curry-Howard isomorphism: What is the logical counterpart of closure conversion?

Continuation-Passing Style (CPS) translation in programming languages corresponds to double-negation translation in logic (and the Yoneda lemma in category theory). Then what in logic corresponds to ...
12
votes
1answer
355 views

What is meant by a computational interpretation of univalence?

In homotopy type theory the univalence axiom implies function extensionality. Suppose we have a recursive set we are not sure is empty (e.g. the set of even integers$\geq 4$ that are not a sum of two ...
0
votes
0answers
92 views

What is the exact consistency strength of this type-set theory?

Language: bi-sorted first order logic with equality and its axiom and additionally the extra-logical primitives: $ ``\tau, < , \in"$, the first is a total unary function on sets denoting is the ...
2
votes
0answers
263 views

Can we have $\sf V=HTD$? How it relates to $\sf V=HOD$?

In my search for some type-set motivated line of thought that might prove axiom of choice, I was thinking of a concept that looks like $\sf V=HOD$, but in terms of types instead of ordinals, that is ...
6
votes
1answer
200 views

Categorical semantics of universe levels in dependent type theory

I know that locally closed cartesian categories provide categorical semantics for type theories with dependent products. What kind of categories model type theories with infinite universe hierarchies (...
1
vote
0answers
110 views

The difference between Agda and Idris for programming using Homotopy type theory [closed]

Which is better for programming benifiting by Homotopy type theory(HoTT),Idris or Agda.compare them.
3
votes
0answers
233 views

Intuitive (topological) explanation of a proof from the HoTT book [closed]

My friends and I are struggling with understanding intuitively the proof of equivalence between based and free path inductions (HoTT book 1.12.2) The first major problem is understanding the meaning ...
1
vote
0answers
54 views

Filtered colimits in type theory

My question is, what is a type theoretic way of expressing filtered colimits? Suppose, for instance, that we would like to express the filtered colimit of objects in a dependent type theory. How might ...
1
vote
0answers
120 views

What is the proof theoretic strength of PCF?

Godel's system $T$ means different, although equivalent, things to different people. To people working in the traditon of mathematical logic, $T$ is a quantifier-free equational theory of arithmetic ...
1
vote
0answers
87 views

constructive type theory references books

What is the best book you recommend for a beginner in constructive type theory applied to computer science?
32
votes
3answers
4k views

Top-down mathematics, or "Where it all begins"

Sorry if this is off-topic. It was my attempt to take a top-down approach to mathematics. Being an inexperienced undergraduate (so please take my writing here lightly), I've been presented with ZFC as ...
6
votes
2answers
296 views

Characterization of 'canonical' natural numbers objects

Canonicity is a useful property satisfied by some type theories, saying that every element of natural number type is propositional equal to an element of the form $s^n(0)$, where $s$ is the successor ...
7
votes
1answer
224 views

Ordered logic is the internal language of which class of categories?

Wikipedia says: The internal language of closed symmetric monoidal categories is linear logic and the type system is the linear type system. "A Fibrational Framework for Substructural and Modal ...
7
votes
2answers
244 views

Explicit different proofs of the same identity type in MLTT

This question is similar to (but more specific than) this one: When are two proofs of the same theorem really different proofs I do not know very much about homotopy type theory, but I am trying to ...
9
votes
1answer
448 views

3 questions about basics of Martin-Löf type theory

I started to read the HoTT book. I'm now on chapter 1 and I have several questions concerning not even homotopical, but "regular" type theory. On page 24, where the universes are introduced,...
3
votes
0answers
165 views

Is there a non-constructive dependent type theory?

If I understand correctly constructivism is not the only difference between intensional Martin-Löf type theory and a first-order set theory (e.g. ZFC). Can we drop constructivism and yet have a ...
10
votes
0answers
334 views

Are we sure the Calculus of Inductive Constructions and ZFC plus countably many inaccessible cardinals are equiconsistent?

This answer says, IIRC, the calculus of inductive constructions is equi-interpretable with ZFC plus countably many inaccessibles -- see Benjamin Werner's "Sets in Types, Types in Sets". (...
13
votes
4answers
1k views

Two interpretations of implication in categorical logic?

I am a bit confused about the interpretation of "implication" in the standard treatment of categorical logic, for example in [Bart Jacobs 1999] "Categorical Logic and Type Theory". ...
124
votes
5answers
21k views

What makes dependent type theory more suitable than set theory for proof assistants?

In his talk, The Future of Mathematics, Dr. Kevin Buzzard states that Lean is the only existing proof assistant suitable for formalizing all of math. In the Q&A part of the talk (at 1:00:00) he ...
0
votes
1answer
302 views

What does the ramified in ramified type theory mean?

I've recently become intrigued by the ramified type theory of Russell and Whitehead, for various reasons. I had thought it had been superseded by all the work since then. But now, I wonder whether I ...
9
votes
2answers
1k views

Russell's paradox as understood by current set theorists

Many mathematicians like to think of the set of natural numbers as existing as a completed object. But it is difficult to make set theory as concrete, because Russell's paradox, in conjunction with ...
0
votes
2answers
168 views

Type Theory with no Base Types

Is there any work in type theory where no base types are assumed, e.g., that there are only function types in place ($t_1 \to t_2$ is a type whenever $t_1$ and $t_2$ are types)? If not, are there ...
8
votes
0answers
157 views

Does the "coproduct-elimination transform" have an accepted name, and where can I learn more about it?

Suppose we're in a bicartesian closed category. Then given a morphism $$f : X \rightarrow Y_1 + \ldots + Y_n$$ and a test object $T$, we get a corresponding morphism $$T^f : X \times [Y_1,T] \times \...
2
votes
1answer
586 views

Data abstraction in set theory via Urelements

I am working in a setting of set theory where set theory is embedded in simply-typed higher-order logic, basically as described for example in Chad E. Brown and Cezary Kaliszyk and Karol Pak (2019) ...
6
votes
0answers
102 views

Inductive type constructors with the defined type appearing in non-strictly positive position

In the HoTT book §5.6 ‘The general syntax of inductive definitions’ there is a proof that the existence of an inductive type $T$ with a constructor $t : ((T \to \mathsf{Prop}) \to \mathsf{Prop}) \to T$...
0
votes
1answer
217 views

Why are quotient sets (types) called quotients -- are they the inverse of some product? [closed]

There seems to be a beautiful relation between natural numbers and sets (and types), as in the size of a discriminate union, cartesian product, and function type, is described by the sum, product, ...
0
votes
0answers
194 views

Is there a foundational approach that takes "structure" as primitive?

As per the title, I'd be curious to know if there have been attempts at constructing a foundation of mathematics taking, somehow, purely the notion of "structure" as primitive, maybe via a system of ...
7
votes
1answer
719 views

What types are to mathematical proofs as types à la Martin-Löf are to constructive proofs, and what's wrong with them?

The question is motivated by this surprising sentence from Freek Wiedijk's The QED Manifesto Revisited. I agree that the QED-like systems that exist today are not good enough to start developing ...
7
votes
1answer
324 views

Is $\prod_{X : \mathcal{U}} (X \to X) \cong 1$ consistent with type theory?

Assume we work in some minimalistic version of Martin-Löf type theory. Does it break consistency to postulate that the function that selects the identity function has an inverse? $$\prod_{X : \...
8
votes
2answers
561 views

Type theory - category theory correspondence

As explained here, simply typed lambda calculus can be viewed as a syntactic language for category theory. My question is, can the following modification make it equally well a formal syntactic ...
4
votes
1answer
384 views

Uniqueness principle for functions types in the HoTT book

Chapter 1.2 of the HoTT book says this about eta-conversion: $$ f \equiv (\lambda x . f(x)). $$ This equality is the uniqueness principle for function types, because it shows that $f$ is uniquely ...
2
votes
0answers
168 views

Categorical semantics of the identity type

In Appendix B of the article Simplicial Model of Univ. Foundations, Definition B.1.3 specifies the structure for identity types in a contextual category $\mathcal{C}$ (which in particular is equipped ...
5
votes
0answers
201 views

Are any formal systems based upon the idea of "iterated characterization pushing" currently in existence? If not, is anyone working on them?

I had an idea in regards to the design of formal systems with foundational aspirations. To convey the idea, let's talk a bit about the second-order Peano axioms. The way these axioms work, we have a ...
0
votes
2answers
311 views

A sequence in the hierarchy of universes

The HoTT Book states in the first chapter that universes are cumulative and that every universe is in some other universe. Obviously, there needs to be an infinite number of universes then, but ...
0
votes
0answers
139 views

An equation involving multisets

For finite multisets $A, B, C, A', B', C'$, if $A \uplus B \uplus \{B \uplus C\} \uplus \{A \uplus \{C\}\}$ = $A' \uplus B' \uplus \{B' \uplus C'\} \uplus \{A' \uplus \{C'\}\}$, must $A=A',B=B',C=C'$, ...
27
votes
8answers
6k views

Good introductory book to type theory?

I don't know anything about type theory and I would like to learn it. I'm interested to know how we can found mathematics on it. So, I would be interested by any text about type theory whose angle ...
6
votes
2answers
229 views

When is a fold monomorphic/epimorphic

Given a functor $F : \mathcal C \to \mathcal C$ with initial algebra $\alpha : FA \to A$, and another algebra $\xi : FX \to X$, we obtain a unique morphism $\mathsf{fold}~\xi : A \to X$ such that $\...
7
votes
2answers
1k views

How can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?

It is well-known that the simply typed lambda calculus is strongly normalizing (for instance, Wikipedia). Hence, it is not strong enough to be Turing-complete, as also mentioned on the Wikipedia page ...
3
votes
0answers
263 views

Formal foundations done properly [closed]

I would want to do mathematics properly, so that the proofs of results can be trusted on instead of them being just suggestions on which results could perhaps apply. This means formulating the math in ...
13
votes
1answer
638 views

A peculiarity of Henkin's 1950 proof of completeness for higher order logic

My question concerns Henkin's original (1950) completeness proof https://projecteuclid.org/euclid.jsl/1183730860 for classical higher order logic and type theory relative to so-called general models. ...