Questions tagged [type-theory]
The type-theory tag has no usage guidance.
201
questions
9
votes
2
answers
388
views
Categorical semantics of W-types
Jacob's book titled "Categorical Logic and Type Theory" gives a nice description of Π and Σ types as adjunctions to substitution functors induced by display maps. Is there a similar ...
9
votes
3
answers
935
views
What do I call type theory without Curry-Howard?
Is there a word I can say which will convey to type theorists that I am not thinking about types as propositions?
Background: as a category theorist, I am mostly interested in type theories as a ...
9
votes
1
answer
770
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 ...
9
votes
2
answers
785
views
How should I be thinking about object classifiers / universal fibrations / universes?
I have been learning about homotopy type theory this summer. I am not a homotopy theorist but I am more comfortable with homotopy theory than I am with type theory, so the way I rationalize many of ...
9
votes
2
answers
1k
views
Progress towards a computational interpretation of the univalence axiom?
I will preface this by saying that I am not an expert on type theory. I am just a curious outsider slowly making my way through the HoTT book when I (rarely) have some spare time.
I am just curious ...
9
votes
0
answers
409
views
What metatheory proves cut elimination for Simple Type Theory?
Gaisi Takeuti's book Proof Theory proves cut elimination for Simple Type Theory (a combined result of several researchers). Thus it proves consistency of Simple Type Theory with full comprehension in ...
8
votes
3
answers
970
views
How to handle sums in Tait's reducibility proof of strong normalisation?
I've been reading Girard et al's 'Proofs and Types', which in Chapter 6 presents a proof of strong normalisation for the simply typed lambda calculus with products and base types. The proof is based ...
8
votes
2
answers
935
views
Identity types: What makes Intuitionistic Type Theory *intuitionistic*?
In the opening passage of Martin-Löf's (1975) he famously says that
"the theory of types with which we shall be concerned is intended to be a full scale system for formalizing intuitionistic ...
8
votes
3
answers
2k
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 ...
8
votes
2
answers
2k
views
Is simply typed lambda calculus with fixed-point combinator Turing-complete?
There are many sources cite that simply typed lambda calculus extended with fixed-point combinator is Turing complete. For example, Does there exist a Turing complete typed lambda calculus? or the ...
8
votes
2
answers
601
views
Reduction rules for inductive types
(I'm not sure if I should post this here rather than at Theoretical Computer Science, I've found a lot of type theory related questions on MathOverflow)
I'm working in Martin-Löf type theory with ...
8
votes
2
answers
695
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 ...
8
votes
1
answer
1k
views
What fails when using call/cc as realizer of the Peirce formula
Define the axiom constants $p_{A,B}^{((A\rightarrow B)\rightarrow A)\rightarrow A}$ as realizers of the Peirce formula, and $f_A^{\bot\rightarrow A}$ as realizers of the Ex Falso Quodlibet. Then $p_{A\...
8
votes
1
answer
724
views
Easier Girard's paradox in a circular pure type system (PTS)
System U is an inconsistent PTS in that one has a term of type $\bot = \forall p\colon \ast \ldotp p$, and such a term is explicitly constructed in Hurkens' A Simplification of Girard's Paradox.
One-...
8
votes
1
answer
682
views
Constructing unnatural transformations
In a nutshell, the question is: is it true that any explicit (not involving axiom of choice) pointwise transformation between sufficiently complicated functors is natural almost everywhere?
Let $C$ ...
8
votes
1
answer
619
views
The independence of path induction
In §1.12 of the Homotopy type theory book, it is mentioned that indiscernibility of identicals is a consequence of path induction. More precisely, for each type $C$ dependent over a type $A$, there is ...
8
votes
1
answer
511
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$,...
8
votes
1
answer
342
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 (...
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 ...
8
votes
0
answers
316
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 ...
8
votes
0
answers
171
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 \...
8
votes
0
answers
187
views
Generalized (co)-presheaves for Generalized Multicategories?
A $T$-multicategory in the sense of Crutwell-Shulman, where $T$ is a monad on a virtual double category $C$ is a monoid in the "horizontal kleisli category", i.e., an object of objects $O$, a ...
8
votes
0
answers
218
views
Ends and parametricity
It is well known that a set of natural transformations can be expressed as an end:
$$\int_{A \in \mathcal{A}} \mathcal{B}(FA, GA) =_{\operatorname{Set}} \operatorname{Nat}(F, G)$$
This holds for ...
7
votes
3
answers
1k
views
Extensionality in HoTT versus extensionality in internal language of a category
What's the extension of judgmental identity in HoTT (homotopy type theory)?
The Martin-Löf intensional dependent type theory with identity types is called (definitionally) extensional if the ...
7
votes
4
answers
1k
views
What is the intuitive meaning of star and box in a pure type system?
The systems of the λ-cube have the axiom $\star:\square$.
I've listed a few meanings that the Curry-Howard isomorphism gives to $t : T$ below. What are the intuitive meanings of $\star$ and $\...
7
votes
2
answers
338
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 ...
7
votes
3
answers
752
views
Can a typing judgment admit essentially different derivations?
In any sort of type theory, there are a bunch of rules for constructing derivations of typing judgments such as $x:A,\; y:B(x) \;\vdash\; z:C(x,y)$. (I intend to include also judgments of the form $B:...
7
votes
1
answer
852
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
2
answers
419
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
1
answer
427
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 : \...
7
votes
1
answer
2k
views
intensional equality in type theory
I want to know why we add an intensional equality in type theory to definitional equality ?
What is the aim with this intensional equality ?
thanks
7
votes
1
answer
1k
views
categorifying induction in homotopy type theory
In trying to understand homotopy type theory, I stumbled upon the following silly question, which is likely to be trivial for the experts.
Let $B=\sqcup_{n\in\Bbb N} BS_n$, which I'd like to think of ...
7
votes
2
answers
1k
views
Recursively dependent types?
Is there such a thing as "recursively dependent types"? Specifically, I would like a dependent type theory containing a type $A(x)$ which depends on a variable $x: A(z)$, where $z$ is a particular ...
7
votes
1
answer
641
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 ...
7
votes
1
answer
343
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
1
answer
321
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 ...
7
votes
1
answer
406
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 ...
7
votes
1
answer
387
views
Pure first order logic formulations of Markov's principle
Markov's principle is a statement of constructive arithmetic that allows classical reasoning on formulas of the shape $\exists x P$ when $P$ is a recursive predicate:
$\neg \neg \exists x P \to \...
7
votes
1
answer
564
views
$\Pi$, $\Sigma$, and identity types without $\eta$ in comprehension categories
In comprehension categories, dependent sums are defined as a choice of left adjoints for all reindexing functors along display maps, satisfying a Beck-Chevalley condition. Dependent products are ...
7
votes
1
answer
329
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 :...
7
votes
0
answers
167
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 ...
7
votes
0
answers
233
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 ...
7
votes
0
answers
293
views
Feasible Type Theories
I am looking for references about efficient type theories,
efficiency in the sense of computational complexity,
and type theory in the sense of Martin-Lof's type theories.
Has there been any studies ...
6
votes
2
answers
358
views
Why no morphisms from the contradictory proposition to the inconsistent context?
Consider Higher order predicate logic over dependent type theory (DPL) as defined in Chapter 11 of B. Jacobs's book "Categorical Logic and Type Theory" (though I think this question applies to first-...
6
votes
1
answer
256
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 ...
6
votes
1
answer
174
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 ...
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 ...
6
votes
1
answer
411
views
Proof of ¬(¬1 ⊗ ¬1) in tensorial logic
I believe I once had a proof of this proposition, but it's been lost to the mists of time and old hard drives, so who knows if it was correct, and try as I might I can't seem to reproduce it.
Is it ...
6
votes
1
answer
825
views
Rice's theorem in type theory
From the formula
$$\forall f\colon A\to A\,\exists x\colon A\,(f(x)=x)$$
we can get the scheme
$$\forall x\colon A\,(\phi(x)\vee\neg\phi(x))\Rightarrow\forall x\colon A\,\phi(x)\vee\forall x\colon A\,\...
6
votes
1
answer
350
views
On an automatic translation of typed lambda calculus in untyped lambda calculus
I have a question regarding the "compilation" of typed lambda calculus in untyped lambda calculus.
Take for example the inductive definition of lists, with introduction rules:
and:
We can ...