Deriving a nicer induction principle for equality

j-to-j.agda

{-# OPTIONS --without-K #-}
module j-to-j where
open import Level

-- Gives rise to the annoying induction principle.
data _≡_ {A : Set} : A → A → Set where
  refl : ∀ {a : A} → a ≡ a

-- Ignore the "Level" junk in here. It's needed because
-- we're trying to eliminate into a Set1 (U1 in Peter's
-- lectures). Otherwise it's quite boring.
J : {l : Level}{A : Set}(C : (a b : A) → a ≡ b → Set l)
  → ((a : A) → C a a refl)
  → (a b : A)(prf : a ≡ b) → C a b prf
J C base a .a refl = base a

-- This is the new J induction principle
-- but with all it's arguments in the wrong
-- order. All we've done is left non-dependent
-- arguments past each other.
delayed : {A : Set}(a b : A)(prf : a ≡ b)
        → (C : (b : A) → a ≡ b → Set)
        → C a refl
        → C b prf
delayed {A} a b prf =
  J (λ a b prf → (C : (b : A) → a ≡ b → Set)
               → C a refl
               → C b prf)
    (λ a C base → base) a b prf

-- We can thus define the actual ind. principle
-- as a trivial corollary.
new-J : {A : Set}(a : A)(C : (b : A) → a ≡ b → Set)
      → C a refl
      → (b : A)(prf : a ≡ b) → C b prf
new-J a C base b prf = delayed a b prf C base


-- The other direction is nice and simply, just
-- apply the motive to a in order to generate something
-- in the shape new-J expects.
j-from-new : {A : Set}(C : (a b : A) → a ≡ b → Set)
           → ((a : A) → C a a refl)
           → (a b : A)(prf : a ≡ b) → C a b prf
j-from-new C base a b prf = new-J a (C a) (base a) b prf

This is baffling and intriguing.

@Morkrom anything I can help clarify?