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.

692 questions
Filter by
Sorted by
Tagged with
3 votes
1 answer
39 views

Why aren't $\infty$-groupoids commutative in HoTT?

I'm trying to read through HoTT, but I'm confused by the path induction principle, it seems too strong at the first glance. I tried "proving" that all suitable paths commute, and it looks ...
• 7,991
1 vote
0 answers
35 views

How strong is Church's type theory?

This article on the Stanford Encyclopedia of Philosophy describes "Church's type theory", i.e. the simply typed lambda calculus together with a set of inference rules and a set of axioms ...
• 553
3 votes
1 answer
54 views

Michell FPL 2.3.5 (observable types)

(a) Show that the relation of observational equivalence remains the same when changing the observable types of pcf from nat, bool to nat. (b) Further show that changing from nat,bool to nat, bool, ...
• 615
2 votes
1 answer
53 views

Mitchell Foundations for PL 2.3.4 (observational equivalence)

Background. The language is PCF, with observable types $\text{bool}$ and $\text{nat}$. $\text{eval}$ is the partial function on PCF terms such that $\text{eval}(M) = N$ iff $N$ is the unique normal ...
• 615
2 votes
0 answers
28 views

Where do recursive types fit in the lambda cube?

A way to extend the simply-typed lambda-calculus $\lambda_\to$ is to consider recursive types of the form $\mu\alpha.\tau$ (see for example http://www-verimag.imag.fr/~iosif/LogicAutomata07/type-...
1 vote
1 answer
51 views

• 3,574
4 votes
0 answers
188 views

How do I play type theory? What are the rules?

What I (think) I know: Type theory is a game where you construct trees from strings. As far as I can tell, the rules of the game are roughly those of a Gentzen system whose "propositions" ...
• 4,922
1 vote
1 answer
101 views

What is the nature of the double negated axiom of choice?

Under what circumstances is the principle $$nnaoc : (\Pi x:A. \lnot \lnot B_x) \implies \lnot \lnot (\Pi x: A. B_x)$$ valid? So the axiom of choice, but using double negation instead of propositional ...
2 votes
0 answers
48 views

Knowledge graphs, logic and categories recommendation

I recently started to be more interested about "classical AI" and in particular about knowledge graphs/ontologies. I was looking for a modern (written after 2015 if possible) and highly ...
• 280
0 votes
0 answers
70 views

Introduction to Proof via Type Theory

Is there an introduction to mathematical proofs book that uses type theory instead of set theory? I'm aware of books like Hammack's Book of Proof or Epp's Discrete Mathematics with Applications but ...
1 vote
1 answer
51 views

How do types and representations/interpretations work together?

I am trying to figure out how types and variables can work together to represent something in the real world but i am getting stuck. This is how i'm trying to define variables that have normal ...
0 votes
0 answers
64 views

Is every non-set collection just a collection of "sets with some extra data"?

Okay, so in set theory, all the sets together do not form a set, so we say we have a "class" of sets (for example, if we do category theory). In the same way, we have a class of groups, ...
4 votes
1 answer
76 views

Does each inductive definition represent new inference rules?

This is the one thing that I understand the least about formal type theory. For example, in HoTT, the book is filled with casual (higher or not) inductive definitions (lists, quotients, the real ...
3 votes
1 answer
90 views

What are the different equivalent systems of mathematical foundations?

We've mostly learned that ZFC set theory can be used as the foundation of mathematics. I remember having seen that there are 5 or 6 equivalent frameworks that can provide the same theoretical ...
• 4,811
2 votes
1 answer
74 views

A seemingly tautological derivation

In Luo's type-theoretical semantics of natural language, he represents, for example, the verb "talk" as having this type: $talk: Human \to Prop$ Unfortunately, Luo doesn't expand much on ...
0 votes
0 answers
40 views

Product types: algebraic structure for modeling product types with commutative and associative product operation

Is there a known algebraic structure over set of Types (however they are defined) which is equipped with: commutative and associative product operation for building product types from simpler types, ...
2 votes
1 answer
316 views

$\mathbb{N}$ as a mathematical object rather than a set [duplicate]

I was reading Terence Tao's book on Real Analysis I. https://terrytao.wordpress.com/books/analysis-i/ My Background: I am not familiar with logic. And I am used to defining $\mathbb{N}$ in the context ...
• 9,468
2 votes
2 answers
98 views

What's the difference between a section and a dependent function?

I'm reading Introduction to Homotopy Type Theory by Egbert Rĳke and get confused by the notions of a section and a dependent function. A section is defined as: Definition 1.2.2 Consider a type family ...
• 730
1 vote
0 answers
121 views

Does Curry-Howard correspondence mean that everyone who writes a program is doing intuitionistic mathematics?

As far as I know, the first statement of the correspondence is between two formal theories named simply typed lambda calculus and intuitionistic propositional logic, which maps types to formulas and ...
• 33
1 vote
0 answers
37 views

Lean: Prove that if homomorphisms are equal as functions, then they are equal as homomorphisms.

Let's say I have a simple magma structure defined as follows: structure Magma := (carrier : Type u) (op : carrier → carrier → carrier) together with a magma ...
• 316
0 votes
0 answers
62 views

Is there an operation of the type $([0,1]\to\text{real})\to(([0,1]\to\text{real})\to\text{real})\to (([0,1]\to\text{real})\to\text{real})$?

In the introduction of the book lambda calculus with types by Barendregt, there are examples of typed functions like And I wonder what operation the underlined type expression is for. Although we can ...
• 323
4 votes
1 answer
145 views

An overview of mathematical-logical approaches in formalizing natural languages

Crossposted on MathOverflow I am an undergraduate mathematics student with a keen interest in pursuing research in the formalization of natural languages (from a more mathematical-logical approach), ...
0 votes
1 answer
113 views

Circularity in the proof of uniqueness principle for product types in HoTT book

This is possibly something I've overlooked while reading the HoTT book (section 1.5), on defining the product types and proving the uniqueness principle for it (every element of a product type is a ...
0 votes
0 answers
62 views

Intuition of embedding set theory as pointed graphs into type theory

I'm reading this SEP on type theory and I am confusd in the following part: How can we explain the notion of sets in terms of types? There is an elegant solution, due to A. Miquel which complements ...
• 11.4k
0 votes
1 answer
73 views

Relationships and differences between typology and type and category theories?

From linguistics, I saw typology. By dictionary, typology is the study of or analysis or classification based on types or categories. So I was wondering if there are some relationships and differences ...
• 47.2k
0 votes
1 answer
66 views

If $\Gamma\vdash b:\mathsf{Glue}[\phi\mapsto(T,f)]A$, then $\Gamma,\phi\vdash b:T$

Can someone help me from where in those rules I can deduce what is printed below, i.e. that if $\Gamma\vdash b:\mathsf{Glue}[\phi\mapsto(T,f)]A$, then $\Gamma,\phi\vdash b:T$? All the gluing types ...
• 3,574
2 votes
1 answer
95 views

How To Choose What Counts As Isomorphic

Just a naive question about univalent foundations. As far as I understand, we want to define our mathematical types like sets, groups, categories, etc. such that structurally identical objects are ...
• 3,574
0 votes
0 answers
44 views

Is it possible to define the notion of an indexed family in higher-order logic?

I have been trying to define the notion of a product of second-order classes using (finitary) second-order and if needed third-order logic. It seems to be possible to define the product of finitely ...
2 votes
0 answers
76 views

What “probable” means in two-sorted set theory?

I’m reading an nlab article two-sorted set theory. It is written that There are a number of ways to present a set theory; one of the most basic decisions when it comes to presenting a set theory is ...
• 406
1 vote
1 answer
85 views

Is there a projection functor $\mathbf{Set}/X^2 \to \mathbf{Set}/X$

I have an object in the slice / arrow category $\mathbf{Set}/X^2$ and I want to transport it to $\mathbf{Set}/X$ by forgetting the second element of the index. Reading up on slice categories I've only ...
• 13
2 votes
0 answers
51 views

violation of Church Rosser with sum types

On https://ncatlab.org/nlab/show/sum+type the following $\eta$-reduction rule is given for sum types: $$\mbox{match}(p,x.c[\mbox{inl}(x)/z],y.c[\mbox{inr}(y)/z]) \rightarrow_{\eta} c[p/z]$$ This rule ...
• 636
0 votes
1 answer
65 views

About double negation and dependent function in Agda

data ⊥ : Set where f : {A : Set} → {B : A → Set} → ((a : A) → ((B a) → ⊥) → ⊥) → (((a : A) → B a) → ⊥) → ⊥ f = {! !} Type of the function f means: If "If ...
• 13
14 votes
3 answers
596 views

Help! I don't believe in the identity elimination rule for Martin-Löf type theory/HoTT!

I was watching this video this video "$\infty$-Category Theory for Undergraduates" by Emily Riehl, and was onboard with everything except the path induction principle for identity types (27:...
• 8,531
9 votes
1 answer
704 views

How is the “ Axiom of choice is trivial in intuitionistic logic”?

In slide 28 of these slides, the author claims that the “Axiom of choice is trivial in intuitionistic logic” and that classical logic makes it a “ monster from outer space”. How is it trivial when it’...
• 1,159
2 votes
1 answer
101 views

Is it fair to say that Martin Löf Type Theory is doing the same for maths as what type theory did for programming languages?

Let me clarify what I mean. I am currently writing a dissertation on ML/Homotopy type theory as someone who is more of a theoretical computer scientist than an Algebraist. My dissertation is focused ...
2 votes
1 answer
158 views

Type Theory as a Meta-Language for Logic

I am unsure which StackExchange site is the most appropriate for this question, but I believe this site is the most appropriate. My current project involves rigorously proving all the mathematical ...
• 951
25 votes
3 answers
3k views

Approaching Type theory and Category Theory as a starting point in the study of mathematics?

I'm a Computer Engineering student, with interest in Type Theory and Category Theory and i have a more pedagogical/philosophical question about these areas. It seems that many researchers in Type ...
2 votes
1 answer
164 views

Typed logic vs many-sorted logic

I am confused as to what is the difference between many-sorted logic and typed logic. Are they the same thing? If not, what are the differences?
• 406
1 vote
1 answer
66 views

Establishing $\Gamma, A: Type \vdash (A)Type\ \textbf{kind}$ in LF

This is a follow-up to my previous question. Consider the same LF as in that question: LF is a simple type system with terms of the following forms: $$\textbf {Type}, El(A), (x:K)K', [x:K]k', f(k),$$ ...
3 votes
1 answer
194 views

Why use LF to define type theories?

I'm trying to understand the notion of a logical framework and how/why/when it's used to define type theories. I'm looking at Luo's "Computation and Reasoning" (1994), where he considers LF, ...
0 votes
0 answers
49 views

How do I define a notion of infinite coproducts for objects in a category?

As part of a project I'm working on; I am writing an interpreter for the STLC (simply typed $\lambda$-calculus) in which the type-checking algorithm treats isomorphic types as "equal". I ...
6 votes
1 answer
239 views

Gödel on the “True Reason” for Incompleteness

In footnote 48a of his famous paper on incompleteness, Gödel writes: [T]he true reason for the incompleteness inherent in all formal systems of mathematics is that the formation of ever higher types ...
• 113
0 votes
1 answer
63 views

Forcing $\pi_1(\tilde f(a))=f(a)$ for an object of a sigma type

Suppose I have an object $f$ of type $\Pi x:A.B(x)$, and consider a new type $\Pi (x:A).\Sigma (t:B(x)).C(t)$. If $\tilde f$ is an object of the second type and $a:A$, then $\pi_1(\tilde f (a)):B(x)$, ...
2 votes
1 answer
77 views

On iterated sigma type

Just to make sure I understand the notation in the excerpt below (from Corfield's "Modal Homotopy Type Theory") correctly, is the "sum" over $x:Activity, y:Achievement$" the ...