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.

1
vote
1answer
25 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 \;\; (...
5
votes
1answer
70 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
33 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
56 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
36 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 ...
4
votes
0answers
39 views

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

By “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
22 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
0answers
50 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 ...
0
votes
0answers
28 views

Type dependence and equivalence vs equality of categorical morphisms?

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
50 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
30 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 ...
1
vote
1answer
58 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
69 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
52 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
908 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
57 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
41 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 ...
0
votes
0answers
26 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
230 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
36 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
52 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
37 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
62 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
139 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
50 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
110 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
44 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
34 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
88 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
61 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
67 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
287 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
84 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 ...
0
votes
0answers
32 views

Closure of a constant

Consider a type $T$, and a set $S$ containing elements of type $T$. An object $f$ of type $T→T→T$ (or $T^2 → T$) is a function and it is closed under $S$ if any two elements of $S$ applied to $f$ ...
2
votes
1answer
99 views

Examples of the categorical interpretation of dependent types

I'm trying to understand the correspondence between dependent types and category theory. Let me tell you about my current (I admit, limited) knowledge on the two topics.....
5
votes
0answers
206 views

Is many sorted logic really a unifying logic?

I am reading "Extensions of First Order Logic" by Maria Manzano (1996). It develops the thesis that "[M]ost reasonable logical systems can be naturally translated into many-sorted first order ...
2
votes
1answer
91 views

Can we prove that the peano axioms are true for $(\mathbb N, \sigma)$ in type theory?

In mathematical logic that I'm used to (i.e. we have first-order formulas and a sequent calculus to derive formula's from axioms), we never prove that the peano axioms are true for the natural numbers,...
1
vote
0answers
63 views

The continuation passing style transformation in the lambda calculus

I have an issue understanding the following definition (from https://tel.archives-ouvertes.fr/tel-00783245/document , p.82) of the continuation-passing style (CPS) transformation in the lambda ...
0
votes
0answers
52 views

Determining type of composed function

We would like to know the type of the function composition $f \circ f$. The function in question is typed as follows: $f :: (\alpha \rightarrow \beta \rightarrow \gamma) \rightarrow (\alpha \times \...
2
votes
1answer
72 views

How to construct quotient sets (types?) in Martin-Löf type theory

I think there is no formation rule for quotient type. How to construct quotient set in Martin-Löf type theory?
1
vote
1answer
85 views

In HoTT, if $A$ and $B$ are both sets, then $A=B$ is a set

In the HoTT book, it is mentioned that if $A,B$ are sets, then so does $A=B$ of paths between $A$ and $B$. Could someone tell me about how to prove this, please? Thank you. With the help of the ...
0
votes
1answer
88 views

Can an entity has more than one type?

I think that 1 is natural number and real number, so $1:\mathbb{N}$ and $1:\mathbb{R}$. In type theory, can an entity has more than one type?
2
votes
1answer
63 views

Does/has type theory influenced how to treat functions as values?

Does/has type theory influenced how to treat functions as values? Particularly, I still believe that it's general to think of functions with some input, e.g. $f(x)=x$ to be the value of the function, ...
1
vote
1answer
112 views

Existence of Natural Numbers as an Axiom

By natural numbers $\mathbb{N}$ I understand any set satisfying Peano axioms: $0 \in \mathbb{N}$ $\sigma : \mathbb{N} \to \mathbb{N}$ $\forall n \in \mathbb{N} \; . \; \sigma(n) \neq 0$ $\forall n,m \...
1
vote
0answers
50 views

definitional extension vs. $\lambda$-abstraction

Let $\mathcal{L}$ be a first-order language in signature $\Sigma$ and $\mathcal{L^+}$ an extension of $\mathcal{L}$ in a richer signature $\Sigma^+$. An $\mathcal{L^+}$-theory $T^+$ is a definitional ...
1
vote
0answers
28 views

Is the converse of the Liskov principle true? if not give a counter example

As I understand the Liskov Substitution Principle, it says that if $A\subset B$ and $X \subset Y$ then $(B\to X) \subset (A\to Y)$. I'm having trouble understanding what the converse of this ...