Dabbling with Agda

I am dabbling with Agda since I want to do something. Can you figure out what?

module Kripke where

open import Data.List.Base as List using (List; []; _∷_)

open import Data.List.NonEmpty as List⁺ using (List⁺; [_]; _∷_)

open import Agda.Builtin.Unit using (⊤; tt)

{- I want to study finite semantics for temporal logic formula over automata -}

{- Kripke structures, maybe switch to labeled transition systems -}

record Kripke (S : Set) (AP : Set) : Set where

  field

    initial : List⁺ S

    transition : (s : S) → List⁺ S

    interpretation : (s : S) → List AP

{- a tree could suffice to describe the semantics for an automaton

   but fails to capture the unravelling of an automaton in the type

   itself -}

data Tree (A : Set) : Set where

  leaf : List A -> Tree A

  branch : A -> List (Tree A) → Tree A

{- instead, the 'clever' idea is to use the following structure, any leaf node

   can be unravelled further into a tree with a generating function -}

data GenTree (A : Set) : Set where

  branch : A -> List (GenTree A) → GenTree A

  generator : ((tt : ⊤) -> GenTree A) -> GenTree A

{- so maybe first try it for lists -}

data GenList (A : Set) : Set where

  cons : A -> GenList A -> GenList A

  generator : ((tt : ⊤) -> GenList A) -> GenList A