<p>I am wondering if there are any interesting rules/judgemental equalities, denoted <span class="math-container">$A$</span>, which satisfy the following properties:</p>

<p><span class="math-container">$iMLTTfe+UA \implies \neg A$</span></p>

<p><span class="math-container">$iMLTTfe+UIP \implies \neg A$</span>, or more specifically Observational type theory.</p>

<p><span class="math-container">$iMLTTfe+A$</span> is consistent and satisfies canonicity.</p>

<p>Where abrrevations mean:<br/>
iMLTTfe - intensional Martin-Löf type theory with function extensionality<br/>
UA - univalence axiom<br/>
UIP - uniqueness of identity proofs</p>

CC BY-SA 4.0
2020-03-30T08:15:15.777Z
Not really familiar with this, but is it possible to add an axiom to a theory without canonicity (e.g. $iMLTT+FunExt$) and get something *with* canonicity? That seems weird to me.
SCappella
CC BY-SA 4.0
2020-03-30T08:18:45.600Z
@SCappella from my understanding this is possible, the new axiom could explain the computational content of the stuck terms.
Ilk
CC BY-SA 4.0
2020-03-30T08:22:09.923Z
Ah, so you're including adding judgemental equalities and similar things, not just postulating terms of particular types (like UA, UIP and FunExt do). Ok, sounds good to me.
SCappella
CC BY-SA 4.0
2020-03-30T16:24:31.477Z
Could you please react to @SCappella's last remark. What is the precise status of your $A$? Can it be a judgmental equality? Can I add a new type constructor with suitable equations? Or must $A$ be precisely an axiom, namely an introduction of a single constant $c$ of some type $T$ that is already expressible in the type theory?
Andrej Bauer
CC BY-SA 4.0
2020-03-30T16:28:53.060Z
Yes it can add new judgmental equalities.
Ilk
CC BY-SA 4.0
2020-03-30T16:36:46.163Z
So you are not really talking about axioms, but rather new rules. Please edit your question accordingly.
Andrej Bauer
CC BY-SA 4.0
2020-03-30T16:39:12.797Z
Hi, I am not entirely sure how to phrase this correctly, is my last edit appropriate?
Ilk
CC BY-SA 4.0
2020-03-30T22:09:26.470Z
I think it's a lot better.
Andrej Bauer
CC BY-SA 4.0
2020-03-30T22:12:05.237Z
A small optimization: since $\mathrm{UA}$ implies $\mathrm{FunExt}$, your base theory could be $\mathrm{iMLTT} + \mathrm{FunExt}$ throughout. Then you're asking for $A$ which is incompatible with univalence *and* with UIP, but it gives you canonicity. Hmm, I can't even think of reasonable $A$'s that are incompatible with both univalence and UIP.
Andrej Bauer
CC BY-SA 4.0
2020-03-30T23:30:55.767Z
Can't you just take $A=$"Every type is 2-truncated, but there exists a type that is not 1-truncated"?
cody
CC BY-SA 4.0
2020-03-30T23:31:28.017Z
Just kind of squeezing a type between UIP and full Univalence...
cody
CC BY-SA 4.0
2020-03-31T07:34:41.647Z
@cody yes, that would fit the bill as long as the resulting type theory is known to be extendible to satisfy canonicity.
Ilk
CC BY-SA 4.0
2020-03-31T07:46:40.873Z
@cody From your comment and googling this would mean Canonicity for 2-Dimensional Type Theory, should fit the bill of what I am looking for.
Ilk
<type-theory>
Rules between UIP with function extensionality and univalence
Ilk
# Rules between UIP with function extensionality and univalence

(Asked by: username_0 on 2020-03-30)

I am wondering if there are any interesting rules/judgemental equalities, denoted $A$, which satisfy the following properties:

$iMLTTfe+UA \implies \neg A$

$iMLTTfe+UIP \implies \neg A$, or more specifically Observational type theory.

$iMLTTfe+A$ is consistent and satisfies canonicity.

Where abrrevations mean:  
iMLTTfe - intensional Martin-Löf type theory with function extensionality  
UA - univalence axiom  
UIP - uniqueness of identity proofs

**Tags:** type-theory

> **Comments:**
> **username_1**: Not really familiar with this, but is it possible to add an axiom to a theory without canonicity (e.g. $iMLTT+FunExt$) and get something *with* canonicity? That seems weird to me.  
> **username_0**: @username_1 from my understanding this is possible, the new axiom could explain the computational content of the stuck terms.  
> **username_1**: Ah, so you're including adding judgemental equalities and similar things, not just postulating terms of particular types (like UA, UIP and FunExt do). Ok, sounds good to me.  
> **username_2**: Could you please react to @username_1's last remark. What is the precise status of your $A$? Can it be a judgmental equality? Can I add a new type constructor with suitable equations? Or must $A$ be precisely an axiom, namely an introduction of a single constant $c$ of some type $T$ that is already expressible in the type theory?  
> **username_0**: Yes it can add new judgmental equalities.  
> **username_2**: So you are not really talking about axioms, but rather new rules. Please edit your question accordingly.  
> **username_0**: Hi, I am not entirely sure how to phrase this correctly, is my last edit appropriate?  
> **username_2**: I think it's a lot better.  
> **username_2**: A small optimization: since $\mathrm{UA}$ implies $\mathrm{FunExt}$, your base theory could be $\mathrm{iMLTT} + \mathrm{FunExt}$ throughout. Then you're asking for $A$ which is incompatible with univalence *and* with UIP, but it gives you canonicity. Hmm, I can't even think of reasonable $A$'s that are incompatible with both univalence and UIP.  
> **username_3**: Can't you just take $A=$"Every type is 2-truncated, but there exists a type that is not 1-truncated"?  
> **username_3**: Just kind of squeezing a type between UIP and full Univalence...  
> **username_0**: @username_3 yes, that would fit the bill as long as the resulting type theory is known to be extendible to satisfy canonicity.  
> **username_0**: @username_3 From your comment and googling this would mean Canonicity for 2-Dimensional Type Theory, should fit the bill of what I am looking for.  

---

## 0 answers

