In this post I would like to present the type theory I have been working on, where the usual equality is replaced by an equality type indexed by the homotopy interval. This results in ideas very similar to those from the cubical system. I have a prototype implementation of this system in Haskell, which you can find on github. The system is unimaginatively called TTIE, a type theory with indexed equality. In this post I will focus on the introducing the type system and its implementation. I save the technical details for another post.

To recap: I have previously written about the 'indexed equality' type. The idea is that if we have the homotopy interval type with two points and a path between them,

-- Pseudo Agda notation data Interval : Type where 0 : Interval 1 : Interval 01 : Eq _ 0 1

then we can then define a type of equality, 'indexed' by the interval:

data Eq (A : Interval → Type) : A 0 → A 1 → Type where refl : (x : (i : Interval) → A i) → Eq A (x 0) (x 1)

Rather than using lambdas all the time in the argument of `Eq` and `refl`, in TTIE I write the bound variable in a subscript. So `refl _{i} (x i)` means

Now the (dependent) eliminator for the interval is

iv : ∀ {A} → {x : A 0} → {y : A 1} → (xy : Eq_{i}(A i) x y) → (i : Interval) → A i iv {A} {x} {y} xy 0 = x iv {A} {x} {y} xy 1 = y iv {A} {x} {y} (refl_{i}(xy i)) i = xy i refl_{i}(iv {A} {x} {y} xy i) = xy

For readability, I write `iv xy i` as `xy ^{i}`.
This combination already makes it possible to prove, for instance, congruence of functions without needing to use substitution (the J rule):

cong : ∀ {A B x y} → (f : A → B) → Eq_{i}A x y → Eq_{i}B (f x) (f y) cong f xy = refl_{i}(f xy^{i})

this can be generalized to dependent types

cong : ∀ {A B x y} → (f : (x : A) → B x) → (xy : Eq_{i}A x y) → Eq_{i}(B xy^{i}) (f x) (f y) cong f xy = refl_{i}(f xy^{i})

And we also get extensionality up to eta equality:

ext : ∀ {A B f g} → ((x : A) → Eq_{i}(B x) (f x) (g x)) → Eq_{i}((x : A) → B x) (\x → f x) (\x → g x) ext fg = refl_{i}(\x → (fg x)^{i})

So far, however, we can not yet represent general substitution. I have found that the most convenient primitive is

cast : (A : I → Type) → (i : Interval) → (j : Interval) → A i → A j

where `cast _{i} A 0 0 x = x` and

This generalized cast makes all kinds of proofs really convenient.
For instance, we would like that `cast A 1 0 ∘ cast A 0 1 = id`.
But it is already the case that `cast A 0 0 ∘ cast A 0 0 = id`. So we just have to change some of those 0s to 1s,

lemma : ∀ {A : Type} {x} → Eq _ (cast_{i}A 1 0 (cast_{i}A 0 1 x)) x lemma {A} {x} = cast_{j}(Eq _ (cast_{i}A j 0 (cast_{i}A 0 j x)) x) 0 1 (refl_{i}x)

As another example, most type theories don't come with a built in dependent or indexed equalty type. Instead, a common approach is to take

Eq_{i}(A i) x y = Eq (A 0) x (cast_{i}(A i) 1 0 y)

or

Eq_{i}(A i) x y = Eq (A 1) (cast_{i}(A i) 0 1 x) y

We can prove that these are equivalent:

lemma' : ∀ {A} {x y} → Eq Type (Eq (A 0) x (cast_{i}(A i) 1 0 y)) (Eq_{i}(A i) x y) lemma' {A} {x} {y} = refl_{j}(Eq_{k}(A (j && k)) x (cast_{i}(A i) 1 j y))

where `i && j` is the and operator on intervals, i.e.

_&&_ : Interval → Interval → Interval 0 && j = 0 1 && j = j i && 0 = 0 i && 1 = i

We can even go one step further to derive the ultimate in substitution, the J axiom:

J : ∀ {A : Type} {x : A} → (P : (y : A) → Eq A x y → Type) → (y : A) → (xy : Eq A x y) → P x (refl x) → P y xy J P y xy pxy = cast_{i}(P xy^{i}(refl_{j}(xy^(j && i)))) 0 1 pxy

With the TTIE implementation, you can type check the all of the above examples. The implementation comes with a REPL, where you can ask for types, evaluate expressions, and so on. Expressions and types can have holes, which will be inferred by unification, like in Agda.

On the other hand, this is by no means a complete programming language. For example, there are no inductive data types. You will instead have to work with product types (`x , y : A * B`) and sum types (`value foo x : data {foo : A; bar : B}`). See the readme for a full description of the syntax.

## Comments

I find this a bit strange. With equality types it should be possible to state that

trueandfalseare not equal. In ordinary type theory this would be the typeId bool true false -> empty, and this type is indeed inhabited. How do you do the same thing in your approach?What I find odd is that normally the equality type on

Ais dependent overA * A, but here it is dependent overI -> A. Since there is no map fromItoboolthat would take0tofalseand1totrue, I do not see how to form the typeId bool false true.In TTIE you can prove that false is not equal to true in much the same way as other dependent type theories. That is, by substitution into a function that gives the empty type for one case and the unit type for another case:

The indexed equality type is of the form

Eq : (A : I → Type) → A 0 → A 1 → Type. This is a strict generalization of the usual equality type. When you take the first argument to be a constant function, you get back the non-indexed equality:So you can still form

Eq (\_ → Bool) false truejust fine. The only 'inhabitants' of this type are functions that take 0 to false and 1 to true, of which there are none. So this equality type is uninhabited, as it should be, since false is not equal tot true.Oops, I totally misread the type of

Eq! I read the first argument asI -> Ainstead ofA : I -> Type. Never mind, sorry for the noise.## Reply