The tag has no wiki summary.

learn more… | top users | synonyms

0
votes
1answer
42 views

problems with validity in type theory

I'm twisting my brains over some simple formulas in intensional type theory. If $\exists x \Box (x=^{\vee}j)$, s.t. $x$ is of type $<e>$ and refers to an entity $e$ and $j$ is of type ...
2
votes
2answers
42 views

Questions regarding well formed expressions in the Theory of types

I'm dealing with a question in type theory: Is it possible to assign types to $\alpha$, $\beta$, and $\gamma$ in such a way that both $(\alpha (\beta))(\gamma)$ and $\alpha (\beta (\gamma))$ are ...
9
votes
2answers
184 views

What is the best path to learn Category theory and Type thoery?

I have little background in Programming in functional languages and wanted to learn type theory. I started with taking Homotopy type theory class Online videos of Robert Harper. I thought rather ...
2
votes
1answer
57 views

Why are Truth, Conjunction, and Implication called “Negative” fragments of IPL (intuitionisti logic Proposition Logic)?

Someone answered that negative means we are ""Using"" them . But the point is for all of these there is an Introduction rule too. So why call them negative? I don't know whether it's computer ...
1
vote
1answer
63 views

Being contractible in homotopy theory vs. homotopy type theory

I'm trying to clarify the notion of being contractible in homotopy theory vs. homotopy type theory. Is the following right? "In homotopy theory the real interval $[0,1]$, considered as a subset ...
0
votes
1answer
35 views

Two questions about the empty type

I have a couple of questions regarding the empty type, $0$, in Martin-Lof type theory. I was reading that, in intuitionistic logic, one has $\neg\neg\neg P\rightarrow \neg P$. This amounts to ...
1
vote
1answer
49 views

What is the 'type' of a natural transformation

Let $C,D$ be categories with objects $O_C,O_D$ and morphisms $M_C:O_C\times O_C\to Type_0$, $M_D:O_D\times O_D\to Type_0$. Let $F,G:C\to D$ be functors. A natural transformation $\eta$ associates to ...
0
votes
0answers
18 views

Proving the Identity Type Has a Term

I am trying to get used to type theory. I have a couple of things to ask. Let $1$ be the unit type with unique term $\star : 1$. As an exercise I was trying to prove that $$ ...
0
votes
1answer
30 views

Type theoretic existential introduction and proof with subtypes

I'm working through a book[1], on type theory and categorial grammar (for linguistic applications). Sadly, I ran into problems pretty early on. I'd be very grateful if someone could Explain the ...
3
votes
0answers
54 views

What is the desirable function identification when setting up arrows in the category of types?

My question is which functions can not be allowed in a statically typed programming language, so that the "canonical" category is less coarse than what you get if you define it's arrows to be ...
0
votes
0answers
36 views

When is the higher-order theory of a model categorical?

I'm interested in (classical) type theories $L$ with the following property. For $M$ any model of $L$ (in Set), let $T(M)$ be the type theory of $M$, i.e., the strongest extension of $L$ satisfied by ...
3
votes
2answers
109 views

Types versus kinds and sorts

In the context of logic, especially Higher‑Order‑Logic and Calculus‑of‑Construction, what is a kind and how does it relates to and differs from a type? My raw guess if that a kind is the higher level ...
1
vote
0answers
71 views

Continuations vs. Yoneda

There is this observation (worldpress blog) that the continuation monad (Wikipedia) stems from the Yoneda embedding. For fixed data types $R$, the monad maps data types $T$ to types $(T\to R)\to R$. ...
0
votes
0answers
27 views

Proper terminology for a pair of magmas

Given two magmas, call them $f$ and $g$ over the same set $a$, what do I call a tuple $h$ of them? With extra properties we call them such names as fields and rings. I am just looking for the generic ...
6
votes
1answer
129 views

How to prove that these are the only type inhabitants?

Consider a type $$\mathsf{Boolean} = \forall \alpha.\ \alpha \to \alpha \to \alpha$$ with its two inhabitants \begin{align} \mathrm{tt} &= \lambda x.\ \lambda y.\ x \\ \mathrm{ff} &= \lambda ...
2
votes
1answer
76 views

How do definitions work in Martin-Lof type theory?

The classical viewpoint is that we can found mathematics by specifying a formal system $F$ whose theorems are precisely those of ZFC. However, since $F$ has essentially no support for the concept of a ...
1
vote
1answer
83 views

Typed Category Theory?

This small book (or long paper) describes objects and morphisims in a cateogry as having types. He also talks about pre-categories as categories with typeless objects and morphisims. While I am ...
0
votes
0answers
33 views

Using types instead for basic proofs

Disclaimer: I know close to nothing about formal type theory, but I program intensively so prefer to think in terms of types. In typical math you write $a \in A$ to speak of the nature of your ...
5
votes
3answers
96 views

Types, Sets and Categories

I am learning Category Theory and at first I just pictured a category like a class in object oriented programming: type definition + methods (morphisms). However the author I am reading uses maps ...
3
votes
2answers
114 views

Is there a (foundational) type theory with the features I'm looking for?

I like to distinguish between sets and subsets. We imagine that sets are floating free in the universe, and that the elements of a set are constructed according to some kind of recursive rules. Like ...
3
votes
1answer
42 views

Basic Propositional Logic

I'm working through Thompson's Type Theory and Functional Programming. I've only read the first chapter and want to make sure I'm understanding the material. The first problem asks to prove the ...
2
votes
1answer
85 views

Do we lose everything, if the natural transformations in a monad are exactly inverse?

I'm currently explaining monads $$T:{\bf C}\to{\bf C},\hspace{1cm}\eta:1_{\bf C}\to T,\hspace{1cm}\mu:T\circ T\to T,$$ to my brain and the "only" tricky thing are really the identity relations. I ...
1
vote
1answer
75 views

How to extract the sets “produced” by a axiomatic set theory, into some newly introduced collection?

Say I know well how to reason in a set theory, which for the sake of this question I'll call $\bf{ST}$, say one of those, it can by $\bf ZFC$. It's principally written down via first order logic and ...
3
votes
0answers
53 views

Logic in closed symmetric monoidal categories; reference request.

Suppose we want an algebraic theory $T$ to be interpretable in any closed symmetric monoidal category $\mathbf{C}.$ I am thinking in particular of the case where $\mathbf{C}$ is the category of models ...
1
vote
1answer
57 views

Find subgraphs in a directed graph which are isolated by edge properties

Please excuse my small knowledge of graph theory vocabulary. I can only describe the problem with common english words. Maybe someone can point me into the right direction and/or terms to look up. ...
0
votes
1answer
28 views

A class of “internal” endofunctors in cartesian closed categories

I'm interested in a class of endofunctors on cartesian closed categories with a quite natural definition, and am wondering whether/where this class has been studied so far (and how it is called). Fix ...
0
votes
0answers
49 views

Proof of $(\forall x. \varepsilon(x)) \Rightarrow \bot $ in $\lambda\pi $ calculus $\equiv$

What is the right representation of the proof of $(\forall x. \varepsilon(x)) \Rightarrow \bot $ in simple type theory as a term of $\lambda\pi $ calculus $\equiv$? Note on notation: The epsilon ...
2
votes
1answer
87 views

Simple type theory: Proof inexistance of closed term

In simple type theory, how can I prove that there is no closed term of type? $$((P \Rightarrow Q) \Rightarrow Q) \Rightarrow P$$
1
vote
0answers
36 views

Reductions under lambda in dependently typed lambda calculus

I am currently reading a Simon Thompson's Type Theory book. In chapter 5 he introduces a system TT(0,C), which limits a notion of reduction . In this notion of reduction, reductions under lambda are ...
1
vote
1answer
66 views

Is there a notion of property of a mathematical object?

I have an alphabet or set of symbols $\Sigma$ from which I can build sequences of symbols in $\Sigma^+$ (think of sentences of characters). Now I have a function ...
0
votes
1answer
29 views

Reexpressing the higher inductive-inductive surreals with only two mutual subdefinitions

In $\S 11.6$ of the HoTT book, the authors describe Conway's surreal numbers in terms of a higher inductive-inductive definition with three mutual subdefinitions. However, it seems to me that only ...
3
votes
2answers
186 views

Two questions on homotopy type theory

In reading the HoTT book, I have found that it is easy to become bogged down in detail and hard to tell the general 'big picture' of what is going on. I hope to get some general answer to the ...
2
votes
1answer
74 views

Is it possible to express sigma-type in Martin-Löf type theory with other constructs

In Martin-Löf type theory we have sigma types (dependent products). Is it possible to express them with other constructs? How expressive is dependently typed lambda calculus without them, i.e. what we ...
1
vote
1answer
46 views

Proof that the empty type exists

Is there a proof that the empty type exists? If there is, it's not in my textbook and I haven't been able to find one online. I feel like if it's impossible to prove the existence of the empty type, ...
4
votes
3answers
118 views

What's a good resource to learn about the simply typed lambda calculus?

I've read An Introduction to Functional Programming Through Lambda Calculus by Greg Michaelson, and found it to be a very good resource to learn about the untyped lambda calculus. However, I want to ...
2
votes
0answers
38 views

What if typing judgements were propositions?

Suppose we created a modified type theory in which typing judgments like $x : X$ are not judgments at all; rather, they're propositions. Would this be a bad idea? If so, why? A good answer should ...
2
votes
1answer
230 views

How to represent Smullyan's “Mockingbird” puzzles in (Homotopy) Type Theory?

(If you're unfamiliar with the puzzles from To Mock a Mockingbird, three pages tell you everything you should need.) Is it possible to solve the riddles in To Mock a Mockingbird in a "propositions as ...
2
votes
2answers
61 views

Construction Types or Type Constructions?

In any (simple) type theory there are base types (i.e. the type of individuals and the type of propositions) and type builders (i.e. $\rightarrow$, which takes two types $t,t'$ and yields the type of ...
2
votes
0answers
57 views

Set Theory - Well Order (Lexiographical combination)

Question: Prove constructively that if $(A_{1},\prec_{1})$ and $(A_{2},\prec_{2})$ are two well-ordered sets then their lexicographical combination $(A_{1} \times A_{2},<_{1,2})$ is also well ...
4
votes
1answer
89 views

How to describe free magmas in more structuralist terms?

Given a generating set $G$ (assume for simplicitly it consists entirely of urelements), the free magma on $G$ can be described concretely as follows. Its underlying set is the least $U \supseteq G$ ...
1
vote
1answer
46 views

Basic concerns about dependent function types

I am working my way through the introductory material of Homotopy Type Theory and by the end of section $1.5$ it is clear that I did not have the earlier material down as clearly as I had thought. I ...
3
votes
1answer
177 views

Logic within Type theory. Is there a rough academic consensus on how this should be done?

I guess because of it's presence in several blogs on math and even physics, I've recently started to learn some type theory, often from people who know about it and from books which use it. I want to ...
16
votes
3answers
641 views

What good is infinity?

I am becoming increasingly convinced that Wildberger's views are, if a little bizarre, at least not hopelessly inconsistent. When I was reading the comments in the video following (MF17), somebody ...
8
votes
1answer
274 views

Axiom of Choice - Type Theory (Proof)

Background In Intuitionistic Type Theory (p. 27-28), Martin Löf provides a proof of the axiom of choice that is constructively valid. This version is considerably weaker than the ordinary set theory ...
2
votes
1answer
113 views

Unprovable Equivalence in Type Theory

Let $\prec$ be a binary relation on a set $A$… A predicate $P(x)$ set $(x:A)$ is said to be progressive with respect to $(A,\prec)$ if \begin{equation} (\forall a:A)\Big((\forall b:A)\big(b \prec a ...
7
votes
4answers
177 views

How or why does intutionistic logic proof negations from within the theory, constructively?

I'm having a little of a cognitive dissonance why, in intuitionistic logic, it's possible to show stentences like $(\neg A \land \neg B) \implies \neg(A\lor B).$ In plain text: If 'A isn't true' as ...
4
votes
2answers
206 views

How to understand the definition of sets in homotopy type theory and the role of univalence?

Bear with me, I'm a physicist. In homotopy type theory, as I understand it, a type $X$ is a set if all the morphisms over its terms $x:X$ are identies. When I say "morphisms", then I view the term as ...
1
vote
1answer
75 views

In type theory, why isn't $x = x' : X$ simply wrong?

If $X$ is a set, then personally, I tend to think of the equality relation on $X$ as a function $X^2 \rightarrow \mathrm{Bool}.$ Following this intuition, think that if $x$ and $y$ are variables of ...
6
votes
3answers
342 views

Introductory books as preparation to read Voevodsky homotopy-theory (HoTT) book

I would like to read Voevodsky HoTT book. However, I lack a lot of the basics. I would need a few introductory books first that cover topics like groupoids, fibrations, W -types, Homotopy theory. ...
5
votes
1answer
204 views

Foundational theories, their uses, interactions and comparisons?

Until now, I heard that there are some theories for building mathematical objects (or at least it is what it seems to my poor knowledge). Some of these are: Set theory; Logic; Category theory; Type ...