# Type theory with indexed equality - the theory

Published: 2018-01-04T21:18Z
Tags: hott, ttie
This post is literate Agda

In a previous post I introduced the TTIE language, along with a type checker and interpreter. My motivation for writing that (aside from it being fun!) was to explore the type system. At the time I started this project, formalizing this system as a shallow embedding in Agda was not easy. But with the addition of a rewriting mechanism, it has become much easier to use Agda without going insane from having to put substitutions everywhere. So, in this post I will formalize the TTIE type system.

This post is literate Agda, and uses my own utility library. The utility library mainly defines automatic rewrite rules like trans x (sym x) refl, which make life a bit more pleasant. All these rewrites use the standard library propositional equality , which I will call meta equality. . All these rewrites use the standard library propositional equality, which I will denote as and call meta equality.

```{-# OPTIONS --rewriting #-}
module _ where

open import Util.Equality as Meta using (_∎) renaming (_≡_ to _⟹_; refl to □; _≡⟨_⟩_ to _⟹⟨_⟩_; _≡⟨_⟩⁻¹_ to _⟸⟨_⟩_)
open import Data.Product
open import Data.Sum
open import Data.Nat using (ℕ; zero; suc)
open import Data.Vec
open import Function
open import Level renaming (zero to lzero; suc to lsuc)
```

First we postulate the existence of the interval. I will abbreviate the interval type as I.

```postulate I : Set
postulate i₀ : I
postulate i₁ : I
```

The canonical eliminator for the interval needs equalities, to show that i₀ and i₁ are mapped to equal values. But we haven't defined those yet. However, there is one eliminator that we can define, namely into I, since values in I are always equal.

```postulate icase : I → I → I → I
postulate icase-i₀ : ∀ a b → icase a b i₀ ⟹ a
postulate icase-i₁ : ∀ a b → icase a b i₁ ⟹ b
{-# REWRITE icase-i₀ icase-i₁ #-}
```

And with this icase construct, we can define conjunction, disjunction, and negation

```_&&_ : I → I → I
i && j = icase i₀ j i

_||_ : I → I → I
i || j = icase j i₁ i

inot : I → I
inot = icase i₁ i₀
```

We can define some extra computation rules based on the principle that when evaluating icase a b c, if we use the a branch then c = i₀, and similarly for b.

```postulate icase-same : ∀ (a b c : I → I) d → a i₀ ⟹ c i₀ → b i₁ ⟹ c i₁
→ icase (a d) (b d) d ⟹ c d

icase-const : ∀ a b → icase a a b ⟹ a
icase-id    : ∀ a   → icase i₀ i₁ a ⟹ a
icase-i₀-x  : ∀ b   → icase i₀ b b ⟹ b
icase-i₁-x  : ∀ b   → icase i₁ b b ⟹ i₁
icase-x-i₀  : ∀ a   → icase a i₀ a ⟹ i₀
icase-x-i₁  : ∀ a   → icase a i₁ a ⟹ a

Show implementationicase-const a b = icase-same (const a) (const a) (const a) b □ □
icase-id    a   = icase-same (const i₀) (const i₁) id a □ □
icase-i₀-x  b   = icase-same (const i₀) id id b □ □
icase-i₁-x  b   = icase-same (const i₁) id (const i₁) b □ □
icase-x-i₀  a   = icase-same id (const i₀) (const i₀) a □ □
icase-x-i₁  a   = icase-same id (const i₁) id a □ □

{-# REWRITE icase-const #-}
{-# REWRITE icase-id #-}
{-# REWRITE icase-i₀-x #-}
{-# REWRITE icase-i₁-x #-}
{-# REWRITE icase-x-i₀ #-}
{-# REWRITE icase-x-i₁ #-}
```

## The equality type

We can now define the indexed equality type

```data Eq {a} (A : I → Set a) : A i₀ → A i₁ → Set a where
refl : ∀ (x : (i : I) → A i) → Eq A (x i₀) (x i₁)
```

For convenience we write the non-indexed object level equality as

```_≡_ : ∀ {a} {A : Set a} → A → A → Set a
_≡_ {A = A} x y = Eq (\_ → A) x y
```

And now that we have equalities, we can write down the the general dependent eliminator for the interval,

```postulate _^_ : ∀ {a A x y} → Eq {a} A x y → (i : I) → A i
postulate ^-i₀   : ∀ {a A x y} x≡y → _^_ {a} {A} {x} {y} x≡y i₀ ⟹ x
postulate ^-i₁   : ∀ {a A x y} x≡y → _^_ {a} {A} {x} {y} x≡y i₁ ⟹ y
postulate ^-refl : ∀ {a A} x → _^_ {a} {A} {x i₀} {x i₁} (refl x) ⟹ x
{-# REWRITE ^-i₀ ^-i₁ ^-refl #-}
infixl 6 _^_
```

At the same time, the _^_ operator also functions as an eliminator for Eq, projecting out the argument to refl. This also means that we have the following eta contraction rule

```refl-eta : ∀ {a A x y} (x≡y : Eq {a} A x y) → refl (\i → x≡y ^ i) ⟹ x≡y -- HIDE a
refl-eta (refl x) = □
{-# REWRITE refl-eta #-}
```

These definitions are enough to state some object level theorems, such as function extensionality

```ext′ : ∀ {a} {A B : Set a} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g -- HIDE a
ext′ f≡g = refl \i → \x → f≡g x ^ i
```

congruence,

```cong′ : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {x y} → x ≡ y → f x ≡ f y -- HIDE a|b
cong′ f x≡y = refl \i → f (x≡y ^ i)
```

and symmetry of ,

```sym′ : ∀ {a} {A : Set a} {x y : A} → x ≡ y → y ≡ x -- HIDE a
sym′ x≡y = refl \i → x≡y ^ inot i
```

We can also define dependent versions of all of the above, which are the same, only with more general types. I'll leave these as an exercise for the reader.

```spoilersym : ∀ {a} {A : I → Set a} {x y} → Eq A x y → Eq (A ∘ inot) y x
sym x≡y = refl \i → x≡y ^ inot i
```

## Transport

In general, to make full use of equalities, you would use substitution, also called transport. I will formalize this as

```postulate tr : ∀ {a} (A : I → Set a) → A i₀ → A i₁ -- HIDE a
```

Where tr stands for transport, since we transport a value of type A i₀ along A, to a value of type A i₁. This should be possible, because there is a path between i₀ and i₁, that is, they are indistinguishable, and because functions are continuous. So A is a continuous path between A i₀ and A i₁. In a previous blog post I have used a more general cast primitive, which can be defined in terms of tr,

```cast : ∀ {a} (A : I → Set a) → (j₀ j₁ : I) → A j₀ → A j₁ -- HIDE a
cast A j₀ j₁ = tr (\i → A (icase j₀ j₁ i))
```

And now we can define things like the usual substitution

```subst : ∀ {a b} {A : I → Set a} (B : {i : I} → A i → Set b) {x} {y} → Eq A x y → B x → B y -- HIDE a|b
subst B xy = tr (\i → B (xy ^ i))
```

and the J axiom

```jay : ∀ {A : Set} {x : A} (B : {y : A} → x ≡ y → Set) → {y : A} → (x≡y : x ≡ y)
→ B (refl (\_ → x)) → B x≡y
jay B xy = tr (\i → B {xy ^ i} (refl \j → xy ^ (j && i)))
```

Yay, jay!

## Evaluating transport

To be useful as a theory of computation, all primitives in our theory should reduce. In particular, we need to know how to evaluate tr, at least when it is applied to arguments without free variables. We do this by pattern matching on the first argument of tr, and defining transport for each type constructor.

The simplest case is if the type being transported along doesn't depend on the index at all

```postulate tr-const : ∀ {a} {A : Set a} {x} → tr (\_ → A) x ⟹ x -- HIDE a
{-# REWRITE tr-const #-}
```

Much more interesting is the case when the type is a function type. To cast function types, we first transport the argument 'back', apply the function, and then transport the result forward. First look at the non-dependent case, i.e. going from A i₀ B i₀ to A i₁ B i₁:

```postulate tr-arrow : ∀ {a b} {A : I → Set a} {B : I → Set b} {f} -- HIDE a|b
→ tr (\i → A i → B i) f
⟹ (\x → tr B (f (cast A i₁ i₀ x)))
```

The dependent case is a bit more complicated, since the type of the result depends on the transported argument. The result of the function has type B i₀ (cast A i₁ i₀ x), and we have to transport this to B i₁ x. So as we go from i₀ to i₁, we want to "undo" the cast operation. We can do this by changing both i₀'s to i₁'s, to get a value of the type B i₁ (cast A i₁ i₁ x). Because cast A i₁ i₁ xx by icase-const and tr-const, this is equivalent to B i₁ x.

```postulate tr-pi : ∀ {a b} {A : I → Set a} {B : (i : I) → (A i) → Set b} {f} -- HIDE a|b
→ tr (\i → (x : A i) → B i x) f
⟹ (\x → tr (\i → B i (cast A i₁ i x)) (f (cast A i₁ i₀ x)))
```

Besides function/pi types, there are also product/sigma types. The idea here is similar: transport both parts of the pair independently. Again, the type of the second part can depend on the transported first part,

```postulate tr-sigma : ∀ {a b} {A : I → Set a} {B : (i : I) → A i → Set b} {x y} -- HIDE a|b
→ tr (\i → Σ (A i) (B i)) (x , y)
⟹ (tr A x , tr (\i → B i (cast A i₀ i x)) y)
```

Finally, let's look at sum types, for which we use simple recursion,

```postulate tr-sum₁ : ∀ {a b} {A : I → Set a} {B : I → Set b} {x} -- HIDE a|b
→ tr (\i → A i ⊎ B i) (inj₁ x) ⟹ inj₁ (tr A x)
postulate tr-sum₂ : ∀ {a b} {A : I → Set a} {B : I → Set b} {x} -- HIDE a|b
→ tr (\i → A i ⊎ B i) (inj₂ x) ⟹ inj₂ (tr B x)
```

## Transport for equality types

The final type constructors in our language are equality types, and this is where things get more hairy. The idea is that a type like Eq A x y behaves like A in many respects. Its values will just be wrapped in a refl constructor.

Consider the case of equalities over (dependent) function types. The evaluation rule could look like

```postulate tr-eq-pi
: ∀ {a b} {A : I → I → Set a} -- HIDE a|b
{B : ∀ i j → A i j → Set b} -- HIDE a|b
{u : ∀ i → (x : A i i₀) → B i i₀ x}
{v : ∀ i → (x : A i i₁) → B i i₁ x}
{f₀ : Eq (\j → (x : A i₀ j) → B i₀ j x) (u i₀) (v i₀)}
→ tr (\i → Eq (\j → (x : A i j) → B i j x) (u i) (v i)) f₀
⟹ refl \j → \x →
let x' = \i' j' → tr (\i → A (icase i₁ i' i) (icase j j' i)) x in
(tr (\i → Eq (\j' → B i j' (x' i j')) (u i (x' i i₀)) (v i (x' i i₁)))
(refl \j' → (f₀ ^ j') (x' i₀ j'))) ^ j
```

Of course the A in Eq A x y could again be an equality type, and we would have to repeat the construction. To do this systematically, I start by collecting all the 'sides' of the equality type recursively. For example the sides of Eq (\i Eq (\j _) x y) u v) are eq (\i eq (\j done) x y) u v,

```mutual
data Sides {a} : ∀ n (A : Vec I n → Set a) → Set (lsuc a) where
done : ∀ {A} → Sides zero A
eq   : ∀ {n A}
→ (sides : (i : I) → Sides n (\is → A (i ∷ is)))
→ Eqs (sides i₀)
→ Eqs (sides i₁)
→ Sides (suc n) A

Eqs : ∀ {a n A} → Sides {a} n A → Set a
Eqs {A = A} done = A []
Eqs {A = A} (eq sides x y) = Eq (\i → Eqs (sides i)) x y
```

Since I A are the continuous functions out of the 1-dimensional interval, you can think of a Vec I n A as a continuous function out of the n-dimensional hypercube. So in geometric terms, we can draw such a function as assigning a value to all elements of the hypercube. Similarly, you can think of Sides {n = n} as a function out of the n-dimensional hypercube with the central cell removed, and Eqs as filling in that central cell.

 Eqs 0 Sides 1 Eqs 1 Vec I 1 → A Sides 2 Eqs 2 Vec I 2 → A

I will spare you the details, see the source code of this post if you are interested. Suffice to say, that if we generalize _^_, icase, etc. from I to Vec I n and from Eq to Eqs, then we can generalize tr-eq-pi to arbitrarily deep Eqs.

```tr-eqs-pi-rhs : ∀ {a b n} {A : I → Vec I n → Set a} -- HIDE a|b
{B : (i : I) → (is : Vec I n) → A i is → Set b} -- HIDE a|b
→ (sides : (i : I) → Sides n (\js → (x : A i js) → B i js x))
→ Eqs (sides i₀)
→ Eqs (sides i₁)
```
```postulate tr-eqs-pi : ∀ {a b n}
{A : I → Vec I n → Set a}
{B : (i : I) → (is : Vec I n) → A i is → Set b}
(sides : (i : I) → Sides n (\js → (x : A i js) → B i js x))
(f₀ : Eqs (sides i₀))
→ tr (Eqs ∘ sides) f₀
⟹ tr-eqs-pi-rhs sides f₀
```

You can do a similar thing for sigma types, except that the types get even messier there because we need a dependently typed map function for Eqs and Sides.

This is the evaluation strategy implemented in the current TTIE interpreter. But it has two issues: 1) it is error prone and ugly 2) we still haven't defined tr (Eq Set u v)

What remains is to define tr (Eq Set u v).

Note that transitivity can be defined by transporting along an equality,

```trans′ : ∀ {a} {A : Set a} {x y z : A} → x ≡ y → y ≡ z → x ≡ z -- HIDE a
trans′ {y = y} x≡y y≡z = tr (\i → (x≡y ^ inot i) ≡ (y≡z ^ i)) (refl \_ → y)
```

There are several ways to generalize this to dependent types. I'll use a variant that is explicit about the type

```trans : ∀ {a} (A : I → I → Set a) {x y z} -- HIDE a
→ Eq (\i → A i₀ i) x y
→ Eq (\i → A i i₁) y z
→ Eq (\i → A i i) x z
trans A {y = y} x≡y y≡z = tr (\i → Eq (\j → A (icase i₀ i j) (icase (inot i) i₁ j)) (x≡y ^ inot i) (y≡z ^ i)) (refl \_ → y)
```

Just as transitivity can be defined in terms of tr, the converse is also true. Instead of specifying transport for nested equality types, we could define tr for Eq types in terms of transitivity and symmetry.

The most general case of such a transport is

```xy = fw (\i → Eq (\j → A i j) (ux ^ i) (vy ^ i)) uv
```

where

```ux : Eq (\i → A i i₀) u x
vy : Eq (\i → A i i₁) v y
uv : Eq (\j → A i₀ j) u v
```

which we can draw in a diagram as

If you ignore the types for now, it seems obvious that

```xy = trans (trans ((sym ux) uv) vy)
```

So, we could take

```postulate tr-eq : ∀ {a} {A : I → I → Set a} -- HIDE a
(ux : ∀ i → A i i₀)
(vy : ∀ i → A i i₁)
(uv : Eq (A i₀) (ux i₀) (vy i₀))
→ tr (\i → Eq (A i) (ux i) (vy i)) uv
⟹ trans (\i j → A (icase i₁ i j) (icase i i j))
(refl (ux ∘ inot)) (trans A uv (refl vy))
```

I will stick to taking tr as primitive. However, this definition will come in handy for defining transport along paths between types.

## Inductive types

It is straightforward to extend the theory with inductive types and higher inductive types. Here are some concrete examples, taken from the HoTT book.

### The homotopy circle

```postulate Circle : Set
postulate point  : Circle
postulate loop   : Eq (\_ → Circle) point point
postulate Circle-elim : ∀ {a} {A : Circle → Set a} -- HIDE a
→ (p : A point)
→ (l : Eq (\i → A (loop ^ i)) p p)
→ (x : Circle) → A x
```

with the computation rules

```postulate elim-point : ∀ {a A p l} → Circle-elim {a} {A} p l point ⟹ p -- HIDE a
postulate elim-loop  : ∀ {a A p l i} → Circle-elim {a} {A} p l (loop ^ i) ⟹ l ^ i -- HIDE a
{-# REWRITE elim-point #-}
{-# REWRITE elim-loop #-}
```

Technically we would also need to specify elim for transitive paths (or paths constructed with tr). First the non-dependent version,

```postulate Circle-elim′-tr-eq : ∀ {a A p l} (x y : I → Circle) xy i -- HIDE a
→ Circle-elim {a} {\_ → A} p l (tr (\j → x j ≡ y j) xy ^ i) -- HIDE a
⟹ tr (\j → Circle-elim {a} {\_ → A} p l (x j) -- HIDE a
≡ Circle-elim {a} {\_ → A} p l (y j)) -- HIDE a
(refl \k → Circle-elim {a} {\_ → A} p l (xy ^ k)) ^ i -- HIDE a

```

To write down the dependent version, it is helpful to first define a generalized version of transport over equality types. This generalized equality transport doesn't just give the final path, but also any of the sides, depending on the argument. Fortunately, it can be defined in terms of the existing transport primitive tr.

```treq : ∀ {a} (A : I → I → Set a) -- HIDE a
→ (x : ∀ i → A i i₀) (y : ∀ i → A i i₁) (xy : Eq (\j → A i₀ j) (x i₀) (y i₀))
→ (i j : I) → A i j
treq A x y xy i j = tr (\k → Eq (A (i && k)) (x (i && k)) (y (i && k))) xy ^ j
```

Note that we have

```treq-i-i₀ : ∀ {a} A x y xy i → treq {a} A x y xy i i₀ ⟹ x i -- HIDE a
treq-i-i₁ : ∀ {a} A x y xy i → treq {a} A x y xy i i₁ ⟹ y i -- HIDE a
treq-i₀-j : ∀ {a} A x y xy j → treq {a} A x y xy i₀ j ⟹ xy ^ j -- HIDE a
treq-i₁-j : ∀ {a} A x y xy j → treq {a} A x y xy i₁ j ⟹ tr (\i → Eq (A i) (x i) (y i)) xy ^ j -- HIDE a
```

Now the dependent version of commuting Circle-elim for transitive paths looks like this:

```postulate Circle-elim-tr-eq : ∀ {a A p l} (x y : I → Circle) xy i -- HIDE a
→ Circle-elim {a} {A} p l (tr (\j → x j ≡ y j) xy ^ i)
⟹ tr (\j → Eq (\k → A (treq _ x y xy j k))
(Circle-elim {a} {A} p l (x j))
(Circle-elim {a} {A} p l (y j)))
(refl \k → Circle-elim {a} {A} p l (xy ^ k)) ^ i
```

We also need to continue this for higher paths, but that should be straightforward, if tedious.

```tedious next step...postulate Circle-elim-tr-eq-eq : ∀ {a A p ll} (x y : I → I → Circle) -- HIDE a
(xy₀ : ∀ k → x k i₀ ≡ y k i₀) (xy₁ : ∀ k → x k i₁ ≡ y k i₁)
xy i j
→ Circle-elim {a} {A} p ll (tr (\k → Eq (\l → x k l ≡ y k l) (xy₀ k) (xy₁ k)) xy ^ i ^ j)
⟹ tr (\k → Eq (\l → Eq (\m → A (tr (\k' → Eq (\l' → x (k && k') l' ≡ y (k && k') l')
(xy₀ (k && k'))
(xy₁ (k && k'))) xy ^ l ^ m) )
(Circle-elim {a} {A} p ll (x k l))
(Circle-elim {a} {A} p ll (y k l)))
(refl \l → Circle-elim {a} {A} p ll (xy₀ k ^ l))
(refl \l → Circle-elim {a} {A} p ll (xy₁ k ^ l)))
(refl \k → refl \l → Circle-elim {a} {A} p ll (xy ^ k ^ l)) ^ i ^ j
```

### Truncation

```postulate Truncate : Set → Set
postulate box  : ∀ {A} → A → Truncate A
postulate same : ∀ {A} x y → Eq (\_ → Truncate A) x y

module _ {p} {A} {P : Truncate A → Set p} -- HIDE p
(b : (x : A) → P (box x))
(s : ∀ {x y} (px : P x) (py : P y) → Eq (\i → P (same x y ^ i)) px py) where

postulate Truncate-elim : (x : Truncate A) → P x

postulate elim-box  : ∀ x → Truncate-elim (box x) ⟹ b x
postulate elim-same : ∀ x y i → Truncate-elim (same x y ^ i)
⟹ s (Truncate-elim x) (Truncate-elim y) ^ i
```

Notice that in the eliminator for every path constructor, we expect an argument of type P "along that path constructor".

### Quotient types

```postulate _/_      : (A : Set) → (R : A → A → Set) → Set
postulate quot     : ∀ {A R} → A → A / R
postulate eqn      : ∀ {A R} → (x y : A) → R x y → Eq (\_ → A / R) (quot x) (quot y)
postulate truncate : ∀ {A R} → (x y : A / R) → (r s : Eq (\_ → A / R) x y) → r ≡ s

module _ {A R} {P : A / R → Set}
(q : (x : A) → P (quot x))
(e : ∀ {x y} → (r : R x y) → Eq (\i → P (eqn x y r ^ i)) (q x) (q y))
(t : ∀ {x y r s}
→ (px : P x) (py : P y) (pr : Eq (\i → P (r ^ i)) px py) (ps : Eq (\i → P (s ^ i)) px py)
→ Eq (\i → Eq (\j → P (truncate x y r s ^ i ^ j)) px py) pr ps) where

postulate /-elim : (x : A / R) → P x

postulate elim-quot : ∀ x → /-elim  (quot x) ⟹ q x
postulate elim-eqn  : ∀ x y r i → /-elim (eqn x y r ^ i) ⟹ e r ^ i
postulate elim-truncate : ∀ x y r s i j
→ /-elim (truncate x y r s ^ i ^ j)
⟹ t (/-elim x) (/-elim y) (refl \k → /-elim (r ^ k)) (refl \k → /-elim (s ^ k)) ^ i ^ j
```

### Indexed types

One caveat to the support of inductive types are indexed types. These are the types with parameters whose value can depend on the constructor, written after the colon in Agda. An obvious example is the standard inductive equality type as it is defined in the standard library,

```data _≡_ {A : Set} (x : A) : A → Set where
refl : x ⟹ x
```

Another example are length indexed vectors,

```data Vec (A : Set) : ℕ → Set where
[] : Vec A zero
_∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)
```

Such inductive types introduce a new kind of equality, and we can't have that in TTIE.

Fortunately, outlawing such definitions is not a big limitation, since any indexed type can be rewritten to a normal inductive type by making the equalities explicit. For example

```data Vec (A : Set) (n : ℕ) : Set where
[] : n ≡ zero → Vec A n
_∷_ : ∀ {m} → A → Vec A m → n ≡ suc m → Vec A n
```

## Univalence

The final ingredient to turn TTIE into a homotopy type theory is the univalence axiom. A univalence primitive might look like this:

```postulate univalence : ∀ {a} {A B : Set a} -- HIDE a
→ (f : A → B)
→ (g : B → A)
→ (gf : ∀ x → g (f x) ≡ x)
→ (fg : ∀ x → f (g x) ≡ x)
→ (fgf : ∀ x → cong′ f (gf x) ≡ fg (f x))
→ Eq (\_ → Set a) A B -- HIDE a
```

By using an equality constructed with univalence in a transport, you can recover the forward and backward functions,

```fw : ∀ {a} {A B : Set a} → A ≡ B → A → B -- HIDE a
fw A≡B = tr (_^_ A≡B)

bw : ∀ {a} {A B : Set a} → A ≡ B → B → A -- HIDE a
bw A≡B = tr (_^_ A≡B ∘ inot)
```

as well as the proofs of left and right-inverse,

```bw∘fw : ∀ {a} {A B : Set a} → (A≡B : A ≡ B) → ∀ x → bw A≡B (fw A≡B x) ≡ x -- HIDE a
bw∘fw A≡B x = refl \j → tr (\i → A≡B ^ icase (inot j) i₀ i)
(tr (\i → A≡B ^ icase i₀ (inot j) i) x)

fw∘bw : ∀ {a} {A B : Set a} → (A≡B : A ≡ B) → ∀ x → fw A≡B (bw A≡B x) ≡ x -- HIDE a
fw∘bw A≡B x = refl \j → tr (\i → A≡B ^ icase j i₁ i)
(tr (\i → A≡B ^ icase i₁ j i) x)
```

Here the trick is that when j = i₁, the transports become the identity, while otherwise they become fw and bw.

Getting out the adjunction fgf is a bit harder. You need to come up with an expression that reduces to f (gf x ^ k) when j = i₀ and that reduces to (fg (f x) ^ k) when j = i₁. The following does the trick

```not-quite-fw∘bw∘fw : ∀ {a} {A B : Set a} → (A≡B : A ≡ B) → ∀ x -- HIDE a
→ cong′ (fw A≡B) (bw∘fw A≡B x) ≡ fw∘bw A≡B (fw A≡B x)
not-quite-fw∘bw∘fw A≡B x = refl \j →
refl \k → tr (\i → A≡B ^ icase                          (icase i₀ k j) i₁ i)
\$ tr (\i → A≡B ^ icase    (icase (inot k) i₁ j) (icase i₀ k j)    i)
\$ tr (\i → A≡B ^ icase i₀ (icase (inot k) i₁ j)                   i) x)
```

but the type is not right. We want an equality between two equalities, both of type fw (bw (fw x)) x. But instead we get a dependent equality type that mirrors the body of the definition.

To resolve this, we need to add another reduction rule to the language, which states that if you transport from i₀ to i and then to i₁, this is the same as going directly from i₀ to i₁. This should hold regardless of what i is.

```postulate tr-tr : ∀ {a} (A : I → Set a) i x → tr (A ∘ icase i i₁) (tr (A ∘ icase i₀ i) x) ⟹ tr A x -- HIDE a
postulate tr-tr-i₀ : ∀ {a} A x → tr-tr {a} A i₀ x ⟹ □ -- HIDE a
postulate tr-tr-i₁ : ∀ {a} A x → tr-tr {a} A i₁ x ⟹ □ -- HIDE a
{-# REWRITE tr-tr-i₀ tr-tr-i₁ #-}
```
```fw∘bw∘fw : ∀ {a} {A B : Set a} → (A≡B : A ≡ B) → ∀ x
→ cong′ (fw A≡B) (bw∘fw A≡B x) ≡ fw∘bw A≡B (fw A≡B x)
fw∘bw∘fw A≡B x =
-- same as above, with ugly rewriting details...  Meta.subst id (cong-Eq
(ext \j → cong-Eq □ □ (tr-tr (\i → A≡B ^ i) (j) x)) □ □)
(refl \j → refl \k
→ tr (\i → A≡B ^ icase                          (icase i₀ k j) i₁ i)
\$ tr (\i → A≡B ^ icase    (icase (inot k) i₁ j) (icase i₀ k j)    i)
\$ tr (\i → A≡B ^ icase i₀ (icase (inot k) i₁ j)                   i) x)
```

### Computation rules

The computation rules are now obvious: when fw, bw, etc. are applied to a univalence primitive, return the appropriate field.

```module _ {a} {A B} f g gf fg fgf (let AB = univalence {a} {A} {B} f g gf fg fgf) where -- HIDE a
postulate tr-univalence-f : ∀ x → tr (\i → AB ^ i) x ⟹ f x
postulate tr-univalence-g : ∀ x → tr (\i → AB ^ inot i) x ⟹ g x
{-# REWRITE tr-univalence-f #-}
{-# REWRITE tr-univalence-g #-}

postulate tr-univalence-gf : ∀ x j
→ tr (\i → AB ^ icase j i₀ i) (tr (\i → AB ^ icase i₀ j i) x)
⟹ gf x ^ inot j
postulate tr-univalence-fg : ∀ x j
→ tr (\i → AB ^ icase j i₁ i) (tr (\i → AB ^ icase i₁ j i) x)
⟹ fg x ^ j
{-# REWRITE tr-univalence-gf #-}
{-# REWRITE tr-univalence-fg #-}
-- tr-univalence-fgf ommitted
```

Ideally, we would be able to compute tr for AB ^ f i for any function f, and even

```tr (\i → AB ^ f1 i) ∘ ⋯ ∘ tr (\i → AB ^ fn i)
```

But we quickly run into problems. Consider

```  problem : I → I → A → B
problem j k = tr (\i → AB ^ icase k i₁ i)
∘ tr (\i → AB ^ icase j k i)
∘ tr (\i → AB ^ icase i₀ j i)
```

When j=i₁, this reduces to

```problem i₁ k = fg ^ k ∘ f
```

and when k=i₀, it reduces to

```problem j i₀ = f ∘ gf ^ j
```

These two types look a lot like the adjunction fgf, but there are two differences: 1. For the two reductions of problem to be confluent, the two right hand sides should be equal in the meta language (judgementally equal). But an adjunction inside the theory doesn't guarantee this.

2. Even when using fgf, we can not get an expression for problem with the right reductions. The issue is that depending on j and k, problem can represent any of the following compositions

```problem i₀ i₀ = f  ∘ id ∘ id
problem i₀ i₁ = id ∘ f  ∘ id
problem i₁ i₀ = f  ∘ g  ∘ f
problem i₁ i₁ = id ∘ id ∘ f
```

### Transporting univalent paths

Finally, we also need to decide how to transport along equality types involving univalence. As I showed previously, transporting along equalities can be defined in terms of transitivity. So that is what we will do here. The idea is that to transport along trans AB BC, you first transport along AB, and then along BC. The same goes for other directions of using this transitive path (bw, fw∘bw, etc.)

```module _ {a} {A B C : Set a} (A≡B : A ≡ B) (B≡C : B ≡ C) where
trans-f : A → C
trans-f = fw B≡C ∘ fw A≡B

trans-g : C → A
trans-g = bw A≡B ∘ bw B≡C

trans-gf : ∀ x → trans-g (trans-f x) ≡ x
trans-gf x = cong′ (bw A≡B) (bw∘fw B≡C (fw A≡B x)) ⟨ trans′ ⟩ bw∘fw A≡B x

trans-fg : ∀ x → trans-f (trans-g x) ≡ x
trans-fg x = cong′ (fw B≡C) (fw∘bw A≡B (bw B≡C x)) ⟨ trans′ ⟩ fw∘bw B≡C x

postulate trans-fgf : ∀ x → cong′ trans-f (trans-gf x) ≡ trans-fg (trans-f x)
-- trans-fgf should be provable, but proof is omitted here

trans-equivalence : A ≡ C
trans-equivalence = univalence trans-f trans-g trans-gf trans-fg trans-fgf
```

And we use this transitivity to define transport,

```postulate tr-eq-Set : ∀ {a} (A B : I → Set a) (A₀≡B₀ : A i₀ ≡ B i₀)
→ tr (\i → Eq (\_ → Set a) (A i) (B i)) A₀≡B₀
⟹ trans-equivalence (refl (A ∘ inot)) (trans-equivalence A₀≡B₀ (refl B))

-- spacial case for fw
tr-tr-eq-Set : ∀ {a} (A B : I → Set a) (A₀≡B₀ : A i₀ ≡ B i₀) x
→ tr (\j → tr (\i → Eq (\_ → Set a) (A i) (B i)) A₀≡B₀ ^ j) x
⟹ tr B (tr (_^_ A₀≡B₀) (tr (A ∘ inot) x))
tr-tr-eq-Set A B A₀≡B₀ x = Meta.cong (\A₁≡B₁ → tr (_^_ A₁≡B₁) x) (tr-eq-Set A B A₀≡B₀)
```

Note that tr-eq-Set cannot be used as a rewrite rule. Agda incorrectly complains about universe levels, and when removing those the rule is accepted, but the file takes more than 10 minutes to type check.

### Reduction rules spoiled by univalence

While we are at it, it would be nice if we could add some additional judgemental equalities to the type system. For instance, trans xy (sym xy) = refl \_ x should hold for all xy.

However, we can not add this as a reduction. The reason is that for paths build with univalence, transporting along the left hand side reduces to bw∘fw, and this is not necessarily the same as reflexivity. Here is an example

```-- A path that flips the interval in one direction, but not in the other
-- so fw ∘ bw ≠ refl
flip-I : I ≡ I
flip-I = univalence id inot
(\i → refl (icase (inot i) i))
(\i → refl (icase (inot i) i))
(\i → refl \_ → refl (icase (inot i) i))

module _ (trans-sym : ∀ {a A x y} xy → trans′ {a} {A} {x} {y} xy (sym xy) -- hide {a}
⟹ (refl \_ → x)) where
problem2 : i₀ ⟹ i₁
problem2 =
Meta.begin
i₀
⟸⟨ tr-tr-eq-Set (_^_ flip-I ∘ inot) (_^_ flip-I ∘ inot) (refl \_ → I) i₁ ⟩
tr (\i → trans′ flip-I (sym flip-I) ^ i) i₁
⟹⟨ Meta.cong (\AB → tr (\i → AB ^ i) i₁) (trans-sym flip-I) ⟩
i₁
∎
```

tr (\i trans flip-I (sym flip-I) ^ i) i₁ evaluates to i₁ with tr-eq-Set, since we follow the equivalence backward and then forward. But according to trans-sym it is an identity path, and so this expression evaluates to i₀. So, we have a term that can evaluate to either i₀ or to i₁, depending on the evaluation order. In other words, reduction is no longer confluent.

This might not seem too bad, since i₀ i₁ inside the theory. But note that the reduction relation is not a homotopy equality. And it might even be untyped if we were using an untyped meta-theory, like the Haskell TTIE implementation. With a non-confluent reduction relation, it is easy to break the type system,

```flip-Bool : Bool ≡ Bool
flip-Bool = univalence not not not-not not-not not-not-not

bad : i₀ ⟹ i₁ → (Bool , false) ⟹ (_,_ {B = id} Bool true)
bad x = Meta.cong {B = Σ Set id} (\i → flip-Bool ^ i , tr (\j → flip-Bool ^ i && j) false) x

worse : i₀ ⟹ i₁ → ⊥
... | ()
```

So, trans-sym is out.

Another seemingly sensible reduction is that cong f (trans xy yz) trans (cong f xy) (cong f yz). But, if we also postulate that all paths over the interval can be defined in terms of icase, we end up in the same problematic situation.

```module _ (trans-cong : ∀ {a b A B x y z} (f : A → B) xy yz -- HIDE a|b
→ cong′ f (trans′ {a} {A} {x} {y} {z} xy yz) -- HIDE a
⟹ trans′ {b} (cong′ f xy) (cong′ f yz)) -- HIDE b
(tr-eq-I : ∀ (j k : I → I) jk₀ → tr (\i → Eq (\_ → I) (j i) (k i)) jk₀
⟹ refl (icase (j i₁) (k i₁))) where
trans-sym : ∀ {a A x y} xy → trans′ {a} {A} {x} {y} xy (sym xy) ⟹ (refl \_ → x) -- HIDE a
trans-sym {x = x} xy =
Meta.begin
trans′ xy (sym xy)
⟸⟨ trans-cong (_^_ xy) (refl id) (refl inot) ⟩
cong′ (\i → xy ^ i) (trans′ (refl id) (refl inot))
⟹⟨ Meta.cong (cong′ (_^_ xy)) (tr-eq-I inot inot (refl \_ → i₁)) ⟩
refl (\_ → x)
∎

problem3 : i₀ ⟹ i₁
problem3 = problem2 trans-sym
```

I don't have any solution to these problems, aside from not adding the problematic reductions.

Reductions that do seem fine are those involving only a single path. For instance, things like trans xy (refl \_ y) ⟹ xy.

## Conclusion

What I have presented is the type theory with indexed equality. As mentioned before, there is also a prototype implementation in Haskell.

The theory is quite similar to the cubical system, but it is developed mostly independently.

Some area's I haven't discussed or investigated yet, and some issues with the theory are:

1. Transitive paths involving HIT path constructors are not reduced, so trans loop (sym loop) is not the same as refl \_ point, however, the two are provably equal inside the theory. As with a general trans-sym rule, adding such a reduction would break confluence.

2. I have defined a function treq that generalizes tr (Eq ..). This could be taken as a primitive instead of tr. In that case we should further generalize it to take Sides, so that it also works for higher paths.

3. It is possible to combine transports to write terms that do not reduce, for example

```x : A
AB : A ≡ B
f : A → Set
y : f (bw AB (fw AB x))
tr (\i → f (tr (\j → AB ^ icase (inot i) i₀ j)
(tr (\j → AB ^ icase i (inot i) j)
(tr (\j → AB ^ icase i₀ i j) x)))) y
```

the tr-tr rule handles one such case, but more are possible. For well-behaved equalities flatting all this out is not a problem, but with univalence the intermediate steps become important.

4. I am not entirely happy with univalence breaking confluence in combination with trans-sym. It means that you have to be really careful about what, seemingly benign, reductions are allowed.

## Comment

 Name Homepage (optional) Email (optional. The email adress is stored and used for subscription notification. It will not be shared with third parties or used for anything else.) Subscribe to comments on this article Human? Name a function of type [[a]] -> [a]:
Use > code for code blocks, @code@ for inline code. Some html is also allowed.