FinPow.agda

module FinPow where

open import Data.Bool
open import Data.Nat renaming (ℕ to Nat)
open import Data.Fin renaming (zero to fzero ; suc to fsuc)
open import Data.Product renaming (Σ to Sg ; proj₁ to proj1 ; proj₂ to proj2)
open import Relation.Binary.PropositionalEquality renaming (_≡_ to _==_)

record Iso (X Y : Set) : Set where
  field
    fwd : X -> Y
    bwd : Y -> X
    fwdbwd==id : forall x -> bwd (fwd x) == x
    bwdfwd==id : forall y -> fwd (bwd y) == y

open Iso public

Card : Set -> Nat -> Set
Card X n = Iso X (Fin n)

IsFinite : Set -> Set
IsFinite X = Sg _ (Card X)

Pow : Set -> Set
Pow X = X -> Bool

BoolIsFinite : IsFinite Bool
BoolIsFinite = 2 , record { fwd = fwdb ; bwd = bwdb ; fwdbwd==id = fwdbwd==idb ; bwdfwd==id = bwdfwd==idb }
  where
    fwdb : Bool -> Fin 2
    fwdb false = fzero
    fwdb true = fsuc fzero

    bwdb : Fin 2 -> Bool
    bwdb fzero = false
    bwdb (fsuc fzero) = true

    fwdbwd==idb : forall b -> bwdb (fwdb b) == b
    fwdbwd==idb false = refl
    fwdbwd==idb true = refl

    bwdfwd==idb : forall f -> fwdb (bwdb f) == f
    bwdfwd==idb fzero = refl
    bwdfwd==idb (fsuc fzero) = refl

finpow : forall X -> IsFinite X -> IsFinite (Pow X)
finpow X (m , p) = (2 ^ m) , (the-crucial-lemma X Bool m 2 p (proj2 BoolIsFinite))
  where
    the-crucial-lemma : forall X Y m n -> Card X m -> Card Y n -> Card (X -> Y) (n ^ m)
    the-crucial-lemma X Y m n p q = {!!}