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.

- What is
`refl _→_`? - What is
`refl refl`? Does this even make sense? - For the representation of
`x : A`and`refl x`to be the same,`A`and`Path A x x`also need to have the same representation. That seems works for functions and inductive types, but what about`Set`? - Is
`Path`an applicative functor in some sense? With`refl`as return and`cong`as ap?

## Comment