Monotonic map between finite ordinals

Mono.agda

module Monotone where

open import Data.Nat using (ℕ; zero; suc; z≤n; s≤s)
open import Data.Nat.Properties using ()
open import Data.Fin using (Fin; zero; suc; _≤_)
open import Relation.Binary.PropositionalEquality

data Mono : ℕ → ℕ → Set where
  nil : ∀ {n} → Mono zero n
  new : ∀ {n m} → Mono n       m       → Mono (suc n) (suc m)
  old : ∀ {n m} → Mono n       (suc m) → Mono (suc n) (suc m)

⟦_⟧ : ∀ {n m} → Mono n m → Fin n → Fin m
⟦ new m ⟧ zero    = zero
⟦ new m ⟧ (suc x) = suc (⟦ m ⟧ x)
⟦ old m ⟧ zero    = zero
⟦ old m ⟧ (suc x) = ⟦ m ⟧ x

isMonotone : ∀ {n m} (f : Mono n m) → (i j : Fin n) → i ≤ j → ⟦ f ⟧ i ≤ ⟦ f ⟧ j
isMonotone (new f) zero    j       0≤j       = z≤n
isMonotone (new f) (suc i) (suc j) (s≤s i≤j) = s≤s (isMonotone f i j i≤j)
isMonotone (old f) zero    j       0≤j       = z≤n
isMonotone (old f) (suc i) (suc j) (s≤s i≤j) = isMonotone f i j i≤j

-- This definition is filled by C-c C-a
_⨟_ : ∀ {n m p} → Mono n m → Mono m p → Mono n p
nil ⨟ g = nil
new f ⨟ new g = new (f ⨟ g)
old f ⨟ new g = old (f ⨟ new g)
old f ⨟ old g = old (f ⨟ old g)
new f ⨟ old g = old (f ⨟ g)

⨟-assoc : ∀ {n m p r} (f : Mono n m) (g : Mono m p) (h : Mono p r) → f ⨟ (g ⨟ h) ≡ (f ⨟ g) ⨟ h
⨟-assoc nil g f = refl
⨟-assoc (new f) (new g) (new h) = cong new (⨟-assoc f g h)
⨟-assoc (old f) (new g) (new h) = cong old (⨟-assoc f (new g) (new h))
⨟-assoc (new f) (old g) (new h) = cong old (⨟-assoc f g (new h))
⨟-assoc (old f) (old g) (new h) = cong old (⨟-assoc f (old g) (new h))
⨟-assoc (new f) (new g) (old h) = cong old (⨟-assoc f g h)
⨟-assoc (new f) (old g) (old h) = cong old (⨟-assoc f g (old h))
⨟-assoc (old f) (new g) (old h) = cong old (⨟-assoc f (new g) (old h))
⨟-assoc (old f) (old g) (old h) = cong old (⨟-assoc f (old g) (old h))