module NatCat where

open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Data.Fin hiding (_+_)
open import Data.Sum renaming (map to map⊎)
open import Data.Product renaming (map to map×)
open import Function 

split : ∀ {m n} -> Fin (m + n) -> Fin m ⊎ Fin n
split {zero} i = inj₂ i
split {suc n} zero = inj₁ zero
split {suc n} (suc i) = map⊎ suc id (split i)

glue : ∀ {m n} -> Fin m ⊎ Fin n -> Fin (m + n)
glue {zero} (inj₁ ())
glue {zero} (inj₂ y) = y
glue {suc n} (inj₁ zero) = zero
glue {suc n} (inj₁ (suc i)) = suc (glue {n} (inj₁ i))
glue {suc n} (inj₂ y) = suc (glue {n} (inj₂ y))

iso1 : ∀ {m n} (i : Fin (m + n)) -> glue {m} {n} (split i) ≡ i
iso1 {zero} i = refl
iso1 {suc n} zero = refl
iso1 {suc n} (suc i) with split {n} i | iso1 {n} i
iso1 {suc n}  (suc i) | inj₁ x | glueinj₁x≡i rewrite glueinj₁x≡i = refl
iso1 {suc n'} (suc i) | inj₂ y | glueinj₂y≡i rewrite glueinj₂y≡i = refl 

iso2 : ∀ {m n} (i : Fin m ⊎ Fin n) -> split {m} {n} (glue i) ≡ i
iso2 {zero} (inj₁ ())
iso2 {zero} (inj₂ y) = refl
iso2 {suc n} (inj₁ zero) = refl
iso2 {suc m} {n} (inj₁ (suc i)) rewrite iso2 {m} {n} (inj₁ i) = refl
iso2 {suc m} {n} (inj₂ y) rewrite iso2 {m} {n} (inj₂ y) = refl

proj : ∀ {m n} -> Fin (m * n) -> Fin m × Fin n
proj {zero} ()
proj {suc m} {n} f = [ (\ x -> zero , x) , (\ y -> map× suc id (proj {m} y)) ]′ (split {n} f)

comb : ∀{m n} -> Fin m × Fin n -> Fin (m * n)
comb {zero} (() , _)
comb {suc m} (zero , b) = glue (inj₁ b)
comb {suc m} {n} (suc a , b) = glue {n} (inj₂ (comb (a , b)))

iso21 : ∀ {m n} (i : Fin (m * n)) -> comb {m} {n} (proj i) ≡ i
iso21 {zero} ()
iso21 {suc m} {n} i with split {n} i | inspect (split {n}) i 
iso21 {suc m} {n} i | inj₁ x | [ eq ]  = trans (cong glue (sym eq)) (iso1 {n} i)
iso21 {suc m} {n} i | inj₂ y | [ eq ] = trans (cong (glue {n} ∘ inj₂) (iso21 {m} y)) (trans (cong (glue {n}) (sym eq)) (iso1 {n} i))

iso22 : ∀ {m n} (p : Fin m × Fin n) -> proj {m} {n} (comb p) ≡ p
iso22 {zero} (() , _) 
iso22 {suc m} {n} (zero , j) rewrite iso2 {n} {m * n} (inj₁ j) = refl
iso22 {suc m} {n} (suc i , j) rewrite iso2 {n} {m * n} (inj₂ (comb (i , j))) | iso22 {m} {n} (i , j) = refl