<p>This is not an answer but a very long comment.</p>
<p>I find the idea quite interesting. To keep things focused, I think it would be very good to have a clear idea of what it means for the encoding of cubical type theory to be correct, namely that it is <em>sound</em> and <em>conservative</em>.</p>
<p>Soundness just means you can encode everything (for instance, that you did not forget to encode <code>cong</code>) and that all the expected judgmental equalities (conversions) that are supposed to hold do hold. This should be the easy part.</p>
<p>Conservativity means that the encoding cannot do more than what it is supposed to. Suppose <code>A</code> is a type in cubical type theory and let <code>A'</code> be its encoding using self-types. Then we want</p>
<blockquote>
<p><em>If <code>A'</code> is inhabited in type theory with self-types then <code>A</code> is inhabited in cubical type theory.</em></p>
</blockquote>
<p>And given another type <code>B</code> encoded by <code>B'</code>, we want:</p>
<blockquote>
<p><em>If <code>A' ≣ B'</code> in type theory with self-types then <code>A ≣ B'</code> in cubical type theory.</em></p>
</blockquote>
<p>I would particularly worry about the interval type <code>I</code>. In cubical type theory this is <em>not a type</em>! It is a pre-type that is treated specially. However, you are encoding it as an ordinary type, just like any other, and that sounds very fishy. I think there is a proof in cubical type theory showing that <code>I</code> cannot be an ordinary type but I don't remember it off the top of my head.</p>

CC BY-SA 4.0
2020-09-21T18:25:24.740Z
I agree. From my experience, it makes sense that `I` cannot be an ordinary type, and I think I even see where things would break down: "transp" seems to require a "typecase" that treats "I" in a very "special" way. Regardless, the fact that all the definitions above behave identically to the "hardcoded" cubical primitives makes me think that, if we look into it further, we may find some "clever way" to let these definitions be internal libraries, keeping the language implementation itself minimal, which is my ultimate goal.
MaiaVictor
CC BY-SA 4.0
2020-09-21T18:28:59.540Z
For example, perhaps there is a whole class of "special types" (not just `I`) that can be "lifted" out of self-encodings into something that is more "part of the language". Or not, but answering that question even negatively (as in, "Interval **must** be a primitive") would give me insights about its nature (and then I'd accept it as a primitive on Formality :P). Regardless, I find it very unlikely that "transp" as a primitive will turn out to be the simplest way to add cubical features to a proof language.
MaiaVictor
CC BY-SA 4.0
2020-09-21T18:40:15.643Z
At the very least all the cubes `I ⨉ I ⨉ ... ⨉I` are special also. I do not think the interval must be special, but there should be distinction between pre-types and types. I wonder how exactly Cubical Agda gets around this.
Andrej Bauer
CC BY-SA 4.0
2020-09-21T19:53:39.367Z
Yep, seems like `I` is special exactly in the sense that a `I` in the context isn't like a normal variable in context. I hope I can get a deeper understanding of "why" and "how" it differs precisely.
MaiaVictor
CC BY-SA 4.0
2020-09-21T20:44:27.143Z
The semantic answer is that it's not a Kan cubical set, i.e., it is not fibered.
Andrej Bauer
CC BY-SA 4.0
2020-09-23T18:03:07.963Z
Is it sufficient to make `I` live in another universe?  In my toy language, I use `Bool` for `I` but require my "evidence functions" treat their Bool argument as erased/implicit (in the sense of ICC/ICC*)
Stefan
CC BY-SA 4.0
2020-09-23T21:42:00.200Z
Using `Bool` for `I` is a bit like the tricks employed in Coq and Agda to fake the interval. They rely on abstraction, i.e., hiding the lie behind a mechanism that prevents looking at the definition.
Andrej Bauer
CC BY-SA 4.0
2020-09-29T19:28:11.633Z
Cubical Agda does treat `I` as a type but it does not presume that all types are fibrant. In particular `I` does not support `transp` or `hcomp`: [page 19](https://pure.itu.dk/portal/files/84649948/icfp19main_p164_p.pdf)
Łukasz Lew
CC BY-SA 4.0
2020-09-21T18:13:25.790Z
2020-09-21T18:13:25.790Z
Andrej Bauer
<p>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 &quot;hardcoded&quot; native datatype system. I am now trying to answer if we can also derive the features of Cubical Type Theory. It seems like most essential features, including higher inductive types, Path, Interval and so on can, indeed, be derived from Self alone. But some corners are still missing. I'm posting this as a question to sum up my progress and ask for a helping hand.</p>
<h3>Explaining Self Types (for context)</h3>
<p>For those still unfamiliar, let me explain what Self types are. It is simple: remember that, in a dependently-typed language, <code>f(x) : B(x)</code>? That is, the type returned by an application has access to the applied argument? In a self-dependently-typed language, <code>f(x) : B(f,x)</code>, i.e., the returned type can also access the applied function. That's all. This allows us to derive inductive datatypes naturally. For example, <code>Nat</code> can be defined as:</p>
<pre><code>Nat : Type
  ∀self(P : Nat -&gt; Type) -&gt;
  ∀(zero : P(λz. λs. z)) -&gt;
  ∀(succ : ∀(n : Nat) -&gt; P (λz. λs. s n)) -&gt;
  P self
</code></pre>
<p>With its induction principle being:</p>
<pre><code>nat-ind : (n : Nat) -&gt; P(0) -&gt; ((n : Nat) -&gt; P n -&gt; P (succ n)) -&gt; P n
nat-ind = λn. λz. λs. n P z (λx. s (nat-ind x z s))
</code></pre>
<p>Notice the <code>self</code> variable on the first <code>∀</code> of <code>Nat</code>. When we call <code>n P</code>, it is substituted by <code>n</code> itself, allowing <code>nat-ind</code> to return <code>P(n)</code>. This was the only thing preventing λ-encoded datatypes to replace native datatypes on raw type theory.</p>
<h3>Encoding Path and Interval</h3>
<p>The cool thing about encoding data with Self is that it isn't restricted by the limitations of a native datatype implementation. That allows us to do things that weren't expected by the &quot;language designer&quot;. For example, we're able to implement &quot;constructors with conditions that compute&quot;. We can encode <code>Int</code> as a pair of two <code>Nat</code>s such that <code>int (succ a) (succ b)</code> reduces to <code>int a b</code>. Similarly, nothing prevents us from creating constructors that return &quot;other datatype&quot;. Higher Inductive Types can then be encoded with constructors that return the equality type.</p>
<p>With that in mind, my plan to derive HoTT with Self is to encode the Interval type as a &quot;boolean&quot;, except with a third constructor that enforces the first two to be equal. For that, we need a notion of equality, so I use the cubical <code>Path</code>, which is, too, encoded an inductive datatype, but one with only one constructor: the path abstraction. In Agda pseudocode, it would be written as:</p>
<pre><code>data I : Set where
  i0 : I
  i1 : I
  ie : Path _ i0 i1

data Path (A : I -&gt; Set) : A i0 -&gt; A i1 -&gt; Set where
  abs : (t : (i : I) -&gt; A i) -&gt; Path A (t i0) (t i1)
</code></pre>
<p>Note that <code>Path</code> and <code>I</code> are mutually recursive: <code>Path</code> uses <code>I</code> for its endpoints, and <code>I</code> uses <code>Path</code> to ensure it can only be pattern-matched accompanied by a proof that both branches are equal. This is different from the usual interval type (which can't be pattern-matched at all), but thanks to Path, the effect is the same. The full representation with Self is:</p>
<pre><code>I : Set
  ∀self(P: (i : I) -&gt; Set) -&gt;
  ∀(I0 : P i0) -&gt;
  ∀(I1 : P i1) -&gt;
  ∀(IE : Path P I0 I1) -&gt;
  P(self)

i0 : I
  λP. λi0. λi1. λie. i0

i1 : I
  λP. λi0. λi1. λie. i1

ie : Path (λi. I) i0 i1
  λP. λabs. abs (λi. i)
  
Path (A : I -&gt; Set) (a : A i0) (b : A i1) : Set
  ∀self(P : (a : A i0) -&gt; (b : A i1) -&gt; Path A a b -&gt; Set) -&gt;
  ∀(Abs: (t : (i : I) -&gt; A i) -&gt; P (t i0) (t i1) (abs A t)) -&gt;
  P a b self

abs (A: I -&gt; Type) (t : (i : I) -&gt; A i): Path A (t i0) (t i1)
  λP. λabs. abs t
</code></pre>
<p>This encoding allows us to derive other Path primitives as functions.</p>
<h3>Path application</h3>
<p>Path application allows us to apply a <code>Path A a b</code> to an <code>i : I</code> and get either <code>a</code> or <code>b</code>. Since <code>Path</code>'s only constructor is the path abstraction, then <code>app</code> is just the identity:</p>
<pre><code>app (A : I -&gt; Set) (a : A i0) (b : A i1) (e : Path A a b) (i : I) : A i
  i A a b e
</code></pre>
<h3>Path reflexivity</h3>
<p>We can implement <code>refl</code>, as expected, as a constant path:</p>
<pre><code>refl (A : Set) (x : A) : Path (λi. A) x x
  λP. λabs. abs (λi. x)
</code></pre>
<h3>Path congruence</h3>
<p>We can apply a function to both sides of a <code>Path</code>:</p>
<pre><code>cong (A : Set) 
     (B : A -&gt; Set)
     (x : A)
     (y : A)
     (f : ∀ (a : A) -&gt; B(a))
     (p : Path (λi. A) x y)
     : Path (λi. B (app (λi. A) x y p i)) (f x) (f y)
  λP. λabs. abs (λi. f (app (λi. A) x y p i))
</code></pre>
<h3>Function extensionality</h3>
<p>As expected, funext is very simple for the <code>Path</code> type. We just create a path abstraction that flips <code>i</code> and <code>x</code>:</p>
<pre><code>funext
  (A : Type)
  (B : A -&gt; Type)
  (f : ∀(x : A) -&gt; B x)
  (g : ∀(x : A) -&gt; B x)
  (h : ∀(x : A) -&gt; Path (λi. B x) (f x) (g x))
  : Path (λi. ∀(x : A) -&gt; B x) f g
  abs (λi. ∀(x : A) -&gt; B x) (λi. λx. app (λi. B x) (f x) (g x) (h x) i)
</code></pre>
<h3>Transport</h3>
<p>Now the problem. While <code>Path</code> is great to work with, in order to be a reasonable equality type, we need a <code>transport</code> operation. Defining that seems to be non-trivial. After consulting the <a href="https://www.researchgate.net/publication/334757469_Cubical_agda_a_dependently_typed_programming_language_with_univalence_and_higher_inductive_types" rel="noreferrer">Cubical Agda paper</a>, I've managed to implement its <code>transport</code> and <code>transpPi</code>:</p>
<pre><code>transp (A : I -&gt; Set) (i : I) (x : A i0) : A i1
  ?transp

transport (A : Set) (B : Set) (p : Path (λi. Set) A B) (a : A) : B
  transp (λi. app (λi. Set) A B p i) i0 a

transpPi (A : I -&gt; Set) (B : (i : I) -&gt; A(i) -&gt; Set) (f : (x : A i0) -&gt; B i0 x) (x : A i1) : B i1 x
  let fx : B i0 (transp _ i0 x)
         = f (transport (A i1) (A i0) (abs (λi. Set) (λi. A (not i))) x)
      be : Path (λi. Set) (B i0 (transp _ i0 x)) (B i1 (transp _ i1 x))
         = abs (λi. Set) (λj. B j (transp (λi. A (max (not i) j)) j x)
  in transport _ _ be fx
</code></pre>
<p>But as for <code>transp</code>, I do not know what to do. Agda says it is a primitive and isn't precise about how it computes. It does say, though, that <code>transp _ i1 x = x</code>; but that requires <code>A</code> to be constant when <code>i = i1</code>, otherwise we'd have <code>x : A i0</code> and <code>x : A i1</code> simultaneously, which is ill-typed! This is the first problem: we can't enforce that a function is constant on CoC+Self alone; replicating that would require some &quot;hardcoded&quot; access to a &quot;count_variable_uses(x, term)&quot; function. The second problem is that, on the <code>i0</code> case, seems like we'd need to <strong>type-case</strong> on <code>A i0</code>, in order to specialize <code>x : A i0</code> as <code>x : ∀ (k : P i0) -&gt; Q i0 k</code> and then call <code>transpPi</code>. The nice thing is, since the only type former is <code>Pi</code>, this would complete the proof. But how would such <code>type-case</code> primitive work?</p>
<h3>Questions</h3>
<p>Finally, my questions are.</p>
<ol>
<li><p>Since, in CoC+Self, inside <code>transp</code>, we can't enforce that <code>A</code> is constant when <code>i=i1</code>, is there any other to write <code>transp</code> that doesn't require such ability?</p>
</li>
<li><p>Is my reasoning that <code>type-case</code> is necessary to &quot;pattern-match&quot; on <code>A i0 : Type</code> right? If so, what is the correct elimination rule for <code>Type</code>?</p>
</li>
<li><p>How <em>exactly</em> <code>transp</code> computes? The paper mentioned affirms that <code>transp _ i1 x = x</code>, but what about the other two cases (<code>transp _ i0 x</code> and <code>transp _ ie x</code>)? Is it possible to write how they would look like (even if just as a pseudo-code)?</p>
</li>
</ol>
<p>(You can type-check the proofs above using <a href="https://gist.github.com/MaiaVictor/a34cf36918c89e731b7df8bf97601cf7" rel="noreferrer">this file</a> and Formality.)</p>

CC BY-SA 4.0
2020-09-23T03:37:55.617Z
What are the categorical semantics of Self types?
Mike Shulman
CC BY-SA 4.0
2020-09-23T14:35:47.607Z
I see the type of your `Nat` refers to `Nat`.  Do you have a reference for why/where/when this kind if "recursion" is sound?
Stefan
CC BY-SA 4.0
2020-09-23T17:08:12.613Z
@MikeShulman I don't know, check Aaron Stump's original paper for a more formal presentation.
MaiaVictor
CC BY-SA 4.0
2020-09-23T17:14:34.480Z
@Stefan the usage of `Nat` in `Nat` is necessary for Scott Encodings. I don't think it makes sense to reason about the soundness of a particular feature in isolation, it depends on the language on which said feature is inserted. Looking for sound languages that admit Scott Encodings might provide some answer to your question. Some may want to avoid Scott in favor of Church encodings which are easier to deal with, but I personally find that a mistake.
MaiaVictor
CC BY-SA 4.0
2020-09-23T17:59:03.473Z
@MaiaVictor: my question was indeed if you could point me to a sound language that admits this kind of encoding
Stefan
CC BY-SA 4.0
2020-09-23T20:11:28.973Z
@Stefan I'm not aware of many proven sound languages that use Scott Encodings though. Lambda encodings in general are very unpopular (sadly).
MaiaVictor
CC BY-SA 4.0
2020-09-23T22:07:23.753Z
I can't see use of the Scott encoding in Aaron's paper on self-types (he seems to use the Church encoding), which is why I'm wondering if there is a language which admits this kind of recursion and is sound (or can you get the same result via something like induction-recursion?)
Stefan
CC BY-SA 4.0
2020-10-15T00:04:46.280Z
@Stefan you won't find anything merely because nobody did it, but there is no reason to believe a language with self-types and structural recursion wouldn't be consistent; that's basically Coq, just simplified.
MaiaVictor
CC BY-SA 4.0
2020-10-15T03:32:20.507Z
@MaiaVictor: structural recursion, I agree.  But definitions whose type refers to the definition itself is a completely different matter.
Stefan
<type-theory><lambda-calculus><calculus-of-constructions><homotopy-type-theory>
Can we derive Cubical Type Theory from Self-Types?
MaiaVictor
# Can we derive Cubical Type Theory from Self-Types?

(Asked by: username_0 on 2020-09-21)

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" native datatype system. I am now trying to answer if we can also derive the features of Cubical Type Theory. It seems like most essential features, including higher inductive types, Path, Interval and so on can, indeed, be derived from Self alone. But some corners are still missing. I'm posting this as a question to sum up my progress and ask for a helping hand.
Explaining Self Types (for context)
For those still unfamiliar, let me explain what Self types are. It is simple: remember that, in a dependently-typed language, f(x) : B(x)? That is, the type returned by an application has access to the applied argument? In a self-dependently-typed language, f(x) : B(f,x), i.e., the returned type can also access the applied function. That's all. This allows us to derive inductive datatypes naturally. For example, Nat can be defined as:
Nat : Type
  ∀self(P : Nat -> Type) ->
  ∀(zero : P(λz. λs. z)) ->
  ∀(succ : ∀(n : Nat) -> P (λz. λs. s n)) ->
  P self

With its induction principle being:
nat-ind : (n : Nat) -> P(0) -> ((n : Nat) -> P n -> P (succ n)) -> P n
nat-ind = λn. λz. λs. n P z (λx. s (nat-ind x z s))

Notice the self variable on the first ∀ of Nat. When we call n P, it is substituted by n itself, allowing nat-ind to return P(n). This was the only thing preventing λ-encoded datatypes to replace native datatypes on raw type theory.
Encoding Path and Interval
The cool thing about encoding data with Self is that it isn't restricted by the limitations of a native datatype implementation. That allows us to do things that weren't expected by the "language designer". For example, we're able to implement "constructors with conditions that compute". We can encode Int as a pair of two Nats such that int (succ a) (succ b) reduces to int a b. Similarly, nothing prevents us from creating constructors that return "other datatype". Higher Inductive Types can then be encoded with constructors that return the equality type.
With that in mind, my plan to derive HoTT with Self is to encode the Interval type as a "boolean", except with a third constructor that enforces the first two to be equal. For that, we need a notion of equality, so I use the cubical Path, which is, too, encoded an inductive datatype, but one with only one constructor: the path abstraction. In Agda pseudocode, it would be written as:
data I : Set where
  i0 : I
  i1 : I
  ie : Path _ i0 i1

data Path (A : I -> Set) : A i0 -> A i1 -> Set where
  abs : (t : (i : I) -> A i) -> Path A (t i0) (t i1)

Note that Path and I are mutually recursive: Path uses I for its endpoints, and I uses Path to ensure it can only be pattern-matched accompanied by a proof that both branches are equal. This is different from the usual interval type (which can't be pattern-matched at all), but thanks to Path, the effect is the same. The full representation with Self is:
I : Set
  ∀self(P: (i : I) -> Set) ->
  ∀(I0 : P i0) ->
  ∀(I1 : P i1) ->
  ∀(IE : Path P I0 I1) ->
  P(self)

i0 : I
  λP. λi0. λi1. λie. i0

i1 : I
  λP. λi0. λi1. λie. i1

ie : Path (λi. I) i0 i1
  λP. λabs. abs (λi. i)
  
Path (A : I -> Set) (a : A i0) (b : A i1) : Set
  ∀self(P : (a : A i0) -> (b : A i1) -> Path A a b -> Set) ->
  ∀(Abs: (t : (i : I) -> A i) -> P (t i0) (t i1) (abs A t)) ->
  P a b self

abs (A: I -> Type) (t : (i : I) -> A i): Path A (t i0) (t i1)
  λP. λabs. abs t

This encoding allows us to derive other Path primitives as functions.
Path application
Path application allows us to apply a Path A a b to an i : I and get either a or b. Since Path's only constructor is the path abstraction, then app is just the identity:
app (A : I -> Set) (a : A i0) (b : A i1) (e : Path A a b) (i : I) : A i
  i A a b e

Path reflexivity
We can implement refl, as expected, as a constant path:
refl (A : Set) (x : A) : Path (λi. A) x x
  λP. λabs. abs (λi. x)

Path congruence
We can apply a function to both sides of a Path:
cong (A : Set) 
     (B : A -> Set)
     (x : A)
     (y : A)
     (f : ∀ (a : A) -> B(a))
     (p : Path (λi. A) x y)
     : Path (λi. B (app (λi. A) x y p i)) (f x) (f y)
  λP. λabs. abs (λi. f (app (λi. A) x y p i))

Function extensionality
As expected, funext is very simple for the Path type. We just create a path abstraction that flips i and x:
funext
  (A : Type)
  (B : A -> Type)
  (f : ∀(x : A) -> B x)
  (g : ∀(x : A) -> B x)
  (h : ∀(x : A) -> Path (λi. B x) (f x) (g x))
  : Path (λi. ∀(x : A) -> B x) f g
  abs (λi. ∀(x : A) -> B x) (λi. λx. app (λi. B x) (f x) (g x) (h x) i)

Transport
Now the problem. While Path is great to work with, in order to be a reasonable equality type, we need a transport operation. Defining that seems to be non-trivial. After consulting the Cubical Agda paper, I've managed to implement its transport and transpPi:
transp (A : I -> Set) (i : I) (x : A i0) : A i1
  ?transp

transport (A : Set) (B : Set) (p : Path (λi. Set) A B) (a : A) : B
  transp (λi. app (λi. Set) A B p i) i0 a

transpPi (A : I -> Set) (B : (i : I) -> A(i) -> Set) (f : (x : A i0) -> B i0 x) (x : A i1) : B i1 x
  let fx : B i0 (transp _ i0 x)
         = f (transport (A i1) (A i0) (abs (λi. Set) (λi. A (not i))) x)
      be : Path (λi. Set) (B i0 (transp _ i0 x)) (B i1 (transp _ i1 x))
         = abs (λi. Set) (λj. B j (transp (λi. A (max (not i) j)) j x)
  in transport _ _ be fx

But as for transp, I do not know what to do. Agda says it is a primitive and isn't precise about how it computes. It does say, though, that transp _ i1 x = x; but that requires A to be constant when i = i1, otherwise we'd have x : A i0 and x : A i1 simultaneously, which is ill-typed! This is the first problem: we can't enforce that a function is constant on CoC+Self alone; replicating that would require some "hardcoded" access to a "count_variable_uses(x, term)" function. The second problem is that, on the i0 case, seems like we'd need to type-case on A i0, in order to specialize x : A i0 as x : ∀ (k : P i0) -> Q i0 k and then call transpPi. The nice thing is, since the only type former is Pi, this would complete the proof. But how would such type-case primitive work?
Questions
Finally, my questions are.

Since, in CoC+Self, inside transp, we can't enforce that A is constant when i=i1, is there any other to write transp that doesn't require such ability?

Is my reasoning that type-case is necessary to "pattern-match" on A i0 : Type right? If so, what is the correct elimination rule for Type?

How exactly transp computes? The paper mentioned affirms that transp _ i1 x = x, but what about the other two cases (transp _ i0 x and transp _ ie x)? Is it possible to write how they would look like (even if just as a pseudo-code)?


(You can type-check the proofs above using this file and Formality.)

**Tags:** type-theory, lambda-calculus, calculus-of-constructions, homotopy-type-theory

> **Comments:**
> **username_1**: What are the categorical semantics of Self types?  
> **username_2**: I see the type of your `Nat` refers to `Nat`.  Do you have a reference for why/where/when this kind if "recursion" is sound?  
> **username_0**: @MikeShulman I don't know, check Aaron Stump's original paper for a more formal presentation.  
> **username_0**: @username_2 the usage of `Nat` in `Nat` is necessary for Scott Encodings. I don't think it makes sense to reason about the soundness of a particular feature in isolation, it depends on the language on which said feature is inserted. Looking for sound languages that admit Scott Encodings might provide some answer to your question. Some may want to avoid Scott in favor of Church encodings which are easier to deal with, but I personally find that a mistake.  
> **username_2**: @username_0: my question was indeed if you could point me to a sound language that admits this kind of encoding  
> **username_0**: @username_2 I'm not aware of many proven sound languages that use Scott Encodings though. Lambda encodings in general are very unpopular (sadly).  
> **username_2**: I can't see use of the Scott encoding in Aaron's paper on self-types (he seems to use the Church encoding), which is why I'm wondering if there is a language which admits this kind of recursion and is sound (or can you get the same result via something like induction-recursion?)  
> **username_0**: @username_2 you won't find anything merely because nobody did it, but there is no reason to believe a language with self-types and structural recursion wouldn't be consistent; that's basically Coq, just simplified.  
> **username_2**: @username_0: structural recursion, I agree.  But definitions whose type refers to the definition itself is a completely different matter.  

---

## 1 answers

### Answer by username_3 on 2020-09-21. Score: 10

This is not an answer but a very long comment.

I find the idea quite interesting. To keep things focused, I think it would be very good to have a clear idea of what it means for the encoding of cubical type theory to be correct, namely that it is *sound* and *conservative*.

Soundness just means you can encode everything (for instance, that you did not forget to encode `cong`) and that all the expected judgmental equalities (conversions) that are supposed to hold do hold. This should be the easy part.

Conservativity means that the encoding cannot do more than what it is supposed to. Suppose `A` is a type in cubical type theory and let `A'` be its encoding using self-types. Then we want

> *If `A'` is inhabited in type theory with self-types then `A` is inhabited in cubical type theory.*

And given another type `B` encoded by `B'`, we want:

> *If `A' ≣ B'` in type theory with self-types then `A ≣ B'` in cubical type theory.*

I would particularly worry about the interval type `I`. In cubical type theory this is *not a type*! It is a pre-type that is treated specially. However, you are encoding it as an ordinary type, just like any other, and that sounds very fishy. I think there is a proof in cubical type theory showing that `I` cannot be an ordinary type but I don't remember it off the top of my head.

> **Comments:**
> **username_0**: I agree. From my experience, it makes sense that `I` cannot be an ordinary type, and I think I even see where things would break down: "transp" seems to require a "typecase" that treats "I" in a very "special" way. Regardless, the fact that all the definitions above behave identically to the "hardcoded" cubical primitives makes me think that, if we look into it further, we may find some "clever way" to let these definitions be internal libraries, keeping the language implementation itself minimal, which is my ultimate goal.  
> **username_0**: For example, perhaps there is a whole class of "special types" (not just `I`) that can be "lifted" out of self-encodings into something that is more "part of the language". Or not, but answering that question even negatively (as in, "Interval **must** be a primitive") would give me insights about its nature (and then I'd accept it as a primitive on Formality :P). Regardless, I find it very unlikely that "transp" as a primitive will turn out to be the simplest way to add cubical features to a proof language.  
> **username_3**: At the very least all the cubes `I ⨉ I ⨉ ... ⨉I` are special also. I do not think the interval must be special, but there should be distinction between pre-types and types. I wonder how exactly Cubical Agda gets around this.  
> **username_0**: Yep, seems like `I` is special exactly in the sense that a `I` in the context isn't like a normal variable in context. I hope I can get a deeper understanding of "why" and "how" it differs precisely.  
> **username_3**: The semantic answer is that it's not a Kan cubical set, i.e., it is not fibered.  
> **username_2**: Is it sufficient to make `I` live in another universe?  In my toy language, I use `Bool` for `I` but require my "evidence functions" treat their Bool argument as erased/implicit (in the sense of ICC/ICC*)  
> **username_3**: Using `Bool` for `I` is a bit like the tricks employed in Coq and Agda to fake the interval. They rely on abstraction, i.e., hiding the lie behind a mechanism that prevents looking at the definition.  
> **username_4**: Cubical Agda does treat `I` as a type but it does not presume that all types are fibrant. In particular `I` does not support `transp` or `hcomp`: [page 19](https://pure.itu.dk/portal/files/84649948/icfp19main_p164_p.pdf)  

---

