gistfile1.idr

%default total

class Cardinality (a : Type) (n : Nat) where
  toFin         : a -> Fin n
  fromFin       : Fin n -> a
  bijective     : (a' : a) -> fromFin (toFin a') = a'
  bijective_inv : (f : Fin n) -> toFin (fromFin f) = f

data T = A | B | C

instance Cardinality T 3 where
  toFin A = fZ
  toFin B = fS fZ
  toFin C = fS $ fS fZ

  fromFin fZ               = A
  fromFin (fS fZ)          = B
  fromFin (fS (fS fZ))     = C
  fromFin (fS (fS (fS f))) = absurd f

  bijective A = refl
  bijective B = refl
  bijective C = refl

  bijective_inv fZ               = refl
  bijective_inv (fS fZ)          = refl
  bijective_inv (fS (fS fZ))     = refl
  bijective_inv (fS (fS (fS f))) = absurd f

instance Cardinality Bool 2 where
  toFin True  = fZ
  toFin False = fS fZ

  fromFin fZ          = True
  fromFin (fS fZ)     = False
  fromFin (fS (fS f)) = absurd f

  bijective True  = refl
  bijective False = refl

  bijective_inv fZ          = refl
  bijective_inv (fS fZ)     = refl
  bijective_inv (fS (fS f)) = absurd f

data T1 : (t : Type) -> Type where
  T1_A : t -> T1 t
  T1_B : t -> t -> T1 t

instance Cardinality t n => Cardinality (T1 t) (n + n * n) where