cong from refl in univalent OTT

Published: 2013-07-04T16:00Z
Tags: agda, hott
This post is literate Agda, get the source

This is a follow up on last week's post. There I showed that in a univalent Observational Type Theory, you can derive subst from cong. Now I am going to go one step further.

Suppose we change the definition of paths for functions from

Path (A  B) f g   x  f x  g x

to

Path (A  B) f g   {x y}  x  y  f x  g y

Then for a function f, refl f is actually the same thing as cong f!. So that's one less primitive to worry about. In fact the only two path related primitives that remain are Path and refl. The rest is just in the computation rules.

Here are the changes in the agda code compared to last week:

postulate Path-→ :  {a b} {A : Set a} {B : Set b} (f g : A  B)
                  Path (A  B) f g
                  ((x y : A)  Path A x y  Path B (f x) (g y))
-- cong = refl cong : {a b} {A : Set a} {B : Set b} (f : A B) {x y} Path A x y Path B (f x) (f y) cong f x=y = Meta.subst id (Path-→ f f) (refl _ f) _ _ x=y
-- subst is the same as last time 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
-- and paths for dependent functions postulate Path-Π : {a b} {A : Set a} {B : A Set b} (f g : Π A B) Path (Π A B) f g ((x y : A) (pa : Path A x y) Path (B y) (subst B pa (f x)) (g y))

Of course this doesn't really change anything, since defining refl for function types is no easier than defining cong.

Representation

You might also notice that for all types A (except Set), the structure of Path A is essentially the same as that of A. In fact, for a (non-indexed) data type

data Foo : Set where
  foo₀ : Foo
  foo₁ : A  Foo
  foo₂ : Foo  Foo  Foo

you can mechanically derive its path type to be

data Path Foo : Foo  Foo  Set where
  refl-foo₀  : Path (foo₀ x) (foo₀ x)
  cong₁-foo₁ :  {x x'}  Path A x x'  Path Foo (foo₁ x) (foo₁ x')
  cong₂-foo₂ :  {x x' y y'}  Path Foo x x'  Path Foo y y'
                               Path Foo (foo₂ x y) (foo₂ x' y')

In theory this allows for a nice implementation trick: we can take the representation of x and refl x to be the same. So for example 5 : Path Int 5 5 is a path that asserts that 5 = 5, and it is the only such path.

Originally I thought that an implementation would have to pass cong f along with every parameter f of a function type (which would suck). But in this way we don't have to, since f and cong f are the same function.

This also corresponds nicely to the idea that extra path constructors can be added in Higher Inductive Types. But I am not quite sure yet how that works out.

Food for thought

Comment

(optional)
(optional, will not be revealed)
0 + 3 =
Use > code for code blocks, @code@ for inline code. Some html is also allowed.