Substitution from congruence in univalent OTT

Published: 2013-06-22T14:51Z
Tags: agda, hott
License: CC-BY
This post is literate Agda, get the source

In this post I will show that in an univalence style observational type theory, it is enough to take congruence as a primitive, rather than the more complicated substitution or J axioms. This post is literate Agda, so here are some boring import declarations

module subst-from-cong where
open import Level open import Function open import Data.Unit open import Data.Bool open import Data.Empty open import Data.Product

I will be using the standard propositional equality as a meta equality,

open import Relation.Binary.PropositionalEquality as Meta using (__)

while postulating a path type (equality type) and its computation rules for me to prove things about,

postulate Path :  {a}  (A : Set a)  A  A  Set a
postulate refl :  {a}  (A : Set a)  (x : A)  Path A x x

The idea of Observational Type Theory (OTT) is that Path is actually defined by case analysis on the structure of the argument type. For the finite types this is simple, there is a path if and only if the values are the same,

postulate Path-⊤ : Pathtt tt 
postulate Path-Bool00 : Path Bool false false postulate Path-Bool01 : Path Bool false true postulate Path-Bool10 : Path Bool true false postulate Path-Bool11 : Path Bool true true

A path for functions is a function to paths, which also means that we have functional extensionality.

Π :  {a b} (A : Set a) (B : A  Set b)  Set (ab)
Π A B = (x : A)  B x
postulate Path-Π : {a b} {A : Set a} {B : A Set b} (f g : Π A B) Path (Π A B) f g ((x : A) Path (B x) (f x) (g x))

In their original OTT paper, Alternkirch defined equality for types also by structure matching. I.e. Π types are equal to Π types with equal arguments, Σ types are equal to Σ types, etc. But this is incompatible with the univalence axiom from Homotopy Type Theory. That axiom states that equivalent or isomorphic types are equal. So, what happens if we take isomorphism as our definition of equality between types?

Iso :  {a}  (A B : Set a)  Set a
Iso {a} A B
  = Σ (A  B) \fw 
    Σ (B  A) \bw 
    ( x  Path A (bw (fw x)) x) ×
    ( y  Path B (fw (bw y)) y)
id-Iso : {a} (A : Set a) Iso A A id-Iso A = (id , id , refl A , refl A)
postulate Path-Type : {a} (A B : Set a) Path (Set a) A B Lift {a} {suc a} (Iso A B)

Now suppose that we have a congruence, i.e. that all functions preserve paths. So from a path between x and y, we can construct a path between f x and f y for any function f.

-- we have congruence for non-dependent functions
postulate cong :  {a b} {A : Set a} {B : Set b}
                (f : A  B)   {x y}  Path A x y  Path B (f x) (f y)

Then this is enough to define substitution, since the paths for a type B x are isomorphisms, and we can apply these in the forward direction

subst :  {a b} {A : Set a} (B : A  Set b) {x y : A}  (Path A x y)  B x  B y
subst B {x} {y} p with Meta.subst id (Path-Type (B x) (B y)) (cong B p)
... | lift (fw , bw , _ , _) = fw

With substitution we can now finally define what paths are for dependent Σ types. A path between pairs is a pair of paths,

postulate Path-Σ :  {a b} {A : Set a} {B : A  Set b} (x y : Σ A B)
                  Path (Σ A B) x y
                  Σ (Path A (proj₁ x) (proj₁ y))
                     (\pa  Path (B (proj₁ y)) (subst B pa (proj₂ x)) (proj₂ y))

Substitution is not the most general eliminator for paths. It is not enough to prove properties about paths. For that we need the general induction principle for paths, often called J

J :  {a b} {A : Set a} {x : A}  (B : (y : A)  Path A x y  Set b)
   {y : A}  (p : Path A x y)  B x (refl A x)  B y p

Unfortunately, I was unable to prove J from just congruence. For that I needed an additional lemma,

postulate subst-refl :  {a} {A : Set a} {x y : A}  (p : Path A x y)
                      p  subst (Path A x) p (refl A x)

Since Path A is inductively defined, I believe that subst-refl should be provable by case analysis on A, but I have not yet done so. We can now implement J by using subst with a dependent pair. Note that here I have to manually apply the comptuation rules for Path (Σ _ _) and use the subst-refl lemma.

J {A = A} {x = x} B {y} p
  = subst (uncurry B)
      (Meta.subst id (Meta.sym $ Path-Σ (x , refl A x) (y , p)) $
      (p , Meta.subst (\q  Path (Path A x y) q p) (subst-refl p)
           (refl (Path A x y) p)))

Does it compute

An important question to ask is whether this style of OTT is actually implementable. We can certainly implement the definitions, but would they allow us to compute?

The type Path A certainly reduces, by definition. Similarly, it is not hard to implemenent refl. The hard part is defining what cong means for various functions, and then proving subst-refl. Somewhere in there we should put the fact that paths are transitive and symmetric, since we have not used that property so far. For what I have done up till now I could equally well have taken Iso A B = A B.

Here are the implementations of refl,

_≡[_]≡_ :  {a} {A B : Set a}  A  A  B  B  Set a
a ≡[ p ]≡ b = Meta.subst id p a  b
postulate refl-⊤ : refltt ≡[ Path-⊤ ]≡ tt refl-Bool0 : refl Bool false ≡[ Path-Bool00 ]≡ tt refl-Bool1 : refl Bool true ≡[ Path-Bool11 ]≡ tt refl-Π : {a b} {A : Set a} {B : A Set b} (f : Π A B) refl (Π A B) f ≡[ Path-Π f f ]≡ (\x refl (B x) (f x)) refl-Type : {a} (A : Set a) refl (Set a) A ≡[ Path-Type A A ]≡ lift (id-Iso A)

For refl (Σ _ _) we need yet another lemma, which is a bit a dual to subst-refl₁, allowing refl in the second argument instead of the third.

  subst-refl₁ :  {a b} {A : Set a} {B : A  Set b} {x : A} {y : B x}
               y  subst B (refl A x) y
refl-Σ : {a b} {A : Set a} {B : A Set b} (x : Σ A B) refl (Σ A B) x ≡[ Path-Σ x x ]≡ (refl A (proj₁ x) , Meta.subst (\x1 Path (B (proj₁ x)) x1 (proj₂ x)) (subst-refl₁ {B = B} {y = proj₂ x}) (refl (B (proj₁ x)) (proj₂ x)))

And here is a start of the implementation of cong,

  cong-const :  {a b} {A : Set a} {B : Set b} {x x'} {y} {p : Path A x x'}
              cong (\x  y) p  refl B y
  cong-id    :  {a} {A : Set a} {x x'} {p : Path A x x'}
              cong (\x  x) p  p
  cong-∘     :  {a b c} {A : Set a} {x x'} {p : Path A x x'}
                 {B : Set b} {C : Set c} {f : B  C} {g : A  B}
              cong (\x  f (g x)) p  cong f (cong g p)
  -- etc.

At some point I think you will also need a dependent cong.

But this is enough postulating for one day.


ThorstenDate: 2013-07-02T12:01Zx

Yes you are on the right track (I think). You can go further and observe that J is derivable from subst if equality forms a category. However, the details of derving cong are not easy...


(optional, will not be revealed)
What greek letter is usually used for anonymous functions?
Use > code for code blocks, @code@ for inline code. Some html is also allowed.