Stack Exchange Network

Stack Exchange network consists of 174 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.

0
votes
1answer
30 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
33 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
33 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. ...
1
vote
2answers
52 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
126 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
46 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
96 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
37 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
29 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
86 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
53 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
59 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
272 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
75 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
26 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
95 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
186 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
84 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
55 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
51 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
68 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
71 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.
0
votes
1answer
59 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
62 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
102 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
48 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 ...
3
votes
0answers
93 views

Internal equality for Eq-fibrations

In Jacob's Categorical logic and Type Theory in relation to fibrations with equality the author gives the following definition: ...call two morphisms of Eq-fibrations $(K,H),(H',K') \colon p \to q$ ...
3
votes
1answer
116 views

Is an applicative functor determined by its application operator?

Let $\cal C$ and $\cal D$ be cartesian closed categories, which I will treat type theoretically (i.e. the objects are called types, and $A\to B$ is the exponential object; lambda terms like $\lambda x ...
2
votes
0answers
91 views

Is a dependent type just a vector of types?

You could think of a k-vector of integers as a function of type $\mathbb{Z}/k \to \mathbb{Z}$, associating each member of $\mathbb{Z}/k$ with a single member of $\mathbb{Z}$. Similarly, a dependent ...
10
votes
1answer
109 views

Are there important locally cartesian closed categories that actually are not cartesian closed?

In some (but not all) of the published definitions, a locally cartesian closed category is any category with all its slices cartesian closed. Such a category need not be cartesian closed itself, ...
4
votes
2answers
214 views

Curry-Howard for an imperative programming language?

The Curry-Howard isomorphism links proofs of propositions, with "programs" and types. But the way I am introduced to it, "programs" is interpreted in a functional way, i.e. in lambda calculus with ...
0
votes
1answer
65 views

How do you define in particular a linked list in abstract type theory? Or would you even do that?

I understand somewhat how abstract List is defined. But still not 100%. Type theory literature is not that great yet. I want to know how to build basic data ...
0
votes
1answer
45 views

Would this suffice in a visual type theory to define an abstract List type?

See the image. I got that from: wikipedia article. In that, I don't understand the first function nil : () -> L. What is ()...
2
votes
1answer
38 views

Definition Of Equivalence

I'm reading this paper on the univalence axiom and I'm stuck with the following definitions: Maybe my thinking is still too much grounded in set theory, but let's say $f$ is the identity on $\{0,...
1
vote
1answer
81 views

Can all classical math proofs be represented in type theory?

The curry howard isomorphism states that proofs in intuitionist logic can be represented as terms, and theorems as types. However, I'm wondering: if we add the classical logical axioms like LEM (and ...
2
votes
0answers
84 views

Interdefinability of set, type and category theories [closed]

There seem to be, broadly speaking, three1 distinct foundations of mathematics: set, type and category theory (the latter as per Lawvere), in which it should be possible to formalize all mathematics ...
1
vote
1answer
67 views

Implications as functions in type theory

Unpacking $P\Rightarrow Q$ in logic as $P\to Q$ in type theory I'm reaching confusion. (Ref. Homotopy Type Theory p. 55, 154). Suppose what I want in logic is something like this $(\forall x)(P(x)\...
0
votes
2answers
101 views

If Type Theories are all Logics.

So it sounds like Higher Order Logic (HOL) and Type Theory are equivalent. Then there is Intuitionistic Logic and Intuitionistic Type Theory, but I'm not sure of the connection there. I am just ...
0
votes
0answers
57 views

What is the computational content of induction?

I must first admit that I have troubles formulating my question. I'll try to do my best. Peano Arithmetic postulates induction as an axiom out of the thin air. I understand the convenience of this ...
1
vote
1answer
70 views

How do I call cardinality in type theory?

In set theory, we say "cardinality" when we mean "how many members are there in a set". Is there a corresponding notion in type theory? (Any thereof) For example, I have the idea that the functions ...
3
votes
3answers
114 views

Comma in turnstile (entailment)

In a sequent, on the left and right-hand side of the turnstile operator, does the comma denote disjunction or conjunction? $$\frac{...}{\Delta_1,\Delta_2 \vdash \Gamma_1,\Gamma_2}$$ I think it's one ...
1
vote
1answer
63 views

Formal Model of Immutability

Wondering if there is a formal model / algebra / etc. of immutability. This comes up in functional programming with persistent data structures, but I haven't seen any pure math related to it. For ...
0
votes
1answer
59 views

What is a Permutation of a Typing Environment?

In Types and Programming Languages by Pierce the author talks about how permuting a typing environment does not affect bindings from variables to types. Specifically he states: The first structural ...
2
votes
1answer
62 views

Variable Condition in Typed Lambda Calculus

tl;wr In which way does the variable condition for the typing of $\forall_x$, carried over by the $\forall_x$-introduction rule, limit the type setting? Is there more to it then keeping it in line ...
2
votes
2answers
85 views

What kinds of variables range over proofs?

I hope this question does not seem to obscure... Consider the standard inference rule schema for, say, conjunction: ...
1
vote
1answer
116 views

Intro to computational “side effects” from an algebraic perspective.

In functional programming, side effects are a common problem (dealing with the outside world). In math functions are often thought of as "pure". Elm is a programming language that handles side effects ...
1
vote
0answers
60 views

Primitive notions for positiv types

I am currently trying to understand how to formalize homotopy type theory in Church-style as proposed in the second appendix of the HoTT book. How am I supposed to interpret the constructors of ...
47
votes
5answers
3k views

What do logicians mean by “type”?

I enjoy reading about formal logic as an occasional hobby. However, one thing keeps tripping me up: I seem unable to understand what's being referred to when the word "type" (as in type theory) is ...
1
vote
1answer
50 views

Type former as primitive constants

in the first appendix of the HoTT book the type formers (or connectives) are defined to be primitive constants, e.g. $\sum_{x:A}B$ is defined as $c_{\sum}(A,\lambda x.B)$. I was wondering what the ...