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 ⟹ aShow implementation
icase-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₁ #-}
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.
spoiler
sym : ∀ {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
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!
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₁ x ⟹ x 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)
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.
It is straightforward to extend the theory with inductive types and higher inductive types. Here are some concrete examples, taken from the HoTT book.
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
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".
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
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
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)
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
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.
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₁ → ⊥ worse x with bad x ... | ()
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.
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