An inductive family puzzle

HitPuzzle.agda

{-# OPTIONS --cubical #-}
module HitPuzzle where
open import Cubical.Foundations.Everything
open import Cubical.Data.Empty
open import Cubical.Data.Sum
open import Cubical.Data.Sigma
open import Cubical.Data.Maybe
open import Cubical.Data.Nat

data Perm : Type → Type₁ where
  Zero : Perm ⊥
  Succ : ∀ {X} → Perm X → Perm (Maybe X)

RFin : ℕ → Type
-- This is Cubical.Data.Fin.Recursive
-- but the library doesn't have anything useful
RFin zero = ⊥
RFin (suc n) = Maybe (RFin n)
-- RFin n ≃ Fin n

size : ∀ {X} → Perm X → ℕ
size Zero = 0
size (Succ r) = suc (size r)

path : ∀ {X} (r : Perm X) → X ≡ RFin (size r)
path Zero = refl
path (Succ r) = cong Maybe (path r)

idPerm : ∀ n → Perm (RFin n)
idPerm zero = Zero
idPerm (suc n) = Succ (idPerm n)

toPerm : ∀ {X} n → X ≡ RFin n → Perm X
toPerm n p = subst Perm (sym p) (idPerm n)

toPermRefl : ∀ n → toPerm n refl ≡ idPerm n
toPermRefl n = transportRefl (idPerm n)

zig : ∀ {X} (p : Perm X) → toPerm (size p) (path p) ≡ p
zig Zero = transportRefl Zero  -- Regularity
zig (Succ p)
  = substCommSlice _ (Perm ∘ Maybe) (λ _ → Succ) _ (idPerm (size p))
  ∙ cong Succ (zig p)

zag-size-id : ∀ n → n ≡ size (idPerm n)
zag-size-id zero = refl
zag-size-id (suc n) = cong suc (zag-size-id n)

zag-path-id : ∀ n → cong RFin (zag-size-id n) ≡ path (idPerm n)
zag-path-id zero = refl
zag-path-id (suc n) i j = Maybe (zag-path-id n i j)

-- Slightly more general universes
-- To be PR'd
substInPaths' : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {a a' : A}
                 → (f g : A → B) → (p : a ≡ a') (q : f a ≡ g a)
                 → subst (λ x → f x ≡ g x) p q ≡ sym (cong f p) ∙ q ∙ cong g p
substInPaths' {a = a} f g p q =
  J (λ x p' → (subst (λ y → f y ≡ g y) p' q) ≡ (sym (cong f p') ∙ q ∙ cong g p'))
    p=refl p
    where
    p=refl : subst (λ y → f y ≡ g y) refl q
           ≡ refl ∙ q ∙ refl
    p=refl = subst (λ y → f y ≡ g y) refl q
           ≡⟨ substRefl {B = (λ y → f y ≡ g y)} q ⟩ q
           ≡⟨ (rUnit q) ∙ lUnit (q ∙ refl) ⟩ refl ∙ q ∙ refl ∎

zag-id : ∀ m → Path (Σ[ n ∈ ℕ ] RFin m ≡ RFin n) (size (idPerm m), path (idPerm m)) (m , refl)
zag-id m = sym $ ΣPathP (zag-size-id m ,
  toPathP
    ( substInPaths' (λ _ → RFin m) (λ n → RFin n) (zag-size-id m) refl
    ∙ cong (refl ∙_) (sym (lUnit _))
    ∙ sym (lUnit _)
    ∙ zag-path-id m))

theorem : ∀ {X} → Iso (Perm X) (Σ[ n ∈ ℕ ] X ≡ RFin n)
theorem .Iso.fun p = size p , path p
theorem .Iso.inv (n , p) = toPerm n p
theorem .Iso.leftInv = zig
theorem .Iso.rightInv (n , p) = J
  (λ X q → (size (toPerm n (sym q)) , path (toPerm n (sym q))) ≡ (n , (sym q)))
  (cong (λ u → (size u , path u)) (toPermRefl n) ∙ zag-id n)
  (sym p)