Questions tagged [homotopy-type-theory]

For questions about the field of study known as homotopy type theory.

Filter by
Sorted by
Tagged with
16
votes
1answer
2k views

Formalizing Homotopy Type theory in Idris

Looking at the homotopy type theory blog one can easily find a lot of library formalizing most of Homotopy Type Theory in Agda and Coq. Is there anyone aware if there is any similar attempt to ...
14
votes
2answers
831 views

In the Hott book, are the most of the type formers redundant? And if so, why?

In chapter 1 and Appendix A of the Hott book, several primitive type families are presented (universe types, dependent function types, dependent pair types, Coproduct types, Empty Type, Unit type, ...
14
votes
2answers
1k views

Proof relevance vs. proof irrelevance

I want to use use Agda to help me write proofs, but I am getting contradictory feedback about the value of proof relevance. Jacques Carette wrote a Proof-relevant Category Theory in Agda library. But ...
13
votes
3answers
770 views

What are the negative consequences of extending CIC with axioms?

Is it true that adding axioms to the CIC might have negative influences in the computational content of definitions and theorems? I understand that, in the theory's normal behavior, any closed term ...
13
votes
1answer
755 views

Can we derive Cubical Type Theory from Self-Types?

Self Types are known for being a simple extension to the Calculus of Constructions that allow it to derive all inductive datatypes of a proof assistant like Coq and Agda, without a "hardcoded&...
12
votes
1answer
2k views

Homotopy type theory and Gödel's incompleteness theorems

Kurt Gödel's incompleteness theorems establish the "inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic". Homotopy Type Theory provides an alternative ...
10
votes
1answer
542 views

Why is regularity a problem in cubical type theory?

In my current understanding, regularity in cubical type theory is the following definitional equality (I'm using $A~\textbf{type}$ to emphasize the fact that $i \notin FV(A)$): $$ \cfrac{A~\textbf{...
10
votes
1answer
169 views

Relating univalence for a theory of cateogries to the skeleton concept

Say I work in homotopy type theory and my sole objects of study are conventional categories. Equivalences here are given by functors $F:{\bf D}\longrightarrow{\bf C}$ and $G:{\bf C}\longrightarrow{\...
9
votes
0answers
238 views

Model of Coq (pCuIC) in higher toposes?

Can the type theory of Coq (pCuIC) be modeled in all higher Grothendieck toposes? First of all, even the set theoretical model is not complete (e.g. inductive types in Prop). Although, this is ...
7
votes
4answers
890 views

Do I have to give up the Law of the Excluded Middle in order to Learn $\lambda$-Calculus?

I know very little about what I am talking about in what follows, so I appreciate any all help in pointing out all of my mistakes -- otherwise I won't be able to learn more and advance in my knowledge ...
7
votes
1answer
300 views

How Univalence can be used for proofs about algorithm correctness

I read a book on homotopy type theory. HoTT has the univalence axiom. This axiom seems to simplify working in category theory, but which other fields of mathematics it simplifies? I.e. how can I use ...
7
votes
1answer
626 views

Squash type vs Propositional truncation type

Homotopy type theory has a notion of propositional truncation type. It seems to me that it's strongly related to a notion of squash types. (See https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf ...
7
votes
1answer
177 views

Obtaining the Axiom of Choice through a modality in HTT

In (constructive) homotopy type theory, the law of excluded middle is not derivable. Moreover, assuming parametricity it is refutable. But, one can work inside the double negation modality to obtain (...
6
votes
0answers
109 views

Programmatic higher inductive/inductive-inductive types with equalities between equalities

I can think of practical HITs in verified software that capture some form of alpha equivalence, context equivalence or the example which defines well-typed syntax of type theory from Signatures and ...
5
votes
1answer
177 views

Choose term of coproduct type

We work in homotopy type theory. Denote the propositional truncation of a type $A$ by $\|A\|$ and the function type between types $A$ and $B$ by $A \to B$. Can you construct a term of the following ...
5
votes
2answers
305 views

In homotopy type theory, is there a IsManifold predicate?

Any type $A: \mathcal{U}$ can be thought of as a homotopy type, or a sufficiently nice topological space up to homotopy equivalence. Now, manifolds are topological spaces with some extra structure. ...
4
votes
0answers
133 views

Abstract stone duality and cohesive homotopy type theory

I have been reading the real-cohesive homotopy type theory paper and one of the remarks has sparked an interest. In this paper a string of monadic and comonadic modalities is introduced together with ...
4
votes
0answers
149 views

Model of homotopy type theory where propositional & judgmental equality coincide for closed terms

In intensional Martin-Löf type theory we can prove the metatheorem that two closed terms are propositionally equal iff they are judgmentally equal. Is there a non-empty model of homotopy type theory ...
4
votes
0answers
322 views

Category theory in plain MLTT

I want to define a category in simple MLTT (not in HoTT). I defined it with the help of setoids. I.e. category consists of: a type of objects with equivalence relation (Obj : Set) a type of arrows ...
3
votes
0answers
90 views

Request for an update on a discussion about coinductive types in HoTT (or anywhere else)

Googling something else I stumbled on a conversation titled "coinductives" initiated by Vladimir Voevodsky on Google groups in 2014. It lasted for three days, invloved a dozen people, and ...
2
votes
2answers
166 views

How does axiom K contradict univalence?

I have seen it claimed several times that axiom K is inconsistent with univalence (e.g. here and here), but I have never seen a proof sketch. Specifically, I'm curious about how this manifests in the ...
2
votes
1answer
71 views

Surjection from a type to a universe

We work in homotopy type theory. Can there be a type $A:U_m$ and a map $f:A\to U_n$ for some $n\geq m$ such that the type $\prod_{T:U_n} \|\mathrm{fib}_f(T)\|$ is inhabited?
1
vote
1answer
203 views

What is the coproduct: A + A? [closed]

In the HoTT book, it is said The type of booleans 2 : U is intended to have exactly two elements. It is clear that we could construct this type out of coproduct and unit types as 1 + 1. I don't ...
0
votes
2answers
225 views

Why is plus-comm a b $:\equiv$ refl (plus a b) not a proof of the commutativity of addition?

I've been curious about the 'geometric situation' that one has when considering the type $\prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ m\ n)$. Here, addition is defined in the ...