List2nat

Test.agda

{-# OPTIONS --safe #-}
module Test where

open import Prelude
open import Data.Unit
open import Data.Nat
open import Data.List

private variable
  ℓᵃ ℓᵇ : Level
  A : 𝒰 ℓᵃ
  B : 𝒰 ℓᵇ

record wmap (A : 𝒰 ℓᵃ) (B : 𝒰 ℓᵇ) : 𝒰 (ℓᵃ ⊔ ℓᵇ) where
  constructor mkwmap
  field
    f : A → B
    h : B → A
    r : h retraction-of′ f

open wmap public
    
wtransp : (w : wmap A B) → ∀ a → fibre (w .h) a
wtransp (mkwmap f h r) a = f a , r a

nat2list : ℕ → List ⊤
nat2list  zero   = []
nat2list (suc n) = tt ∷ nat2list n

list2nat : List ⊤ → ℕ
list2nat  []      = 0
list2nat (tt ∷ l) = suc (list2nat l)

ln-coh : nat2list retraction-of′ list2nat
ln-coh  []      = refl
ln-coh (tt ∷ l) = ap (tt ∷_) (ln-coh l)

wlist : wmap (List ⊤) ℕ
wlist .f = list2nat
wlist .h = nat2list
wlist .r = ln-coh

hmor-++-+ : ∀ m n → nat2list m ++ nat2list n ＝ nat2list (m + n)
hmor-++-+  zero   n = refl
hmor-++-+ (suc m) n = ap (tt ∷_) (hmor-++-+ m n)

example : {p q : List ⊤} → p ++ q ＝ q ++ p
example {p} {q} =
  let (m , ep) = wtransp wlist p
      (n , eq) = wtransp wlist q
    in
    ap² _++_ (ep ⁻¹) (eq ⁻¹)
  ∙ hmor-++-+ (list2nat p) _
  ∙ ap nat2list (+-comm (list2nat p) _)
  ∙ hmor-++-+ (list2nat q) _ ⁻¹
  ∙ ap² _++_ eq ep