The Coq mailing list

[Favonia <favonia AT gmail.com>]

I happened to implement an Agda module for higher-order paths (aka
identities, equalities) in homotopy type theory in order to prove
properties about nth sphere for arbitrary finite n. You can look at it
at

https://github.com/favonia/homotopy/blob/master/Path/Higher-order.agda
https://github.com/favonia/homotopy/blob/master/Space/Sphere.agda

This definition

Fixpoint identities (A : Type) (n : nat) : Prop :=
 match n with
   | O => True
   | S n' => forall (x y : A), identities (x = y) n'
 end.

is the same as "Endpoints′⇑" in my Agda implementation except that
mine uses Type, not Prop. (In general we want to avoid Prop-valued
equalities in HTT.) However in my experience this definition doesn't
work well for the exact reason Andrej mentioned. That is, I want to
perform induction from the right hand side (the highest layer), not
from the left hand side (the lowest layer). To accomplish this I fold
end points in the other way around. In Agda (sorry) I used mutual
recursion like this:

Endpoints⇑ : ∀ {ℓ} n → Set ℓ → Set ℓ
Path⇑ : ∀ {ℓ} n {A : Set ℓ} → Endpoints⇑ n A → Set ℓ

Endpoints⇑ {ℓ} 0 A = ↑ ℓ ⊤
Endpoints⇑ (suc n) A = Σ (Endpoints⇑ n A) (λ c → Path⇑ n c × Path⇑ n c)

Path⇑ 0 {A} _ = A
Path⇑ (suc n) (_ , x , y) = x ≡ y

where ≡ is the path type. I am sorry that my Coq-fu is not strong
enough to port the above definition to Coq, but I believe someone in
this mailing list is able to do so. The translated code (with
Prop-valued x = y) in my mind is

Fixpoint endpoints (n : nat) (X : Type) : Type :=
  match n return Type with
    | 0 => unit
    | S n => {e : endpoints n X & path n X e & path n X e}
  end
with path (n : nat) (X : Type) (e : endpoints n X) : Type :=
  match n return Type with
    | 0 => X
    | S n =>
      match e with
        | existT2 _ x y => x = y
      end
  end.

but Coq doesn't like "endpoints" showing up in the type signature of
path. Hope this helps.

Favonia