L. Garde's user avatar
L. Garde's user avatar
L. Garde's user avatar
L. Garde
  • Member for 5 years, 3 months
  • Last seen this week
2 votes

Is there a distinction between rules of inference and axioms in Homotopy Type Theory (HoTT)?

4 votes

Type Theory: we cannot prove double negation, but can we prove it is unprovable?

4 votes
Accepted

Difference between Propositional and Judgmental Equality

0 votes

Can maths functions "return" multiple different mathematical objects?

2 votes
Accepted

Context in context of Type Theory

4 votes

In what sense does Homotopy type theory "model types as spaces"

2 votes

Intuitionistic “atomic” proof of negation?

0 votes

How does the “proofs as programs” correspondence work for equality?

3 votes
Accepted

What is an example of constructive vs. nonconstructive type theory?

3 votes
Accepted

Do we always have $(A\times (A \to 0)) \simeq 0$?

1 vote
Accepted

Propositional truncation and information hiding

0 votes

Extension of a Signature

1 vote
Accepted

concatenation of contexts

2 votes
Accepted

Inductive definition of terms in "The Calculus of Constructions"

1 vote

Consistent ways/ rules to define types with generators.

1 vote

Property of well-formed contexts in Martin-Löf type theory

4 votes
Accepted

Why such a complicated definition of recursion for $\mathbb{N}$ in HoTT?

0 votes

Constructivity and Piecewise Functions

2 votes

a basic univalence puzzle concerning the sup function on sets