Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [type-theory]

For questions about type theory, including normalization, dependent types, identity types, inductive types, universe types, functional programming languages, proofs as programs in simply-typed lambda-calculi, Martin-Löf's intuitionistic type theory or related.Consider using one of the following tags: (lambda-calculus), (logic), (constructive-mathematics),(homotopy-type-theory) if related.

2
votes
1answer
41 views

Is (co)product is a bifunctor?

I am learning category theory from Bartosz's blog, where he mentioned that: If the product exists for any pair of objects, the mapping from those objects to the product is bifunctorial. Based on ...
0
votes
1answer
60 views

What does type constructor in type theory correspond to in category theory?

If types themselves correspond to object or for example Unit type corresponds to terminal object, then what does type constructor correspond to in a category?
2
votes
1answer
32 views

Can we convert existential sentences into functions?

I am trying to grasp the basic ideas of type theory. I understand that universally quantified propositions can be considered as functions, which maps terms to "proof objects". Hence a proposition $$\...
0
votes
1answer
23 views

How to define inferiority relation on natural numbers in a dependently typed lambda-calculus?

Girard's System F have the following definition for natural numbers : $$ \mathbb N := \forall\alpha, (\alpha\rightarrow\alpha) \rightarrow (\alpha\rightarrow\alpha) $$ A dependent type system can ...
0
votes
0answers
50 views

Why is the calculus of constructions called that way, and what is a “construction” in CoC?

I'm reading about the calculus of construction Nederpelt & Geuvers' book "Type theory and formal proof". I can see that CoC allows us to extend the curry howard isomorphism from simply typed ...
3
votes
1answer
95 views

Can we prove the Peano axioms from a type theoretic construction of the natural numbers?

Here are two quotes that, while not literally contradictory, reach conclusions that are opposite in spirit. The first one states that the Peano axioms can be proven to hold for an explicit ...
5
votes
2answers
45 views

Difference between $\lambda$-$\mu$-calculus and intuitionistic type theory + LEM for classical proofs?

I have some experience with using type theory to do proofs in intuitionistic logic. If I want to prove theorems that require classical logic, I simply pose the law of excluded middle (LEM) as an axiom....
8
votes
1answer
59 views

Comment about type theory in Lawvere and Rosebrugh's Sets for Mathematics

The Foreword to Sets for Mathematics (second section, titled Organization) contains the following comment, about the differences between ETCS and other foundations of mathematics: Each map needs ...
1
vote
1answer
43 views

Relation of self-application to non termination in the untyped lambda calculus.

I was reading the following question: Self-application in Church's untyped lambda calculus First, we can have terms which, if applied to themselves, still have normal form. For example, $(\lambda ...
0
votes
0answers
46 views

How does $\neg \phi$ as $\phi \to \textbf{false}$ fit in intuitionist philosophy?

In intuitionist type theory that I know, $\neg \phi$ is interpreted as a function that takes a proof of $\phi$ and outputs a proof of false. It seems to me that this is different from the way that ...
1
vote
1answer
55 views

Difference between proof of negation vs proof by contradiction in practice?

This article explains the difference between proof of negation and proof by contradiction, and this question has asked for a clarification. I understand the difference in the abstract. If we don't ...
0
votes
1answer
39 views

Is expression evaluated before assigning type?

I am assigning type to an $\lambda$-expression: if false then M else N where if A then B else C and ...
1
vote
0answers
52 views

Type theoretic counterpart of calculus of constructions?

The Curry-Howard correspondence connects the simply typed calculus with proofs in propositional intuitionistic logic. This correspondence can be extended between System F (polymorphic typed calculus) ...
2
votes
1answer
48 views

Algebraic transformation for dependent type

One can make the following type algebraic transformation (where $=$ means isomorphic and $\equiv$ means syntactically equal): $$ X * (X \to X) \;\; \equiv \;\; X * X^X = \\ X^{(1+X)} \;\; \equiv \;\; (...
6
votes
1answer
90 views

Higher inductive type: what for?

The typical example of higher inductive type (HIT) is the circle $S^1$ that is nicely described here. I understand HITs are convenient if you want to do homotopy theory within type theory. But what ...
1
vote
1answer
35 views

Transporting via an identity type when inducting along the higher inductive type $S^1$

I am reading the HoTT book https://hott.github.io/book/nightly/hott-online-1198-geeccc59.pdf and my question is regarding page 281, where the book says: When $x$ varies along loop, we need to prove ...
2
votes
1answer
62 views

Why should we adopt the cumulative universe convention?

In various sources on intuitionistic type theory, the universe of types is taken to be cumulative, i.e. $A:\mathcal U _i$ implies $A:\mathcal U_j$ whenever $i\le j$. The question is: why do we have ...
1
vote
0answers
43 views

Construction of Rational Numbers without quotients

The context is Intensional Type Theory, where quotients are unavailable. I managed to construct Integers in this way: $\mathbb{Z}:=(\mathbb{N}^+\times\{{+,-\}})+\{{0\}}$, but I can't see a way to ...
7
votes
0answers
156 views

Natural transformation = parametric polymorphic function in “structure categories”?

By a “structure category” I mean a concrete category that contains as objects all spaces of a particular type of structure, and as morphisms, functions that preserve that type of structure. I.e. the ...
0
votes
0answers
25 views

Formulating concepts from synthetic geometry in constructive type theory.

Constructive Type Theory (CTT) is much closer in structure to informal mathematical thinking than, say, first-order predicate logic is. There are some examples of formalizing e.g. Euclidean proofs in ...
1
vote
1answer
73 views

Can we see all mathematical concepts as (possibly uncountable-time) algorithms?

Note: I am interpreting “algorithms” broadly, to include algorithms that require an infinite and even uncountable number of computational steps. It seems to me that any definition can be seen as a ...
1
vote
0answers
43 views

“Type dependence” in type theory and category theory?

I will distinguish between mathematical functions and computational functions which I will think of for concreteness as $\lambda$-functions. In every context I’ve encountered, the type signature of a ...
2
votes
2answers
53 views

Do type constructors have type themselves?

I'm recently trying to understand the basics of intuitionistic type theory, and I think I have grasped much of it. However, there is this question on my mind. For instance, can the type constructor $\...
0
votes
0answers
31 views

Type Theory without “free variables”. Is it feasible? Is it useful?

Personally, I've always found free variables to be unintuitive, and they force many rules to have lots of edge cases. Is it possible to construct a theory without free variables, i.e. a theory which ...
2
votes
1answer
77 views

Formal definition of “equivalence” between two formalizations of a theory?

Normally, I think of an isomorphism between two structures as requiring they have the same signature. E.g. two structures $(A,\cdot)$ and $(B,+)$ where $\cdot: A\times A\to A$ and $+:B\times B\to B$ ...
2
votes
1answer
71 views

In HoTT, does $\prod_{T : \mathcal{U}} T \to T$ have only one element?

In Homotopy Type Theory, I can define $id : \underset{T : \mathcal{U}}{\prod} T \to T$ by $id(T, t) \equiv t$ But, are there any other elements of $\prod_{T:\mathcal{U}}T \to T$ ? I have been able ...
1
vote
0answers
57 views

Induction over HIT (HoTT)

Setting Currently I try to formulate the simply typed $\lambda$-calculus in HoTT which results in quite involved inductive type families. Since I'm still new, I'm often unsure if my induction ...
18
votes
2answers
929 views

Has a conjecture ever originally been decided by constructing the proof with mathematical logic?

So, one of the things that mathematical logic does is study theorems as abstract objects. There also many theorems about mathematical logic, and these theorems can have connections to other fields. ...
1
vote
0answers
58 views

Encoding the existence of an element of a type for which there exists some proof of irrelevant contents

I'm studying encoding math (and sets in this particular case) in the calculus of constructions. So let's say there are types $S, T$ (so $S : *, T: *$), a predicate $V : S \rightarrow *$ and a function ...
1
vote
0answers
78 views

If circular type definitions are valid

I am confused about type hierarchies in programming languages, which seem to be limited to 2 layers for some reason. This got me wondering if circular reasoning in regards to types is a logical ...
0
votes
0answers
42 views

What does the first “non-free” variable mean here when substituting in simple type theory?

See this screenshot of the book "Basic Simple Type Theory". The infinite sequence they refer to is just a way to formalize the concept of having enough variables to work with no matter what. In my ...
1
vote
0answers
63 views

Expressing subsets in the calculus of constructions

The book I'm reading on the calculus of constructions suggests to treat subsets in the following way. Let's fix some type $S$ as representing the whole set of interest, and express a subset $V \...
0
votes
1answer
34 views

Proving equality is reflexive in Q0 (equality-based formulation of type theory)

The SEP has a nice article on Church's Type Theory, and in it they discuss Peter Andrews' equality-based formulation of type theory called Q0: https://plato.stanford.edu/entries/type-theory-church/#...
6
votes
2answers
234 views

Axiom checking as type checking?

There is a connection between type theory and logic, where types are propositions, and type checking performs the role of checking whether a proof of a proposition is correct (Curry-Howard isomorphism)...
0
votes
1answer
37 views

Proving certain obvious tautologies in the calculus of constructions

I'm trying to prove that $\lnot (\exists y : S.Py) \rightarrow \exists y : S. \lnot Py$ (let me know if the encoding of $\exists$ matters!). I don't have any good ideas about how to do that, but I've ...
2
votes
0answers
53 views

Distinction between a “strictly typed function” and a “not strictly typed function”?

Let $f$ be the identity function for the real numbers. In the vernacular, we'd say that $f$ is a function from reals to reals, or that $f:\mathbb{R}\to \mathbb{R}$. Let $g$ be the inclusion map ...
0
votes
1answer
33 views

C-like type declaration.

In most math books declaring an object along with its type is done with the type after a colon after the object, and the definition of this object is done in another expression. E.g. $$ \begin{align} ...
0
votes
0answers
35 views

What is the name of a coinductive type defined with a total order relation?

In type theory, is there a name for a coinductive type simply defined with a successor operator and an equivalence relation? And what would be the name of such a type if it were defined with a total ...
3
votes
0answers
40 views

Type equivalence in $\lambda\underline\omega$ under lambda abstraction

I'm going through "Type Theory and Formal Proof" by Nederpelt and Geuvers and just trying to play around with $\lambda\underline\omega$ after reading the chapter on it to better grasp the material. ...
2
votes
2answers
69 views

Properties over partly specified inductive families (HoTT)

At the moment I'm about to get my head around homotopy type theory as a new perspective into mathematics. Insofar, I'm trying to mess around with it, prove some simple things and see where it gets; ...
1
vote
1answer
144 views

Intuition for Diaconescu's theorem

Diaconescu's theorem proves that the axiom of choice implies the law of the excluded middle. While I can follow the proof in the above wikipedia article, it just seems like a cheap trick, so to ...
1
vote
0answers
52 views

Prospects of teaching/learning elementary math with computed-checked type theory

I've read as much as I can understand about type theory and homotopy type theory (HoTT) and it seems like these are very promising directions for re-foundationalizing mathematics in a way where ...
2
votes
1answer
133 views

What would synthetic linear algebra look like?

I'm aware of synthetic mathematical fields like synthetic differential geometry and synthetic topology where the area is developed axiomatically rather than deriving everything analytically from a ...
2
votes
1answer
59 views

Universal quantifiers in category theory

I’ve recently learned about the curry howard isomorphism for dependent type theory, and I’m now interested in learning about how to capture this in category theory. I believe that I understand how to ...
0
votes
1answer
40 views

Introduction to categorical logic and CHL-correspondence?

My motivation for this question is that I’m interested in using categorical logic/category theory to intuitively visualize and think about proofs in advanced type-theory based proof-assistants like ...
1
vote
1answer
93 views

Different descriptions of internal languages of a topos

I wanted to learn more about the internal language of of toposes and to do so I have been reading both Sheaves in Geometry and Logic (Sheaves) by Mac Lane and Moerdijk and Introduction to Higher Order ...
3
votes
0answers
65 views

Model for the type-theoretic axiom of choice in Coq.

This is the request for references. It is a known fact that there is a model of ZFC in ZF, so ZFC is consistent if ZF is consistent. It is also know that there is a double-negation Godel-Gentzen ...
4
votes
0answers
69 views

Products are to Cartesian multicategories as exponentials are to what?

Section 2 of this draft by Mike Shulman explains how Cartesian multicategories are able to directly internalize the structural rules of simple intuitionistic type theory as it is usually presented, ...
4
votes
1answer
295 views

Can the axiom of choice be explicitly proved in (intuitionistic) predicate logic, or is something like intuitionistic type theory necessary?

In intuitionistic mathematics, an axiom of choice of the form $$ \forall x \exists y R(x,y) \rightarrow \exists f \forall x R(x, fx) $$ is valid by the meaning of the quantifiers (comp. Dummett, ...
1
vote
1answer
93 views

Questions on the “free functor” functor

I have recently found out that in Haskell we can to turn a type constructor into a functor, using the "free functor" construction [1, 2, 3]. I would like to understand this construction – the free ...