4
votes
2answers
146 views

Question about higher inductive types and computational rules

I have been trying to make my way through the homotopy type theory book, slowly but surely, and I just finished reading this introductory series of 3 articles on hott on ScienceForAll. ...
12
votes
3answers
438 views

Formal/rigorous treatment of (im)predicativity/predicativism

There are several places on the web where one may find quite intuitively understandable accounts of (im)predicativity; here on MO I found two questions with very good detailed answers (Predicative ...
5
votes
2answers
460 views

Why is there no product type in simply typed lambda-calculus?

Consider simply typed $\lambda$-calculus that has only the unit type as primitive. We would like to encode the product and the sum types. An encoding of the product type in the untyped ...
6
votes
1answer
250 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
2answers
860 views

A (very naive) question about Homotopy Type Theory

In homotopy type theory, homotopy types can be viewed as logical types and it is possible to prove some theorems about them without using any underlying space (no simplicial set, no topological ...
16
votes
2answers
856 views

Prospects for reverse mathematics in Homotopy Type Theory

Reverse mathematics, as I mean here, is the study of which theorems/axioms can be used to prove other theorems/axioms over a weak base theory. Examples include Subsystems of Second Order Arithmetic ...
5
votes
0answers
151 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 ...
8
votes
2answers
723 views

Equivalent form of the Univalence Axiom

I'm reading the new HoTT book and I'm wondering about a potential equivalent form of the Univalence Axiom: $(A \simeq B) \simeq (A = B)$. For simplicity, I'm tacitly working in a fixed universe. It ...
5
votes
2answers
346 views

Connection between codata and greatest fixed points

This is, I'm afraid, another question that MSE couldn't answer. It's easy to see how inductively-defined data types correspond to least fixed points. Let's take the natural numbers as an example, ...
10
votes
1answer
1k views

Forcing in Homotopy Type Theory

I apologize if this question doesn't make any sense. I'll just go ahead and delete it if that's the case. But the question is just the title. Is there a notion of forcing in homotopy type theory? ...
9
votes
2answers
562 views

Category of Judgements?

I have been able to find a lot of information on the category of contexts -- for example, the page on syntactic categories at the nLab is a good starting point. However, when I try to find similar ...
4
votes
1answer
496 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
6
votes
2answers
272 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 ...
8
votes
2answers
308 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 ...
5
votes
1answer
907 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 ...
4
votes
1answer
449 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 ...
-1
votes
5answers
793 views

finding cutting edge papers and books

Hi all, what are the best strategies to find cutting edge papers and books on a field of mathematics? .. Example: 2-3 years ago I had to analyze a time series. I found a paper and showed that to ...
4
votes
3answers
479 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 ...
2
votes
1answer
248 views

Relation between different definitions of types [closed]

Is there any connection between the definition of type in model theory and the definitions from type theory? Is there any explanation why the same term is used for these notions, maybe in the ...
6
votes
4answers
658 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 ...
10
votes
2answers
1k views

What is the manner of inconsistency of Girard's paradox in Martin Lof type theory

I am aware that assigning the type of Type to be Type (rather than stratifying to a hierarchy of types) leads to an inconsistency. But does this inconsistency allow the construction of a well-typed ...
6
votes
4answers
727 views

Can dependent sums be encoded as dependent products?

Please forgive any unorthodox notation or obvious errors here... I'm trying to get an intuition for dependently typed languages, so I'm starting out by seeing which analogies I can take from the ...
3
votes
1answer
406 views

What notions of universe does predicative type theory admit?

Palmgren (1997), On universes in type theory, discusses work of several theorists that provide what we might call a family of Large Universe Axioms (LUAs) for predicative type theory, culminating in ...
6
votes
2answers
626 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 ...
12
votes
7answers
2k views

What is lambda calculus related to?

So I'm not much of a math guy but I've really enjoyed programming in Lisp and have become interested in the ideas of lambda calculus which it is based. I was wondering if anyone had a suggestion ...