qiitCross

-- CROSS-QIIT constructions: each data item below builds on the
-- previous ones through their Nova-level reflections.

-- 1. the free monoid (lists) and its abelianization (bags)
data ( L : U
     ; lnil : El L
     ; lcons : El ℕ → El L → El L )

data [a : 𝕌] ( Bag : U
             ; bnil : El Bag
             ; bins : El a → El Bag → El Bag
             ; bswp : (x : El a) (y : El a) (m : El Bag) → bins x (bins y m) ≡ bins y (bins x m) ∈ El Bag )

-- 2. elimination INTO a QIIT: bag append — the motive is the Bag code
--    itself, and the coherence is exactly the swap lemma
def bapp : (a : 𝕌) → El (Bag a) → El (Bag a) → El (Bag a) ≔
  λa. λm. λn. BagElim _ (λw. Bag a) n (λx. λr. λih. bins a x ih) (λx. λy. λr. λih. ⋆) m

-- 3. a map BETWEEN QIITs: the order-forgetting quotient map L → Bag ℕ
def toBag : El L → El (Bag ℕ) ≔
  λt. LElim (λw. Bag ℕ) (bnil _) (λx. λr. λih. bins _ x ih) t

-- toBag coequalizes adjacent transpositions (the universal property's
-- defining triangle, at the generators): by β + the swap lemma
def toBagSwap : (x : El ℕ) (y : El ℕ) (t : El L) →
                toBag (lcons x (lcons y t)) ≡ toBag (lcons y (lcons x t)) ∈ El _ ≔
  λx. λy. λt. ⋆

-- 4. a QIIT whose signature EMBEDS a previous QIIT's reflection: trees
--    with bag-of-naturals labels (El (Bag ℕ) is an external domain
--    carrying the whole Bag signature inside it)
data ( P : U
     ; leaf : El (Bag ℕ) → El P
     ; node : El P → El P → El P )

-- flatten a tree by appending its bags — elimination whose methods use
-- the previous eliminator-derived function
def flatten : El P → El (Bag ℕ) ≔
  λp. PElim (λw. Bag ℕ) (λb. b) (λl. λihl. λr. λihr. bapp _ ihl ihr) p

-- computation across all three QIITs at once
def two : El (Bag ℕ) ≔ bins _ Z (bins _ (S Z) (bnil _))
def flatTest : flatten (node (leaf (toBag (lcons Z lnil))) (leaf (bins _ (S Z) (bnil _))))
               ≡ two ∈ _ ≔ ⋆