Solution to @effectfully's RecN challenge

RecN-challenge.agda

-- Challenge: https://github.com/effectfully/random-stuff/blob/master/RecN-challenge.agda
{-# OPTIONS --type-in-type #-}  -- Just for convenience, not essential.

open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Base

coerce : ∀ {A B} -> A ≡ B -> A -> B
coerce refl = id

record KitRecN : Set where
  field
    RecN : ℕ -> Set
    recN : ∀ n -> RecN n

    Rec0-correct
      : RecN 0
      ≡ ∀ {R} -> (∀ {Q} -> Q -> Q) -> R -> R
    Rec1-correct
      : RecN 1
      ≡ ∀ {A R} -> (∀ {Q} -> (A -> Q) -> Q) -> (A -> R) -> R
    Rec2-correct
      : RecN 2
      ≡ ∀ {A B R} -> (∀ {Q} -> (A -> B -> Q) -> Q) -> (A -> B -> R) -> R
    Rec3-correct
      : RecN 3
      ≡ ∀ {A B C R} -> (∀ {Q} -> (A -> B -> C -> Q) -> Q) -> (A -> B -> C -> R) -> R

    rec0-correct
      : (λ {R} -> coerce Rec0-correct (recN 0) {R})
      ≡ λ k f -> f
    rec1-correct
      : (λ {A R} -> coerce Rec1-correct (recN 1) {A} {R})
      ≡ λ k f -> f (k λ x -> x)
    rec2-correct
      : (λ {A B R} -> coerce Rec2-correct (recN 2) {A} {B} {R})
      ≡ λ k f -> f (k λ x y -> x) (k λ x y -> y)
    rec3-correct
      : (λ {A B C R} -> coerce Rec3-correct (recN 3) {A} {B} {C} {R})
      ≡ λ k f -> f (k λ x y z -> x) (k λ x y z -> y) (k λ x y z -> z)

open KitRecN

-- forallN n K = ∀ {A₁ .. An} → K (λ R → A₁ → .. → An → R) (λ x a₁ .. an → x)
forallN : ℕ → ((F : Set → Set) → (∀ {R} → R → F R) → Set) → Set
forallN zero    K = K (λ Q → Q) (λ x → x)
forallN (suc n) K = ∀ {A} → forallN n λ BC=> const → K (λ Q → A → BC=> Q) λ r x → const r

mapForallN : ∀ {K H} → (n : ℕ) →
             (∀ {F} {const : ∀ {R} → R → F R} → K F const → H F const) →
             forallN n K → forallN n H
mapForallN zero    f g = f g
mapForallN (suc n) f g = mapForallN n f g

kitRecN : KitRecN
kitRecN .RecN n       = forallN n λ ABC=> _ → ∀ {R} → (∀ {Q} → ABC=> Q → Q) → ABC=> R → R
kitRecN .recN zero    = λ _ z → z
kitRecN .recN (suc n) = mapForallN n (λ {BC=>} {const} rec {R} k f →
                                        rec (λ selᵢ → k λ _ → selᵢ)
                                            (f (k λ x → const x)))
                                   (kitRecN .recN n)
kitRecN .Rec0-correct = refl
kitRecN .Rec1-correct = refl
kitRecN .Rec2-correct = refl
kitRecN .Rec3-correct = refl
kitRecN .rec0-correct = refl
kitRecN .rec1-correct = refl
kitRecN .rec2-correct = refl
kitRecN .rec3-correct = refl