# Questions tagged [type-theory]

Type structure is a syntactic discipline for enforcing levels of abstraction.

364 questions
Filter by
Sorted by
Tagged with
175 views

### What is the computational power of the Calculus of Constructions?

The calculus of constructions (CoC) without fix is clearly not Turing complete, as the program that loops infinitely cannot be expressed in it. What I'm wondering: ...
64 views

### Question about "Free-ness" of Free SCWF

In Category with Family by Castellan et al., they introduce the concept of Free SCWF as correspondence of STLC with base type. Seemingly, they define Free B-SCWF as the synonym of initial B-SCWF. My ...
1 vote
45 views

### Question in relating STLC and Free CCC

In Lambek's Intro to Higher Order Cat Logic, Chapter 1 Section 4 introduces the free construction (upon graph) My question is, if I want to have STLC + (fake/incomplete) boolean type, how do I have ...
116 views

### Boolean logic: What is the name of this trick to replace explicit negations by implications?

Consider a Boolean circuit $C$ composed of some finite set of input variables $A_1,\ldots, A_n$ and the connectives $\lor\land\neg\rightarrow$ (with $X\rightarrow Y=\neg X\lor Y$) (update: assume that ...
75 views

### Type theory: Eliminating callback functions?

Consider a type theory such as the one developed in Chapter 1 of the HoTT book, or similar. In fact, I am currently only interested in the types that can be constructed from a collection of elementary ...
40 views

### What does impredicativity mean in substructural and co-intuitionistic logics?

Predicative foundations puts restrictions on power sets and function sets. Entirely apart from the philosophy predicative theories are a lot easier to prove things about and this sounds interesting to ...
154 views

### How do we use directed univalence in directed type theory?

In directed type theory of Riehl and Shulman, we have a new type, $hom_A\:x\:y$ representing arrows between elements $x$, $y$ of type $A$, note that these are not a priori functions. I will call the ...
127 views

### Is there a way to define dependent types without explicit substitutions internally within agda?

I am playing around the Programming Language Foundations in Agda exercises and wondering if we can achieve the same level of theories with dependent types. With simple types, the definition usually ...
447 views

### Induction-recursion in models other than $\mathbf{Set}$

It is well-known that various flavors of induction-recursion are consistent*. Typically, this is proven by showing that the standard model of type theory in sets can be extended to include induction-...
651 views

### What's the logical counterpart to jumps with arguments on CPS terms?

It's well known that the CPS (continuation-passing style) translation often employed in compilers corresponds to double negation translation under the Curry-Howard isomorphism. Though often the target ...
113 views

### For which type systems have normalizaton proofs been formalized?

I am trying to understand what the open problems are in the area of formalizing proofs of normalization for type systems. Obviously STLC has been done many times. For predicative System F, I found one ...
Pattern unification is a simplified form of higher-order unification in which existential variables only appear applied to distinct universal variables. Thus, for instance, an equation such as $M \,x\... 10 votes 2 answers 393 views ### What are the issues with a set-like interpretation of quantifiers in type theory? In his answer to a question that tries to treat universal and existential quantifiers as intersections and unions of sets, Andrej Bauer says: Forget the intersections and unions. People get this idea ... 8 votes 4 answers 278 views ### Type theory and fixed points of datatypes For the purposes of this question, say that a datatype is a type constructor with one type parameter (this is sometimes called a type operator). In Haskell, we can define a fixed point ... 0 votes 0 answers 138 views ### What is wrong with the "obvious" approach to function extensionality by providing context-aware rewrites? There is an obvious, dirty and probably wrong approach that allows one to prove function extensionality in a straight-forward manner: provide an equality primitive with a context-aware rewrite. For ... 7 votes 1 answer 319 views ### Which universities in the U.S. are doing research in type theory? The question is meant to be broad in that recommendations with mentions of the particular areas within type theory research are greatly appreciated. Also, the research need not be conducted in ... 4 votes 1 answer 166 views ### Effect of HoTT/Univalence Axiom on equality between terms of inductive types? It is well known that Univalence contradicts Axiom K, for example there are two ways$\mathbf{2} = \mathbf{2}$may be proved using Univalence, via$\mathtt{id}_{\mathbf{2}}$or$\mathtt{not}$. But ... 9 votes 2 answers 394 views ### Why is the Curry-Howard isomorphism? The Curry-Howard isomorphism is the correspondence between type systems (like for the simply typed lambda calculus) and proof systems (like natural deduction). More precisely, types resemble ... 6 votes 1 answer 167 views ### What is the general definition of 'extensionality' in type theory and how is extensionality defined for positive types? It is well-known in the literature that (internal) extensionality of a function type means$(\prod_a f~a=g~a)\implies f=g$(where$=$is the intensional equality type) and extensionality of a product ... 3 votes 2 answers 262 views ### How does axiom K contradict univalence? I have seen it claimed several times that axiom K is inconsistent with univalence (e.g. here and here), but I have never seen a proof sketch. Specifically, I'm curious about how this manifests in the ... 1 vote 1 answer 98 views ### Are coproduct types redundant in presence of natural numbers and$\Sigma$-types? In the homotopy type theory book section A.2.5 defines$\Sigma$-types, A.2.6 coproduct types and A.2.9 the natural numbers type. If we already have$\Sigma$-types and the natural numbers type can we ... 7 votes 0 answers 172 views ###$\lambda$-definability and structure preserved by homomorphisms I imagine there are some standard results that bear on this, but I'm having trouble finding a proof or refutation of it. Some prelimary definitions. A Henkin structure$A = (A^\cdot, ⟦\cdot⟧_A)$for ... 8 votes 2 answers 359 views ### What's the categorical semantics of definitional equality? The categorical semantics of a dependent type theory is normally described as a CwA/CwF/CompCat/etc. and in these models, we can talk about propositional equality by interpreting an 'identity type'. ... 6 votes 3 answers 1k views ### How does type theory change how one thinks about programming? I have been dabbling in HoTT and I am convinced that dependent type theory is much more suitable than set theory for proof assistants. Now, this made me wonder - how fundamental is Type Theory ... 2 votes 2 answers 186 views ### What is the point of the eliminator for the unit type? In the HoTT book p. 436 A.2.8 the eliminator$\mathrm{ind}_{\mathbf{1}}$for the unit type is described. What is the point of it? What if you did not introduce it and instead just replaced all the ... 5 votes 1 answer 120 views ###$\eta$-reduction not locally confluent on well-typed terms This paper says: "In the presence of a unit type,$\eta$-reduction is not even locally confluent on well-typed terms ."  is a reference to a 300-page book with no further details and ... 2 votes 0 answers 70 views ### Reference request: characterisation of simultaneous substitution For simply typed λ-calculus, a simultaneous substitution from$\Gamma$to$\Delta$is concretely a type-preserving map from variables in$\Delta$to terms in$\Gamma$. See, for example, Programming ... 9 votes 0 answers 175 views ### Constructive Strong Normalization of the Extended Calculus of Constructions The extended calculus of constructions (ECC) is basically the calculus of constructions with cumulative universes. I use the definition which Zhaohui Luo used in his PhD theses which contained a proof ... 3 votes 1 answer 155 views ### How to think about comp in cubical type theory Consider the definition: ... 2 votes 1 answer 104 views ### External failure of law of excluded middle in Martin-Löf type theory Is there an explicit type$T$in Martin-Löf type theory such that$(T\to \mathbf{0})\to\mathbf{0}$has an explicit closed term and$T$can be shown externally to not have closed terms? 1 vote 0 answers 91 views ### CubicalTT: successor of add proof? Lecture 2 of the cubical type theory lectures provide a proof of (suc a) + b = suc (a + b): ... 2 votes 0 answers 78 views ### MLTT/MiniTT: why do normal forms of sum types carry environments? I am learning how to implement MiniTT: a simple type theoretic language, which is a dependently typed language with sum types, mutual recursive/inductive definitions and a universe of small types. A ... 6 votes 1 answer 209 views ### What are the pros and cons for type cases in dependent type theories? Pattern matching on$\cal U$is allowed in XTT and Idris2 (for unerased types), and that implies the injectivity of type constructors (that's just my intuition, though -- I also wonder how do I prove ... 2 votes 2 answers 458 views ### Does univ : univ always lead to a contradiction in a dependently typed language? I am currently following Checking Dependent Types with Normalization by Evaluation: A Tutorial by David Christiansen, where we consider the type of U (the universe ... 2 votes 1 answer 187 views ### Alternatives to Normalization by Evaluation Reading about lambda calculus I got the impression that normalization is evaluation. So I don't understand what is meant by Normalization by Evaluation (used e.g. in several publications of A. Abel). ... 3 votes 0 answers 88 views ### Equality reflection without$\eta$Are type theories with equality reflection (i.e. having a term of an identity type between two objects allows us to freely swap them) but not the$\eta$-rule for$\Pi$-types interesting? Does function ... 3 votes 2 answers 406 views ### What technique is used to implement type checking for CoC? I am studying David Christiansen's tutorial on implementing a dependently typed language, where it says: Typed normalization by evaluation is far from the only way to implement conversion checking ... 11 votes 1 answer 672 views ### Why is regularity a problem in cubical type theory? In my current understanding, regularity in cubical type theory is the following definitional equality (I'm using$A~\textbf{type}$to emphasize the fact that$i \notin FV(A)$): $$\cfrac{A~\textbf{... 5 votes 1 answer 129 views ### Definitional function extensionality for functions out of \mathbf{2} Denote by a and b the canonical terms of \mathbf{2}. For any map f:\mathbf{2}\to \mathcal{U} we have the eliminator$$\mathrm{ind}_{\mathbf{2}}(f) : \big(f(a) \times f(b)\big) \to \prod_{x:\... 0 votes 2 answers 97 views ### Pi-type over a list in dependent type theory In a formalization I need to create an inductive type which has a term for each element in a list, something like this (I'll use Agda in the following, but everything here is standard dependent type ... 3 votes 1 answer 163 views ### Are uniqueness rules converse to introduction rules? I've seen many people connecting introduction rules and elimination rules, saying that they're dual notion. Indeed, like in the categorical model, these rules are symmetric morphisms. However, if we ... 0 votes 1 answer 103 views ### Reference for context-free grammar for Martin-Löf type theory Are the terms and the types of Martin-Löf type theory described by context-free grammars? Have such grammars been written down somewhere? 3 votes 0 answers 89 views ### Boltzmann sampling for containers/dependent polynomials? I’d like to randomly sample from dependently-typed data structures. Has anyone looked at extending Boltzmann sampling to containers or dependent polynomials? 3 votes 1 answer 235 views ### Is just one W-type enough for formalizing mathematics? We work in intensional Martin-Löf type theory with$0$,$1$,$2$,$\Pi$,$\Sigma$,$W$and a cumulative hierarchy of universes. Suppose our goal is to formalize constructive mathematics. Now if we ... 2 votes 0 answers 151 views ### Set-theoretic encoding of functions in type theory Functions usually get encoded in set theory as follows. A function$A\to B$is a subset$f\subset A\times B$such that$\pi_1:f\to A$is a bijection. In type theory to give a function$A\to B$is to ... 2 votes 1 answer 125 views ### Dependent eliminator for empty type in intensional Martin-Löf type theory In calculus of inductive constructions you can just say that the empty type is the type with no constructors and it automatically builds the dependent eliminator. But let's say I'm setting up ... -1 votes 1 answer 100 views ### How much type information do Hindley-Milner proof assistants need to remain sound? A known benefit of the HM type system is that you can usually infer a term's most general type with no user-provided type annotations. For example, if my theory contains the standard axiom:$$\forall ... 1 vote 2 answers 147 views ### Explicit type system with infinite non-cumulative universe hierarchy Is there an open-source proof assistant or at least an explicit set of rules written down somewhere for a type system with an infinite non-cumulative universe hierarchy and unique typing? I want to ... 2 votes 0 answers 88 views ### What is the relation of parametricity and function extensionality? In Agda function extensionality can be defined like this: funExt = {A : Set} {B : Set} {f1 f2 : A → B} → (∀ x1 x2 → x1 ≡ x2 -> f1 x1 ≡ f2 x2) → f1 ≡ f2 One may ... 2 votes 2 answers 141 views ###$\mathbb{N}$in intensional MLTT with judgmentally commutative$+$and$\times\$ 