Questions tagged [type-theory]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
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 ...
Russell O'Connor's user avatar
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 ...
Mike Shulman's user avatar
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 ...
Peter Gerdes's user avatar
  • 2,551
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 ...
Daniel Barter's user avatar
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 ...
ಠ_ಠ's user avatar
  • 5,933
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 ...
Colin McLarty's user avatar
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 ...
RAC's user avatar
  • 83
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 ...
StudentType's user avatar
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 ...
Pace Nielsen's user avatar
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 ...
kittyphon's user avatar
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 ...
Guillaume Brunerie's user avatar
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 ...
Ronald J. Zallman's user avatar
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\...
Christoph-Simon Senjak's user avatar
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-...
H Koba's user avatar
  • 369
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$ ...
Anton Fetisov's user avatar
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 ...
Zhen Lin's user avatar
  • 14.9k
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$,...
Arshak Aivazian's user avatar
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 (...
mfddnjk2'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,675
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 ...
efk's user avatar
  • 193
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 \...
goblin GONE's user avatar
  • 3,693
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 ...
Max New's user avatar
  • 785
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 ...
Manuel Bärenz's user avatar
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 ...
user40276's user avatar
  • 2,199
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 $\...
Matthew's user avatar
  • 303
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 ...
João Alves Jr.'s user avatar
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:...
Mike Shulman's user avatar
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 ...
François Jurain's user avatar
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 ...
EBP's user avatar
  • 85
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 : \...
Mario Román's user avatar
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
user avatar
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 ...
Sergey Melikhov's user avatar
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 ...
Mike Shulman's user avatar
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 ...
GeoffChurch's user avatar
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 ...
rfloc's user avatar
  • 473
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 ...
Nico's user avatar
  • 775
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 \...
Matteo's user avatar
  • 71
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 ...
Paolo Capriotti's user avatar
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 :...
Trebor's user avatar
  • 1,021
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 ...
ಠ_ಠ's user avatar
  • 5,933
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 ...
wlad's user avatar
  • 4,823
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 ...
Kaveh's user avatar
  • 5,362
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-...
Russell O'Connor's user avatar
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 ...
Christopher King's user avatar
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 ...
Spaceka13'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
  • 699
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 ...
Twey's user avatar
  • 121
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\,\...
George Cherevichenko's user avatar
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 ...
meditans's user avatar
  • 243