Data.CT.Functor.Instances

Definitions

id : Functor c c

Totality: total
Visibility: public export

IndCat : Cat -> Type

  Functor Type -> Cat^op

Totality: total
Visibility: public export

Const : IndCat c

Totality: total
Visibility: public export

FamObj : Type -> Cat

Totality: total
Visibility: public export

FamMor : (x -> y) -> Functor (FamObj y) (FamObj x)

Totality: total
Visibility: public export

FamIndCat : IndCat TypeCat

  Functor Type -> Cat^op, we will mostly instantiate this for `c=TypeCat`

Totality: total
Visibility: public export

Base : Functor DLens TypeCat

  Functor which projects the forward part of a dependent lens

Totality: total
Visibility: public export

FamDLens : IndCat DLens

  DLens -> Type -> Cat^op

Totality: total
Visibility: public export

AddBase : Functor AddDLens TypeCat

  Functor which projects out the forward part of an additive dependent lens

Totality: total
Visibility: public export

FamAddDLens : IndCat AddDLens

Totality: total
Visibility: public export

IndexedType : Type -> Type

Totality: total
Visibility: public export

TypeDPair : IndexedType a -> Type

Totality: total
Visibility: public export

TypeDFun : IndexedType a -> Type

Totality: total
Visibility: public export

IndexedCont : Cont -> Type

  TODO probably name clash with other "Indexed container"

Totality: total
Visibility: public export

ContDPair : IndexedCont a -> Cont

Totality: total
Visibility: public export

ContProbDPair : IndexedCont a -> Cont

Totality: total
Visibility: public export

ContDPairSimple : (c : Cont) -> IndexedCont c -> Cont

Totality: total
Visibility: public export

ContDFun : (c : Cont) -> IndexedCont c -> Cont

Totality: total
Visibility: public export

constFam : Cont -> IndexedCont c

Totality: total
Visibility: public export

trivialFam : IndexedCont c

Totality: total
Visibility: public export

boolFam : IndexedCont c

Totality: total
Visibility: public export