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
2
votes
1answer
85 views

Confusion about quasi-inverses and equivalences in HoTT

I'm reading the HoTT book, section 2.4, where for $f : A \to B$, they define $$\mathsf{qinv}(f) = \sum_{g:B\to A} \big( (f \circ g \sim \mathrm{id}) \times (g \circ f \sim \mathrm{id}) \big)$$ $$\...
0
votes
0answers
39 views

Syntax independent presentation of Homotopy Type Theory

By "syntax independent" I mean no explicit reference to variables. For example, Lambda Calculus is syntax dependent because the notions of "variable", "variable renaming",...
2
votes
1answer
53 views

Can function types be represented using $\Sigma$-types?

Fix types $A, B : \mathsf{Type}$, and let $\mathbf{2} = \{ 0, 1 \} : \mathsf{Type}$ be a two-element type. We define $B' : A \to \mathsf{Type}$ by $B'(a) = B$. $C : \mathbf{2} \to \mathsf{Type}$ by $...
0
votes
1answer
45 views

Can you have Type Theory without types?

Thinking about Type Theory, we define types such as the natural numbers: zero:Nat succ(n:Nat):Nat But I thought that this might be equivalent to having just 2 ...
1
vote
1answer
108 views

Why isn't there an app that allows you to enter in all the rules of a given formal system so that the app supports all formal systems of math?

I'm jumping around between articles about ETCS to Simple TT to Calculus of Constructions wondering what my app should focus on. I'm wondering, why there isn't yet a software app in which you can ...
3
votes
1answer
81 views

Why isn't $\forall x \in X, P(x)$ the same thing as a map of types $P:X \to \text{TrueProp}$?

For example, $\forall x \in X, P(x)$ can be viewed as a map $P : X \to \text{TrueProp}$ the collection of true propositions. Why do we make the distinction in type theory, which seems to want to ...
0
votes
0answers
49 views

Why does a type of all types including itself create a paradox in Martin-Löf type theory?

In Per Martin-Löf (1998) "An Intuitionistic Theory of Types" in G Sambin and JM Smith (eds) Twenty-five years of constructive type theory Clarendon Press (original work written 1972 but ...
1
vote
1answer
82 views

How to derive $\prod x: \text{Nat}, Id(S(x), O) \to \bot$ in Intensional Type Theory

In HoTT Lecture, https://www.youtube.com/watch?v=VWmXF-P4-Z8&list=PL1-2D_rCQBarjdqnM21sOsx09CtFSVO6Z&index=7, Harper introduced a dependent form of recursion rule: $$ \Gamma \vdash M : Nat ~~~ ...
0
votes
1answer
65 views

In homotopy type theory, what is this "mechanical way to create a new expression F' now depending on t' and an equivalence between F(T) and F'(T')"? [closed]

I've read a few slides on the topic citing the following quotation from an email, which, according to these slides, defines the biggest advantage of homotopy lambda calculus over other caculi of ...
2
votes
1answer
84 views

λP2, the Calculus of Constructions, and quantifying over propositions

In $\lambda P2$, we can write polymorphic functions like $\Lambda A. \lambda x. x: \Pi A. A \to A$. By Curry–Howard, this corresponds to the proposition "for all propositions $A$, $A$ implies $A$&...
1
vote
0answers
57 views

Homotopy type theory: what is «path induction» useful for?

I am reading the HoTT book. At page 49 path induction is introduced. Let us recap it. Given a family $$ C: \displaystyle \prod_{(x,y:A)} x =_A y \rightarrow 𝓤 $$ and a function $$ c: \displaystyle \...
6
votes
0answers
130 views

Precise statement of the syntactic category of a logic/type theory, in maximum generality?

I've been trying to understand the notion of syntactic category for a type theory/logic. This entry in the ncatlab is the closest I've found to a clear explanation. It seems like a fairly good article,...
1
vote
2answers
80 views

Formalizing constant symbols as terms in type theory.

In type theory, we usually define each type with a constant symbol, e.g., the dependent product uses '$\Pi$', the dependent sum uses '$\Sigma$', the sum/coproduct uses '$+$'. I noticed that we could ...
1
vote
1answer
62 views

Does the degree of impredicativity always matter in type theory?

My question here is actually about whether different degress of impredicativity matter? To show that, lets confine ourselves with the following predicative formalism. Language: multi-sorted first ...
2
votes
2answers
125 views

judgmental and propositional statements in homotopy type theory

In homotopy type theory one has to distinguish between judgmental and propositional statements, eg in case of $a: A$ ("$a$ has type $A$") and equalities $a =_p b, a=_A b$. That is, are a ...
6
votes
0answers
127 views

What is undecidability within the computational trilogy

The computational trilogy page on nLab gives a nice "Rosetta stone" that translates concepts between the theories of logic, category theory, and type theory. However, one concept it does not ...
1
vote
1answer
97 views

Encoding arbitrary algebraic data types in set theory?

Natural numbers are often defined recursively as an algebraic data type: type Nat := | Zero | Succ of Nat In set theory/ZFC, we can define the natural numbers ...
1
vote
1answer
61 views

Help me understand type theory notation

From Calculus Of Constructions : Does this mean, for definition environment $\Gamma$, for $x$ is of type $A$, and for even more definitions $\Gamma '$, it is assumed that there are no contradictions ...
0
votes
0answers
23 views

Type-theoretic strategies for encoding the notion of an even integer given an evenness predicate and an integer type

A type is loosely analogous to a set. Pushing on this analogy a bit, I'm wondering what the equivalent of the axiom schema of specification is. In particular, I'm curious what strategies are available ...
4
votes
1answer
58 views

Why is coherence important in the LCCC interpretation of substitution in dependent type theory?

Reading about the categorical models of dependent type theory (DTT) I have faced many articles pointing out the coherence problem for the interpretation of DTT in locally cartesian closed categories (...
0
votes
1answer
58 views

Is there a way to formally handle ellipses, which are ubiquitously used in human-level mathematics? $X_1 \xrightarrow{f_1} X_2 \xrightarrow{f_2} ...$

For a use case, I want to formally and visually define what a path is in a graph. My definition will allow duplicates of vertices. So, an inductive definition might start: $$ X_1 : \text{Path} \\ X_1 ...
1
vote
0answers
22 views

Functors in List Reversal Natural Transformation

A common example of a natural transformation as it relates to CS/programming languages is list reversal. List is a functor from ...
1
vote
0answers
78 views

Reference request: is axiom of choice motivated along type-set lines?

Language: bi-sorted first order logic with equality and its axiom and additionally the extra-logical primitives: $ ``\tau, < , \in"$, the first is a total unary function on sets denoting is the ...
1
vote
1answer
34 views

Product type in Type theory

I am new to type theory. It was explained that $\Pi$-type is like cartesian product of types. Firstly, in set theoretic formalization of mathematics, a function $f$ from $\mathbb{N}$ to $\mathbb{R}$ ...
2
votes
0answers
30 views

Some observations about third-order functionals: any relationships between them?

Let $X'$ denote $X \to X$. Here are some observations about third-order functionals over $\mathbb{N}$: They are the natural home of ordinal notations. In general, $f \in \mathbb{N}'$ can only be ...
5
votes
1answer
70 views

$\lambda$-calculus: find $F$ such that $FI = x$ and $FK = y$

I'm learning some $\lambda$-calculus using the following book: http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf I'm having some trouble with exercise 2.12 (iii) on page 15. ...
2
votes
0answers
42 views

What is the strength of simple type set theory without infinity?

Lets have a multi-sorted first order theory, so a variable that range over all objects of some sort is denoted by a natural index over that variable as usual. So $x^i$ range over all objects of the $i^...
3
votes
0answers
70 views

constructive type theory books

What is the best book you recommend for a beginner in constructive type theory applied to computer science?
0
votes
1answer
55 views

Is there a general notion of definability/expressibility?

If we want to talk about uncountable sets, then we can distinguish between objects in the set that we can actually "specify" and those that we can't. An example of objects that can be ...
1
vote
0answers
70 views

Polynomial functors, Type Theory and Homotopy

I am finding that there is a bit of a battle going on to provide a "foundation" of Type Theory, and perhaps for Mathematics, either with polynomial functors or Homotopy Type Theory. There ...
1
vote
1answer
46 views

Derivation of term conversion rule

I've started to read Egbert Rijke's HoTT lecture notes which can be found here. In the first lecture, some inference rules and structural rules are given, and in Exercise 1.1 it is asked to derive ...
0
votes
0answers
32 views

What do I lose if I thread fresh variables through typing judgements?

What do I lose if I thread fresh variables through my typing rules? It's useful for moving to HOAS in stuff like Coq later. This seems sequent like to me but I don't understand the sequent calculus. ...
8
votes
1answer
105 views

Intensional identity

I have some basic questions about intensional identity. Two types are said to be (intensionally) identical iff “they have the same objects and identical objects of one of the types are also identical ...
1
vote
0answers
81 views

Right adjoint of pullback functor

Let $f:A {\rightarrow} B$ be an arrow in a topos $\mathbb{C}.$ The pullback functor $f^*: \mathbb{C} /B {\rightarrow} \mathbb{C} /A$ sends an object of the slice category $\mathbb{C} /B$ to the ...
7
votes
1answer
86 views

From $\textsf{Prop}$ to $\textsf{Type}$

Let $P,\top:\textsf{Prop}$ (where $\textsf{Prop}$ is the universe of mere propositions), $A=\{P,\neg P\}:\textsf{Type}$ and $B$ is an identity function such that $B(x)=x$. Given the above definitions, ...
4
votes
0answers
53 views

A question about self-reference

Let $\textsf{Prop}$ denote the universe of propositions and let $A:\textsf{Prop}$. Now, consider $(\star)$: $$A\leftrightarrow\exists X:\textsf{Prop}.(X\rightarrow A)\wedge X\tag{$\star$}$$ It is easy ...
2
votes
2answers
156 views

Motivation behind Lambda Calculus?

The lambda calculus provides a formalism broad used in theoreretical cs to write functions without giving them explicit names, it declares anonymous functions. That is at first glance it's just an ...
0
votes
1answer
182 views

Difference between Propositional and Judgmental Equality

I'm reading the HoTT book and actually I'm a bit confused on core difference between propositional equality (noation: $a=_A b$ where $a, b:A$ and judgmental equality $ a \equiv b $. The ...
1
vote
0answers
44 views

Transport operation on $\Sigma$-types in cubical type theory

In Exercise 4.3 of "Cubical Methods in Homotopy Type Theory and Univalent Foundations'', It sais that we run into problems when we try to define computation rules for transport operation on $\...
6
votes
1answer
53 views

Truncation and fixed finite domain

Let $P$ be a type, $||P||$ denotes a mere proposition obtained by truncating $P$. Let $D$ be a type and $A:D\rightarrow\textsf{U}$, then $\Pi x:D.A(x)$ is a well-formed type. Assuming that we are ...
2
votes
0answers
98 views

How to go from Category Theory to Geometry?

I want to connect my knowledge of category theory and type theory to geometry, and I am wondering which theories I should learn. I know category/topos/type theory, but little other abstract algebra. I ...
25
votes
3answers
1k views

Function "evaluation" just means "composition"?

I am self-studying and have a basic or naive question that follows from a simple observation. I have also included tags for type theory, etc because "evaluation" probably has a different ...
5
votes
1answer
104 views

Why is the interval not a type but a pretype?

In Section 3.3 of Naive cubical type theory (Bruno Bentzen): We suggested above that every type is Kan. In fact, the interval is the only exception to this rule, since we have been implicitly ...
8
votes
1answer
789 views

Hierarchy in logical systems

I had an informal conversation in which I was told that logical systems could be intuitively drawn in a hierarchy according to their expressive power, i.e. the amount of things we can prove with them. ...
2
votes
0answers
51 views

Functions which are provably total in second order peano arithmetic

Girard has a representation theorem claiming: The functions representable in $F$ are exactly those which are provably total in second-order peano arithmetic $PA_2$. I believe the usual way to prove ...
6
votes
0answers
55 views

Disjoint union types in MLTT

In MLTT, by identifying propositions as types (and vice versa), a proposition carries the information regarding how a proof of the proposition is constructed. My question is related to this. Let $P:\...
2
votes
1answer
56 views

Truncation and $\Pi$-types (ii)

I just read Ximei's post Truncation and $\Pi$-types. Can anyone explain in simple terms why ($\star$) implies ($\star\star$) but not vice versa. In other words, I wonder why ($\star$) is stronger than ...
1
vote
1answer
83 views

In homotopy type theory, prove that law of excluded middle implies reduction ad absurdum

It's about Excercise 2 from here: While the principle of excluded middle $P\vee\neg P$ ( tertium non datur) is not provable, prove its double negation using the propositions as types translation: $\...
9
votes
1answer
112 views

A question about impredicative type theory

I am playing with impredicative type theories (CC and UTT). I am not quite familiar with the distinction between $\textsf{Prop}$ and $\textsf{Type}$ as it is not available in MLTT. Here is my question....
6
votes
1answer
71 views

Truncation and $\Pi$-types

Truncated types or bracket types are used to recover traditional logic within type theory. I have a question about truncating $\Pi$-types. The question is very basic. Let $A:\textsf{U}$ and $B:A\...

1
2 3 4 5
12