ord.ced

import stdlib.

module ords (U:Nat ➔ ★).

opaque U_zero_is_unit : TpEq·(U zero)·Unit = ●.

data Ord : ★ =
| base : Ord
| next : Π n:Nat. U n ➔ Ord.

nextProjCode : Ord ➔ Nat
= λ o. σ o {
  | base ➔ zero
  | next n u ➔ n
  }.

nextProj : Π o:Ord. U (nextProjCode o)
= λ o. σ o {
  | base ➔ cast -U_zero_is_unit.2 unit
  | next n u ➔ u
  }.


injNextTypeWitness : ∀ na:Nat. ∀ a:U na. ∀ nb:Nat. ∀ b:U nb.
  {next na a ≃ next nb b} ➾ {na ≃ nb}
= Λ na. Λ a. Λ nb. Λ b. Λ e.
  ρ e @ x. {nextProjCode x ≃ nextProjCode (next nb b)}
  - β.

injNextType : ∀ na:Nat. ∀ a:U na. ∀ nb:Nat. ∀ b:U nb.
  {next na a ≃ next nb b} ➾ Cast·(U na)·(U nb)
= Λ na. Λ a. Λ nb. Λ b. Λ e.
  ρ (injNextTypeWitness -na -a -nb -b -e)
  - castRefl·(U nb).

injNext : ∀ na:Nat. ∀ a:U na. ∀ nb:Nat. ∀ b:U nb.
  {next na a ≃ next nb b} ➾ {a ≃ b}
= Λ na. Λ a. Λ nb. Λ b. Λ e.
  ρ e @ x. {nextProj x ≃ nextProj (next nb b)}
  - β.