Questions tagged [type-theory]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
-10 votes
0 answers
239 views

Is there a simple example of why homotopy type theory is useful? [closed]

Feynman said that when he was attempting to understand a complex physical theory he would hold in his mind the simplest physical example to which it would apply. This is why he was able to demolish ...
2 votes
1 answer
124 views

Path types and identity types in dependent type theory

There's been some debate at the nLab recently over the names of "identity type" and "path type" in certain dependent type theories. One user wrote that Many cubical type theorists ...
3 votes
0 answers
74 views

Extending the class of primitive recursive functions with higher order recursion schema

I'm trying to extend the class of primitive recursive functions by extending the recursion schema over higher types. We usually define the class of primitive recursive functions by using zero function,...
  • 191
-1 votes
1 answer
149 views

Is there an obvious inconsistency with this extension of Tangled Type Theory?

This posting is a follow up of this Language multi-sorted FOL, with sorts (types) indexed by the naturals, equality symbol restricted to same type, while membership symbol restricted from lower to ...
3 votes
2 answers
419 views

Can we write Tangled Type Theory without reference to type sequences?

I just want to know if Tangled Type Theory $\mathsf{TTT}$ of Randall Holmes ([see: Holmes - NF is consistent, p:11, Holmes - The equivalence of NF-style set theories with “tangled” type theories; the ...
2 votes
1 answer
169 views

Higher inductive types in higher observational type theory

Mike Shulman gave the following set of talks on higher observational type theory earlier this year (part 1, part 2, part 3). However, while he talked about how the identity types are defined and ...
1 vote
1 answer
247 views

Is this theory equivalent to Tangled Type Theory?

Language: Multi-sorted first order logic with equality and membership, where for each natural $n$ we have variables $x_i^n$ of sort $n$, and for each decidable monotonic strictly increasing sequence ...
1 vote
0 answers
36 views

What is the consistency strength of this addition on simple type-set theory?

Language: multi-sorted first order logic with equality and membership, where for each natural $n$ there is a set $x^n$ of sort $n$. Equality "$=$" only occurs between variables of the same ...
1 vote
0 answers
108 views

What is the proof theoretic ordinal of this kind of predicative type-set theory?

The following is a kind of Predicative Type Set Theory. The question is about what is exactly the proof theoretic ordinal of this theory? Is it lower than the one expected for predicative theories, i....
1 vote
0 answers
97 views

Can this type theory interpret second order arithmetic?

Language: multi-sorted first order logic with equality and membership, where for each natural $t$ there is a set $x^t$ of sort $t$. Equality "$=$" only occurs between variables of the same ...
0 votes
1 answer
123 views

Construct higher inductive types with only generalized algebraic data types and non-truncated quotients?

Higher inductive types are a useful concept in homotopy type theory. However, considering its general syntax is a bit of a challenge. Is it possible to implement all higher inductive types with just ...
  • 283
2 votes
0 answers
84 views

Can this predicative kind of type-set theory reach the consistency of ${\sf Z}_2$?

Add a primitive total one place fuction symbol $\tau$, and a primitive binary relation $<$, to the language of set theory. Add the following axioms: Extensionality: $\forall z \, (z \in x \iff z\in ...
6 votes
2 answers
281 views

Are infinitary monads monadic?

As discussed here, Are monads monadic?, in "On the monadicity of finitary monads" by Steve Lack, the following is shown, the forgetful functor from $Mnd_f(C) \rightarrow Endo_f(C)$ is ...
  • 239
3 votes
1 answer
143 views

Codependent types in type theory

The nLab's article on coinductive types here states that There is an obstacle to the complete dualization of the usual rules for inductive types in homotopy type theory, including dualizing the ...
1 vote
0 answers
131 views

Understanding the double negation modality under the "propositions as types" paradigm

$\DeclareMathOperator\Hom{Hom}$I'm trying to understand the double negation modality under the "propositions as types" paradigm, but I'm running into an apparent contradiction: let $T$ be a ...
2 votes
1 answer
191 views

Well-behaved monad quotients

Reading through Modular specification of monads through higher-order presentations, this paper includes the following lemma within set-truncated homotopy type theory: Given a monad $R$ (they work on ...
  • 239
1 vote
0 answers
103 views

What does "sup" mean in the context of a w type? [closed]

Like the constructor for a W type is called "sup" but I don't know what that expands to. Is it super? maybe supremum? Or is it just an arbitrary name, like dynamic programming?
  • 89
4 votes
4 answers
469 views

Why in Martin-Löf type theory any natural number is assumed to be either $0$ or $S(a)$ for some $a\in\mathsf{N}$?

In laying down the equality rules in Martin-Löf type theory, e.g., for the type $\mathsf{N}$ of natural numbers, there seems to be an implicit assumption that any natural number is either $0$ or $S(a)$...
  • 505
6 votes
0 answers
237 views

More rigorous presentations of Martin-Löf type theory?

I'm enjoying reading Martin-Löf's 1972 paper "An Intuitionistic Theory of Types" for the first time (this constitutes my first-ever exposure to Martin-Löf's papers), but at times find the &...
  • 505
3 votes
0 answers
112 views

Translating set-theoretic concepts to polymorphic type theory or beyond

I've been trying to read Coquand's "An Analysis of Girard's Paradox" lately. I've noticed that he gets a type-theoretic variant of Burali-Forti's paradox once he extends Church's system with ...
  • 505
12 votes
1 answer
528 views

Why does Coq restrict Inductive definitions, and how is this related to Inaccessible cardinals?

Coq lets you define an inductive type of the following form: Inductive Foo := | Base : Foo | Positive : (nat -> Foo) -> Foo. because the position of <...
  • 121
24 votes
1 answer
1k views

Coinduction for all?

Every undergraduate in mathematics learns about proofs by mathematical induction. Moreover, every undergraduate taking a course in theoretical computer science or logic learns about inductive ...
8 votes
1 answer
449 views

What is the status of Jordan's theorem in constructive mathematics in the language of locales?

By constructive mathematics in this matter we mean intuitionistic ZF (*). In the language of locales, the Jordan curve can be defined as $f\colon S^1 \to X$ such that "if $U \cap V = \varnothing$,...
2 votes
1 answer
268 views

Abstraction logic

As part of my research on building an interactive theorem proving system, I have discovered a new logic that I call Abstraction logic. I have written up the details here: https://doi.org/10.47757/...
4 votes
0 answers
89 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
0 answers
130 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 ...
10 votes
1 answer
918 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
1 answer
274 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
0 answers
193 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 ...
  • 283
4 votes
1 answer
367 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
0 answers
119 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 ...
  • 447
8 votes
1 answer
600 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 ...
  • 1,635
6 votes
1 answer
251 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 :...
  • 447
4 votes
1 answer
260 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 ...
7 votes
0 answers
237 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 ...
  • 133
13 votes
1 answer
460 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 ...
  • 131
2 votes
0 answers
294 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 ...
7 votes
1 answer
264 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
0 answers
140 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.
  • 11
3 votes
0 answers
249 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
0 answers
64 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 ...
  • 4,443
1 vote
0 answers
146 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 ...
  • 442
1 vote
0 answers
146 views

constructive type theory references books

What is the best book you recommend for a beginner in constructive type theory applied to computer science?
  • 21
33 votes
3 answers
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 ...
  • 447
6 votes
2 answers
330 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 ...
  • 65
7 votes
1 answer
270 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
2 answers
276 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 ...
11 votes
1 answer
539 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
0 answers
212 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 ...
  • 39
17 votes
2 answers
786 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". (...
  • 283