In this post I will show that in an univalence style observational type theory, it is enough to take congruence as a primitive, rather than the more complicated substitution or J axioms. This post is literate Agda, so here are some boring import declarations

module subst-from-cong where open import Level open import Function open import Data.Unit open import Data.Bool open import Data.Empty open import Data.Product

I will be using the standard propositional equality as a meta equality,

open import Relation.Binary.PropositionalEquality as Meta using (_≡_)

while postulating a path type (equality type) and its computation rules for me to prove things about,

postulate Path : ∀ {a} → (A : Set a) → A → A → Set a postulate refl : ∀ {a} → (A : Set a) → (x : A) → Path A x x

The idea of Observational Type Theory (OTT) is that `Path` is actually defined by case analysis on the structure of the argument type. For the finite types this is simple, there is a path if and only if the values are the same,

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 path for functions is a function to paths, which also means that we have functional extensionality.

Π : ∀ {a b} (A : Set a) (B : A → Set b) → Set (a ⊔ b) Π A B = (x : A) → B x postulate Path-Π : ∀ {a b} {A : Set a} {B : A → Set b} (f g : Π A B) → Path (Π A B) f g ≡ ((x : A) → Path (B x) (f x) (g x))

In their original OTT paper, Alternkirch et.al. defined equality for types also by structure matching. I.e. Π types are equal to Π types with equal arguments, Σ types are equal to Σ types, etc. But this is incompatible with the univalence axiom from Homotopy Type Theory. That axiom states that equivalent or isomorphic types are equal. So, what happens if we take isomorphism as our definition of equality between types?

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)

Now suppose that we have a congruence, i.e. that all functions preserve paths. So from a path between `x` and `y`, we can construct a path between `f x` and `f y` for any function `f`.

-- we have congruence for non-dependent functions postulate cong : ∀ {a b} {A : Set a} {B : Set b} → (f : A → B) → ∀ {x y} → Path A x y → Path B (f x) (f y)

Then this is enough to define substitution, since the paths for a type `B x` are isomorphisms, and we can apply these in the forward direction

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

With substitution we can now finally define what paths are for dependent Σ types. A path between pairs is a pair of paths,

postulate Path-Σ : ∀ {a b} {A : Set a} {B : A → Set b} (x y : Σ A B) → Path (Σ A B) x y ≡ Σ (Path A (proj₁ x) (proj₁ y)) (\pa → Path (B (proj₁ y)) (subst B pa (proj₂ x)) (proj₂ y))

Substitution is not the most general eliminator for paths. It is not enough to prove properties about paths. For that we need the general induction principle for paths, often called J

J : ∀ {a b} {A : Set a} {x : A} → (B : (y : A) → Path A x y → Set b) → {y : A} → (p : Path A x y) → B x (refl A x) → B y p

Unfortunately, I was unable to prove J from just congruence. For that I needed an additional lemma,

postulate subst-refl : ∀ {a} {A : Set a} {x y : A} → (p : Path A x y) → p ≡ subst (Path A x) p (refl A x)

Since `Path A` is inductively defined, I believe that `subst-refl` should be provable by case analysis on `A`, but I have not yet done so. We can now implement J by using `subst` with a dependent pair.
Note that here I have to manually apply the comptuation rules for `Path (Σ _ _)` and use the `subst-refl` lemma.

J {A = A} {x = x} B {y} p = subst (uncurry B) (Meta.subst id (Meta.sym $ Path-Σ (x , refl A x) (y , p)) $ (p , Meta.subst (\q → Path (Path A x y) q p) (subst-refl p) (refl (Path A x y) p)))

An important question to ask is whether this style of OTT is actually implementable. We can certainly implement the definitions, but would they allow us to compute?

The type `Path A` certainly reduces, by definition. Similarly, it is not hard to implemenent `refl`.
The hard part is defining what `cong` means for various functions, and then proving `subst-refl`.
Somewhere in there we should put the fact that paths are transitive and symmetric, since we have not used that property so far. For what I have done up till now I could equally well have taken `Iso A B = A → B`.

Here are the implementations of `refl`,

_≡[_]≡_ : ∀ {a} {A B : Set a} → A → A ≡ B → B → Set a a ≡[ p ]≡ b = Meta.subst id p a ≡ b postulate refl-⊤ : refl ⊤ tt ≡[ Path-⊤ ]≡ tt refl-Bool0 : refl Bool false ≡[ Path-Bool00 ]≡ tt refl-Bool1 : refl Bool true ≡[ Path-Bool11 ]≡ tt refl-Π : ∀ {a b} {A : Set a} {B : A → Set b} (f : Π A B) → refl (Π A B) f ≡[ Path-Π f f ]≡ (\x → refl (B x) (f x)) refl-Type : ∀ {a} (A : Set a) → refl (Set a) A ≡[ Path-Type A A ]≡ lift (id-Iso A)

For `refl (Σ _ _)` we need yet another lemma, which is a bit a dual to `subst-refl₁`, allowing `refl` in the second argument instead of the third.

postulate subst-refl₁ : ∀ {a b} {A : Set a} {B : A → Set b} {x : A} {y : B x} → y ≡ subst B (refl A x) y refl-Σ : ∀ {a b} {A : Set a} {B : A → Set b} (x : Σ A B) → refl (Σ A B) x ≡[ Path-Σ x x ]≡ (refl A (proj₁ x) , Meta.subst (\x1 → Path (B (proj₁ x)) x1 (proj₂ x)) (subst-refl₁ {B = B} {y = proj₂ x}) (refl (B (proj₁ x)) (proj₂ x)))

And here is a start of the implementation of `cong`,

postulate cong-const : ∀ {a b} {A : Set a} {B : Set b} {x x'} {y} {p : Path A x x'} → cong (\x → y) p ≡ refl B y cong-id : ∀ {a} {A : Set a} {x x'} {p : Path A x x'} → cong (\x → x) p ≡ p cong-∘ : ∀ {a b c} {A : Set a} {x x'} {p : Path A x x'} {B : Set b} {C : Set c} {f : B → C} {g : A → B} → cong (\x → f (g x)) p ≡ cong f (cong g p) -- etc.

At some point I think you will also need a dependent `cong`.

But this is enough postulating for one day.

## Comments

Yes you are on the right track (I think). You can go further and observe that J is derivable from subst if equality forms a category. However, the details of derving cong are not easy...

## Reply