# 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

• 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

 Name Homepage (optional) Email (optional, will not be revealed) Subscribe to comments on this article Human? Name a function of type [[a]] -> [a]:
Use > code for code blocks, @code@ for inline code. Some html is also allowed.