Data.CT.Functor.Instances

Definitions

id : Functor c c

Visibility: public export

IndCat : Cat -> Type

  Functor Type -> Cat^op

Visibility: public export

Const : IndCat c

Visibility: public export

FamObj : Type -> Cat

Visibility: public export

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

Visibility: public export

FamIndCat : IndCat TypeCat

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

Visibility: public export

Base : Functor DLens TypeCat

  Functor which projects the forward part of a dependent lens

Visibility: public export

FamDLens : IndCat DLens

  DLens -> Type -> Cat^op

Visibility: public export

AddBase : Functor AddDLens TypeCat

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

Visibility: public export

FamAddDLens : IndCat AddDLens

Visibility: public export

IndexedType : Type -> Type

Visibility: public export

TypeDPair : IndexedType a -> Type

Visibility: public export

TypeDFun : IndexedType a -> Type

Visibility: public export

IndexedCont : Cont -> Type

Visibility: public export

ContDPair : IndexedCont a -> Cont

Visibility: public export

ContProbDPair : IndexedCont a -> Cont

Visibility: public export

IndexedAddCont : AddCont -> Type

Visibility: public export

AddContDPair : IndexedAddCont a -> AddCont

Visibility: public export

AddContDFunFinite : (Fin n -> AddCont) -> AddCont

Visibility: public export

indexShp : (j : Fin n) -> (AddContDFunFinite i) .Shp -> (i j) .Shp

Visibility: public export

AddContDFunction : IndexedAddCont a -> AddCont

Visibility: public export

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

Visibility: public export

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

Visibility: public export

constFam : Cont -> IndexedCont c

Visibility: public export

trivialFam : IndexedCont c

Visibility: public export

boolFam : IndexedCont c

Visibility: public export

ContUniverse : Cont

Visibility: public export

famFromChart : (c : Cont) -> c =&> ContUniverse -> IndexedCont c

Visibility: public export