# Questions tagged [type-theory]

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

262 questions
Filter by
Sorted by
Tagged with
130 views

### What's the point of stack judgement in CBPV?

Call-by-push-value (CBPV) introduces two main families of types, values and computations, and their corresponding judgements. However, in some extensions/variants/adaptation of CBPV, there is a third ...
219 views

### Fixed set of type constructors to simulate all intensional inductive families?

I'm wondering, are there small dependent calculi that can simulate a language with inductive families (that is, has a type isomorphic to each inductive family, at least as powerful of induction ...
71 views

### Is System-F with higher-kinded newtypes equivalent in computational power to System-F omega?

If we have System-F with higher-kinded types and newtypes, then we can express everything (I think) of System-F omega, except we have to manually (un)pack. For example: ...
152 views

### Structural equality of Pi Types with heterogeneous equality?

I'm trying to implement a proof of the following type: ...
56 views

### Diagram of relations between different branches of mathematical logic and type theories

There are many forms of various mathematic logics, lambda-calculus, satisfiability modulo theories, category theories, type theories, including HoTT and Cubic HoTT, and so on. Lambda cube is a famous ...
160 views

### Is my understanding regarding how to implement Quotient Types correct?

I was trying to understand Quotient Types, and determine if Self-Types can be used to implement them. From a Reddit post, Here is an example and explanation that may be more familiar to non-...
3k views

### Prove proof irrelevance in Coq?

Is there a way to prove the following theorem in Coq? Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2. EDIT: An attempt to give a brief ...
177 views

### Type-theoretic interpretation of Skolemization

What is the type-theoretic interpretation / equivalent of Skolemization? Skolemization converts some formula into Skolem normal form. The two formulae are equisatisfiable with each other. Or, to say ...
151 views

### Model of Coq (pCuIC) in higher toposes?

Can the type theory of Coq (pCuIC) be modeled in all higher Grothendieck toposes? First of all, even the set theoretical model is not complete (e.g. inductive types in Prop). Although, this is ...
110 views

315 views

440 views

### Proof techniques for showing that dependent type checking is decidable

I'm in a situation where I need to show that typechecking is decidable for a dependently-typed calculus I'm working on. So far, I've been able to prove that the system is strongly normalizing, and ...