Can we derive Cubical Type Theory from Self-Types?

Question

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.

1. 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?

2. 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?

3. 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.)

Answer 1

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.