Initial.

Finite/Interfaces.idr

+module Finite.Interfaces
+
+import Data.Fin
+import Isomorphism.Isomorphism
+
+
+interface Finite t where
+  card : Nat
+  iso  : Iso t (Fin card)  
+
+implementation Finite (Fin n) where
+  card {n} = n
+  iso  = ?kika
+
+{-
+
+---}

Finite/Operations.idr

+module Finite.Operations
+
+import Data.Fin
+import Data.List
+
+import Finite.Predicates
+import Sigma.Sigma
+import Sigma.Operations
+import Isomorphism.Isomorphism
+
+
+||| Cardinality of finite types
+card : {A : Type} -> (fA : Finite A) -> Nat
+card = outl
+
+
+||| Isomorphism of finite types
+iso : {A : Type} -> (fA : Finite A) -> Iso A (Fin (card fA))
+iso = outr
+
+
+||| Maps a finite type |A| to a list of |A|-values
+toList : {A : Type} -> (fA : Finite A) -> List A
+toList (MkSigma _ iso) = ?kika -- toList (from iso)
+
+

Finite/Predicates.idr

+module Finite.Predicates
+
+import Data.Fin
+import Isomorphism.Isomorphism
+import Sigma.Sigma
+
+
+public export
+Finite : Type -> Type
+Finite t = Sigma Nat (\ n => Iso t (Fin n))

Isomorphism/Isomorphism.idr

+module Isomorphism.Isomorphism
+
+                                                                                                                          
+import Data.Fin                                                                                                           
+                                                                                                                          
+                                                                                                                          
+||| An isomorphism between two types                                                                                      
+public export
+record Iso a b where                                                                                                      
+  constructor MkIso                                                                                                       
+  to : a -> b                                                                                                             
+  from : b -> a                                                                                                           
+  toFrom : (y : b) -> to (from y) = y                                                                                     
+  fromTo : (x : a) -> from (to x) = x

Sigma/Operations.idr

+module Sigma.Operations
+
+import Sigma.Sigma
+
+
+public export
+outl : {A : Type} -> {P : A -> Type} -> Sigma A P -> A
+outl (MkSigma a _) = a
+
+
+public export
+outr : {A : Type} -> {P : A -> Type} -> (s : Sigma A P) -> P (outl s)
+outr (MkSigma _ p) = p

Sigma/Sigma.idr

+module Sigma.Sigma
+
+
+public export
+data Sigma : (A : Type) -> (P : A -> Type) -> Type where
+  MkSigma : {A : Type} -> {P : A -> Type} -> (x : A) -> (pf : P x) -> Sigma A P