Questions tagged [type-theory]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
4 votes
1 answer
237 views

Is univalence equivalent to every type function being a functor over equivalence?

Introduce a rule in type theory that if $\Gamma \vdash f : \text{Type} \to \text{Type}$ and $\Gamma \vdash e : A \simeq B$ then $\Gamma \vdash f[e] : f(A) \simeq f(B)$. It may seem like such a rule is ...
Christopher King's user avatar
14 votes
1 answer
458 views

How exactly are realizability and the Curry-Howard correspondence related?

Consider, on the one hand: the Curry-Howard correspondence between, on the one hand, types and terms (programs) in various flavors of typed $\lambda$-calculus, and on the other, propositions and ...
Gro-Tsen's user avatar
  • 29.7k
2 votes
1 answer
120 views

Does substitution on named terms correspond to substitution on de Bruijn terms?

Altenkirch wrote (in the unpublished draft α-conversion is easy): I leave it to the reader to show that (some natural translation function) preserves substitution, i.e. it maps substitutions on named ...
Pavel Shuhray's user avatar
2 votes
0 answers
67 views

Relation of top and bottom types given multiple universes

This is something that I haven't seen mentioned in any literature. In a type theory (extensional, intuitionistic, Martin Lof variant), given two ordered Tarski Universes such that $U_i < U_{i+1}$, ...
Daniel Smith's user avatar
1 vote
1 answer
49 views

Constructing set-truncations of types from universes

This is a follow-up question from my previous question titled Constructing coproduct types and boolean types from universes, where I showed how every basic operation in set theory/topos theory could ...
Madeleine Birchfield's user avatar
4 votes
1 answer
134 views

Constructing coproduct types and boolean types from universes

Suppose we have a dependent type theory which has dependent product types, dependent sum types, identity types, function extensionality, an empty type, and a universe $U$ which is closed under the ...
Madeleine Birchfield's user avatar
3 votes
1 answer
83 views

How to represent morphisms in a fibration in the internal type theory

Given a fibration $p:\mathcal{E \to B}$, we can work with a minimal type theory with semantics in $p:\mathcal{E \to B}$, its internal type theory. The type theory for $p$ is dependent, with contexts ...
seldon's user avatar
  • 1,033
6 votes
1 answer
267 views

In HoTT with LEM, are sets and pointed sets the same thing?

The operations of adding and removing a point (where removing is a consideration of a subset of elements x such that $(x = *) \to 0$) implements the equivalence of these 1-types, as far as I can see. ...
Arshak Aivazian's user avatar
1 vote
0 answers
28 views

Any papers on the Lambek graph-$\lambda$ calculus-adjunction and the semantics of the Hindley Milner type system?

Joachim Lambek has described an adjunction between the category of graphs and the category of positive intuitionistic calculi with iteration, see e. g. Introduction to Higher Order Categorical Logic ...
Johan Thiborg-Ericson's user avatar
6 votes
1 answer
224 views

Existence property for second-order propositional logic

Consider the intuitionistic second-order propositional calculus (SOL) formulated in the full $\wedge,\vee,\rightarrow,\bot,\top,\forall,\exists$ language. Question: Assume that $\Gamma$ and $\Psi$ are ...
Z. A. K.'s user avatar
  • 333
6 votes
1 answer
172 views

Consistency in pure type systems

Summary My question is about how (i) a certain presentation of pure type systems in the $\lambda$-cube, bears on (ii) a standard definition of consistency in pure type systems. In short, I'm ...
Spaceka13's user avatar
0 votes
0 answers
47 views

Product types: algebraic structure for modeling product types with commutative and associative product operation

Is there a known algebraic structure over set of Types (however they are defined) which is equipped with: commutative and associative product operation for building product types from simpler types, ...
000 000's user avatar
8 votes
0 answers
94 views

Adjoining a morphism to a finitely complete category

Let $\mathscr C$ be a finitely complete category. Let $x, y$ be objects of $\mathscr C$. We can describe the universal property of freely adjoining a morphism $x \to y$ to $\mathscr C$: it comprises a ...
varkor's user avatar
  • 8,595
12 votes
2 answers
780 views

An overview of mathematical-logical approaches in formalizing natural languages

Crossposted on Mathematics SE I am an undergraduate mathematics student with a keen interest in pursuing research in the formalization of natural languages (from a more mathematical-logical approach),...
Heleyrine Brookvinth's user avatar
4 votes
0 answers
105 views

What exactly is the difficulty in giving a precise definition to dependent type theories?

In this talk by fields Medalist Vladmir Voevodosky on "The meta theory of dependent type theories" dated at Feb 27, 2017, the following is said: I start with a few words about the title. ...
tryst with freedom's user avatar
7 votes
0 answers
166 views

Constructive theory of Lie algebras

I'm looking for references on constructive Lie algebra theory, e.g. the sort of theory you could develop in Martin-Löf type theory or internal to some topos with a NNO. Obviously excluded middle is ...
ಠ_ಠ's user avatar
  • 5,875
10 votes
2 answers
910 views

Dependent sum/product and the base-change functor adjunctions

In type theory, the dependent sum $\sum_{x : A} T(x)$ and the dependent product $\prod_{x:A} T(x)$ are defined by their introduction/elimination rules. In category theory, we use a base-change functor....
Bartosz Milewski's user avatar
4 votes
0 answers
78 views

Lifting adjunctions along a localisation of 2-categories

Let $\mathcal S$ be a base category and let $Fib_\mathcal S^{split}$ be the 2-category consisting of split fibrations, fibered functors which strictly preserve the splitting and vertical ...
Nico's user avatar
  • 765
7 votes
1 answer
314 views

Does type theory help us avoid the "defining postulate"?

As a personal project, I decided to prove everything I learned in mathematics using formal proofs. The difference between informal proof, which is commonly used by mathematicians, and formal proof is ...
rfloc's user avatar
  • 463
5 votes
1 answer
337 views

Book that shows a construction of ZFC with Calculus of Constructions

Is there any book that teaches the basics of Type Theory and Calculus of Inductive Constructions (CIC) and also shows a construction of ZFC (or preferably NBG) in CIC? I only found the paper "...
rfloc's user avatar
  • 463
6 votes
0 answers
271 views

Is there any reason not to use Hofmann-Streicher universes?

Let $\mathcal C$ be a small category, and consider the topos $Psh(\mathcal C)$ of $Set$-valued presheaves on $\mathcal C$. For simplicity, assume that there exists a proper class of inaccessible ...
Tim Campion's user avatar
  • 60.2k
7 votes
1 answer
400 views

The idempotence of Mike Shulman's "Stack semantics"

I am struggling to understand lemma 7.20 of the paper Stack Semantics and the Comparison of Material and Structural Set Theories by Mike Shulman (arXiv:1004.3802). It contains formal sequents of the ...
Nico's user avatar
  • 765
5 votes
1 answer
157 views

Are lists in homotopy type theory free $A_\infty$-spaces?

Traditionally in dependent type theory with axiom K or uniqueness of identity proofs, every type $A$ is 0-truncated, and thus the type of lists on $A$, $\mathrm{List}(A)$, is 0-truncated and the free ...
Madeleine Birchfield's user avatar
5 votes
1 answer
276 views

Simple type theory: equational axioms validated by biCartesian closed categories

In this question, we consider only type theories with no ground types and no function symbols. I want to know whether there exists a model of simple type theory with finite products, finite coproducts,...
efk's user avatar
  • 193
1 vote
0 answers
41 views

Is stratified sorted rendering of naive set theory equivalent to tangled type theory?

I think the most important point in stratification is to have what may be called a fixed membership type distance per variable. What I mean is that if a variable $x_i$ occurs in a stratified formula $\...
Zuhair Al-Johar's user avatar
10 votes
0 answers
304 views

Feferman's universes for proof assistants?

This question was prompted by a discussion from another MO question about the consistency of ZFC. There are some mathematicians who are comfortable with ZFC but uneasy with large cardinals. For them,...
Timothy Chow's user avatar
  • 77.9k
7 votes
0 answers
228 views

New Foundations in a Homotopy/Intuitionistic Type Theory form?

New Foundations is a famously odd set theory suggested by Quine in the 1930s which: Features a universal set. Disproves the axiom of choice. Proves the existence of an infinite set by a trivial ...
wlad's user avatar
  • 4,782
1 vote
0 answers
73 views

Directly proving the extensionality principle for product types without quasi-inverses

In section 2.6 of the Univalent Foundations Project's Homotopy Type Theory book, the extensionality principle of product types is proven by showing that for all elements $a:A$, $a':A$, $b:A$, $b':A$, ...
Madeleine Birchfield's user avatar
2 votes
1 answer
322 views

Undecidable statements in type theory

In type theory, proving a statement means to exhibit an instance/element of a type corresponding to the statement. But if the statement is undecidable, no element of the type A nor its negation A → ⊥ ...
Daniel Murcia's user avatar
7 votes
1 answer
611 views

Open problems in type theory

I am only a beginner in the field of type theory, and I'm wondering if the community could point me out a few open problems in the field. I have a good background in logic, in particular, proof theory ...
6 votes
1 answer
141 views

Univalence for weakly Tarski universes

In Martin-Löf type theory, a weakly Tarski universe is a type $\mathcal{U}$ with a type family $\mathcal{T}(A)$ indexed by terms $A:\mathcal{U}$, which is closed under identity types, dependent ...
Madeleine Birchfield's user avatar
2 votes
1 answer
373 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 ...
Madeleine Birchfield's user avatar
4 votes
1 answer
173 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,...
Jii's user avatar
  • 301
-1 votes
1 answer
171 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 ...
Zuhair Al-Johar's user avatar
3 votes
2 answers
487 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 ...
Zuhair Al-Johar's user avatar
2 votes
1 answer
468 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 ...
Madeleine Birchfield's user avatar
0 votes
1 answer
273 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 ...
Zuhair Al-Johar's user avatar
1 vote
0 answers
51 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 ...
Zuhair Al-Johar's user avatar
1 vote
0 answers
123 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....
Zuhair Al-Johar's user avatar
1 vote
0 answers
108 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 ...
Zuhair Al-Johar's user avatar
0 votes
1 answer
197 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 ...
Hexirp's user avatar
  • 335
2 votes
0 answers
89 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 ...
Zuhair Al-Johar's user avatar
6 votes
1 answer
340 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 ...
Ilk's user avatar
  • 559
4 votes
1 answer
295 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 ...
Madeleine Birchfield's user avatar
1 vote
0 answers
225 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 ...
Alexander Praehauser's user avatar
2 votes
1 answer
221 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 ...
Ilk's user avatar
  • 559
1 vote
0 answers
123 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?
Glubs's user avatar
  • 109
4 votes
4 answers
703 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)$...
qk11's user avatar
  • 505
6 votes
0 answers
321 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 &...
qk11's user avatar
  • 505
3 votes
0 answers
122 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 ...
qk11's user avatar
  • 505

1
2 3 4 5