Relation.Indexed

(:*) : (a : i -> Type) -> (b : i -> Type) -> i -> Type

Fixity

Left associative, precedence 3

(:+) : (a : i -> Type) -> (b : i -> Type) -> i -> Type

Fixity

Left associative, precedence 2

(:->) : (a : i -> Type) -> (b : i -> Type) -> i -> Type

Fixity

Left associative, precedence 1

(:.) : (t : Type -> Type) -> (a : i -> Type) -> i -> Type

Fixity

Left associative, precedence 4

All : (a : i -> Type) -> Type

Cst : Type -> i -> Type