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.
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.
Comment