Data.Description.Indexed

The content of this module is based on the paper
A Completely Unique Account of Enumeration
by Cas van der Rest, and Wouter Swierstra
https://doi.org/10.1145/3547636

Definitions

data IDesc : (Type -> Type) -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Zero : IDesc p i

One : IDesc p i

Id : i -> IDesc p i

(*) : IDesc p i -> IDesc p i -> IDesc p i

(+) : IDesc p i -> IDesc p i -> IDesc p i

Sig : (s : Type) -> p s -> (s -> IDesc p i) -> IDesc p i

Elem : IDesc p i -> (i -> Type) -> Type

Totality: total
Visibility: public export

data Fix : (i -> IDesc p i) -> i -> Type

Totality: not strictly positive
Visibility: public export
Constructor: 

MkFix : Elem (d i) (Fix d) -> Fix d i

map : (d : IDesc p i) -> ((v : i) -> x v -> y v) -> Elem d x -> Elem d y

Totality: total
Visibility: export

ifold : ((v : i) -> Elem (d v) x -> x v) -> Fix d v -> x v

Visibility: export