title: cong from refl in univalent OTT
subtitle: ... and hence subst from refl
date: 2013-07-04 18:00 CEST
source link: This post is literate Agda, get the source
language: agda
tags: agda, hott
literate style: latex
\begin{code}
-- HIDDEN
-- this is the same stuff as last time
module cong-from-refl where
open import Level
open import Function
open import Data.Unit
open import Data.Bool
open import Data.Empty
open import Data.Product
open import Relation.Binary.PropositionalEquality as Meta using (_≡_)
postulate Path : ∀ {a} → (A : Set a) → A → A → Set a
postulate refl : ∀ {a} → (A : Set a) → (x : A) → Path A x x
postulate Path-⊤ : Path ⊤ tt 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 b} (A : Set a) (B : A → Set b) → Set (a ⊔ b)
Π A B = (x : A) → B x
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)
\end{code}
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:
\begin{code}
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))
\end{code}
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?