{-# OPTIONS --without-K #-}
module FinEq where

open import Data.Fin
open import Relation.Binary.HeterogeneousEquality -- only using the type
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Empty
open import Data.Unit

OffDiag : ∀ {n m} → Fin n → Fin m → Set
OffDiag zero    zero    = ⊥
OffDiag (suc _) (suc _) = ⊥
OffDiag _       _       = ⊤

inj-Fin-≅ : ∀ {n m} {i : Fin n} {j : Fin m} → i ≅ j → OffDiag i j → ⊥
inj-Fin-≅ {i = zero}  {zero} eq ()
inj-Fin-≅ {i = zero}  {suc j} ()
inj-Fin-≅ {i = suc i} {zero} ()
inj-Fin-≅ {i = suc i} {suc j} p ()

cast : ∀ {α} → {A B : Set α} (p : A ≡ B) (a : A) → B
cast refl a = a

intro : ∀ {A B : Set}{a b} → (eq : A ≡ B) → cast eq a ≡ b → a ≅ b
intro refl refl = refl

-- we can get these from univalence
postulate
  swap : Fin 2 ≡ Fin 2
  swap-lemma : cast swap zero ≡ suc zero

bottom : ⊥
bottom = inj-Fin-≅ (intro swap swap-lemma) _