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.

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 ...
Alexei Averchenko's user avatar
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 ...
M. Sperling's user avatar
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, ...
emesupap's user avatar
  • 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 ...
emesupap's user avatar
  • 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-...
user avatar
1 vote
1 answer
51 views

Combinatory Logic Problem With Partial Reductions

I'm working through Bacon's Philosophical Introduction to Higher Order Logic. I am looking for help on the following problem: Exercise 3.17 Calculate the following, assuming that $\wedge : t \to t \...
C D's user avatar
  • 23
3 votes
2 answers
116 views

Prove that the normal form of a closed term in the STLC of simple type contains no lambdas or applications.

Suppose that we have a closed term x:t in the simply typed lambda calculus (STLC) (i.e. this term does not contain any free variables). You can use the terminology ...
martin's user avatar
  • 185
2 votes
1 answer
80 views

Church–Turing thesis for higher order functions, a clear-up

I came across the following MO question https://mathoverflow.net/questions/461426/church-turing-thesis-for-higher-order-functions and got confused. The author asks for references of Church-Turing-...
Jii's user avatar
  • 143
2 votes
2 answers
156 views

LEM and the curry-howard correspondence

The curry-howard correspondence rests upon constructive/intuitionistic logic. Proof checkers only work because they are guaranteed to halt. Proof checkers are built on the simply typed lambda calculus ...
user avatar
0 votes
0 answers
88 views

Motivations for introducing a "super-universe"

I'm trying to understand universes in type theory, and I'm looking at this note. Let's consider a toy example, where we have just two universes, $U_0$ and $U_1$. Then we have this set of rules (...
user837242's user avatar
0 votes
0 answers
49 views

Can we recursively enumerate every type in type theory?

Can we answer the question: "What are all the types?" i.e. can we recursively generate all the types in a given type theory according to a certain set of rules? Pardon for asking such a ...
Pineapple Fish's user avatar
2 votes
1 answer
103 views

Does The Dependent Product Functor Relate To Type Theory?

I'm confused by the naming of the dependent product functor. As far as I understand, in the category of sets, given $f:X\to Y$ and $u:A\to X$, the dependent product functor $\Pi_f:\mathsf{Set}_{/X}\to\...
fweth's user avatar
  • 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" ...
R. Burton's user avatar
  • 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 ...
tailcalled's user avatar
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 ...
geguze's user avatar
  • 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 ...
Byron Gautier's user avatar
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 ...
Richard Bamford's user avatar
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, ...
Tempestas Ludi's user avatar
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 ...
kongus_bongus's user avatar
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 ...
Netchaiev's user avatar
  • 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 ...
user avatar
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, ...
000 000's user avatar
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 ...
Bryan Shih's user avatar
  • 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 Rijke 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 ...
user144765's user avatar
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 ...
Senmorta's user avatar
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 ...
Jan Matula's user avatar
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 ...
prime235711's user avatar
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), ...
Heleyrine Brookvinth's user avatar
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 ...
Xiaojia Rao's user avatar
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 ...
tryst with freedom's user avatar
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 ...
Tim's user avatar
  • 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 ...
fweth's user avatar
  • 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 ...
fweth's user avatar
  • 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 ...
user867078's user avatar
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 ...
BonBon's user avatar
  • 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 ...
cxandru's user avatar
  • 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 ...
provocateur's user avatar
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 ...
Komoe's user avatar
  • 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:...
D.R.'s user avatar
  • 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’...
Lave Cave's user avatar
  • 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 ...
Dmitriy Filippov's user avatar
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 ...
rfloc's user avatar
  • 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 ...
Mateus Galdino's user avatar
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?
BonBon's user avatar
  • 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),$$ ...
user avatar
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, ...
user avatar
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 ...
Rahul Chhabra's user avatar
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 ...
neddo's user avatar
  • 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)$, ...
user avatar
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 ...
user avatar

1
2 3 4 5
14