Questions tagged [type-theory]
The type-theory tag has no usage guidance.
107
questions
5
votes
0answers
164 views
Are any formal systems based upon the idea of “iterated characterization pushing” currently in existence? If not, is anyone working on them?
I had an idea in regards to the design of formal systems with foundational aspirations.
To convey the idea, let's talk a bit about the second-order Peano axioms. The way these axioms work, we have a ...
0
votes
1answer
186 views
A sequence in the hierarchy of universes
The HoTT Book states in the first chapter that universes are cumulative and that every universe is in some other universe.
Obviously, there needs to be an infinite number of universes then, but ...
0
votes
0answers
126 views
An equation involving multisets
For finite multisets $A, B, C, A', B', C'$, if $A \uplus B \uplus \{B \uplus C\} \uplus \{A \uplus \{C\}\}$ = $A' \uplus B' \uplus \{B' \uplus C'\} \uplus \{A' \uplus \{C'\}\}$, must $A=A',B=B',C=C'$, ...
21
votes
8answers
2k views
Good introductory book to type theory?
I don't know anything about type theory and I would like to learn it.
I'm interested to know how we can found mathematics on it.
So, I would be interested by any text about type theory whose angle ...
6
votes
2answers
203 views
When is a fold monomorphic/epimorphic
Given a functor $F : \mathcal C \to \mathcal C$ with initial algebra $\alpha : FA \to A$, and another algebra $\xi : FX \to X$, we obtain a unique morphism $\mathsf{fold}~\xi : A \to X$ such that $\...
5
votes
2answers
674 views
How can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?
It is well-known that the simply typed lambda calculus is strongly normalizing (for instance, Wikipedia). Hence, it is not strong enough to be Turing-complete, as also mentioned on the Wikipedia page ...
3
votes
0answers
249 views
Formal foundations done properly [closed]
I would want to do mathematics properly, so that the proofs of results can be trusted on instead of them being just suggestions on which results could perhaps apply. This means formulating the math in ...
13
votes
1answer
542 views
A peculiarity of Henkin's 1950 proof of completeness for higher order logic
My question concerns Henkin's original (1950) completeness proof https://projecteuclid.org/euclid.jsl/1183730860 for classical higher order logic and type theory relative to so-called general models.
...
5
votes
1answer
371 views
Progress towards a computational interpretation of the univalence axiom?
I will preface this by saying that I am not an expert on type theory. I am just a curious outsider slowly making my way through the HoTT book when I (rarely) have some spare time.
I am just curious ...
6
votes
1answer
339 views
Proof of ¬(¬1 ⊗ ¬1) in tensorial logic
I believe I once had a proof of this proposition, but it's been lost to the mists of time and old hard drives, so who knows if it was correct, and try as I might I can't seem to reproduce it.
Is it ...
3
votes
1answer
108 views
Internal equality for Eq-fibrations' morphisms
I have posted this question here on M.SE but since it received little attention and since it seems difficult to find helpfule references I reposting it here.
In Jacob's Categorical logic and Type ...
12
votes
4answers
1k views
Formalizations of the idea that something is a function of something else?
I'll state my questions upfront and attempt to motivate/explain them afterwards.
Q1: Is there a direct way of expressing the relation "$y$ is a function of $x$" inside set theory?
More ...
8
votes
0answers
249 views
What metatheory proves cut elimination for Simple Type Theory?
Gaisi Takeuti's book Proof Theory proves cut elimination for Simple Type Theory (a combined result of several researchers). Thus it proves consistency of Simple Type Theory with full comprehension in ...
13
votes
0answers
918 views
What's the point of cubical type theory?
I have been following through the development of homotopy type theory since 2013 because I was really interested in the foundation of mathematics. The novel idea of combining programming with homotopy ...
2
votes
1answer
183 views
Can a type in a lower universe be formed from types in higher universes?
A type universe is a type of small types that is closed under the basic type formation operations (dependent product, sum, coproduct etc.), that is to say for example that from
$A \colon U_i$ and
$x \...
