Data.CT.DependentPara.Instances

Definitions

Para : Type -> Type -> Type

Visibility: public export

(-\-->) : Type -> Type -> Type

  Infix notation for non-dependent parametric functions
  We interpret the extra "-" as a mental symbol for "flat",
  i.e. "non-dependent"

Visibility: public export
Fixity Declaration: infixr operator, level 1

DPara : Type -> Type -> Type

  Parametric functions
  "Usual" dependent para on sets and functions

Visibility: public export

(-\->) : Type -> Type -> Type

  Infix notation for dependent parametric functions
  We interpret the crossed line as a parameter coming in from the top

Visibility: public export
Fixity Declaration: infixr operator, level 1

trivialParam : (a -> b) -> a -\-> b

Visibility: public export

id : a -\-> a

Visibility: public export

composePara : a -\-> b -> b -\-> c -> a -\-> c

Visibility: public export

(\>>) : a -\-> b -> b -\-> c -> a -\-> c

Visibility: public export
Fixity Declaration: infixr operator, level 10

reparam : (pf : a -\-> b) -> {q : a -> Type} -> ((x : a) -> q x -> pf .Param x) -> a -\-> b

Visibility: public export

Param : DPara a b -> a -> Type

Visibility: public export

Run : (pf : DPara a b) -> (x : a) -> Param pf x -> b

Visibility: public export

data IsNotDependent : DPara a b -> Type

Totality: total
Visibility: public export
Constructor: 

MkNonDep : (p : Type) -> (f : (DPair a (const p) -> b)) -> IsNotDependent (MkPara (\{_:12462} => p) f)

GetNonDep : (pf : DPara a b) -> IsNotDependent pf => (p : Type ** DPair a (const p) -> b)

Visibility: public export

GetParam : (pf : DPara a b) -> IsNotDependent pf => Type

  Get the parameter of a non-dependent parametric function

Visibility: public export

composeNTimes : Nat -> a -\-> a -> a -\-> a

Visibility: public export

binaryOpToPara : ((a, p) -> b) -> a -\-> b

Visibility: public export

DParaDLens : Cont -> Cont -> Type

  DParametric dependent lenses
  Not really used in this repo

Visibility: public export

ParaDLens : Cont -> Cont -> Type

Visibility: public export

ParaAddDLens : AddCont -> AddCont -> Type

Visibility: public export

(=\\==>) : AddCont -> AddCont -> Type

Visibility: public export
Fixity Declaration: infixr operator, level 1

trivialParam : a =%> b -> a =\\==> b

Visibility: public export

id : a =\\==> a

Visibility: public export

GetParam : ParaAddDLens a b -> AddCont

Visibility: public export

toHomRepresentation : (f : ParaAddDLens a b) -> GetParam f =%> InternalLensAdditive a b

Visibility: public export

composePara : a =\\==> b -> b =\\==> c -> a =\\==> c

Visibility: public export

DParaAddDLens : AddCont -> AddCont -> Type

  Used in this repo, as all neural networks are additive dependent lenses

Visibility: public export

(=\\=>) : AddCont -> AddCont -> Type

  Infix notation for additive parametric dependent lenses

Visibility: public export
Fixity Declaration: infixr operator, level 1

trivialParam : a =%> b -> a =\\=> b

Visibility: public export

id : a =\\=> a

Visibility: public export

composePara : a =\\=> b -> b =\\=> c -> a =\\=> c

Visibility: public export

(&>>) : a =\\=> b -> b =\\=> c -> a =\\=> c

Visibility: public export
Fixity Declarations:
infixl operator, level 5
infixl operator, level 5
infixr operator, level 10

data IsNotDependent : DParaAddDLens a b -> Type

  A predicate witnessing that a parametric additive dependent lens has
  a non-dependent (constant) parameter.

Totality: total
Visibility: public export
Constructor: 

MkNonDep : (p : AddCont) -> (f : DepHancockProduct a (const p) =%> b) -> IsNotDependent (MkPara (\{_:13414} => p) f)

GetNonDep : (pf : DParaAddDLens a b) -> IsNotDependent pf => (pc : AddCont ** DepHancockProduct a (const pc) =%> b)

Visibility: public export

GetParam : (pf : DParaAddDLens a b) -> IsNotDependent pf => AddCont

Visibility: public export

toHomRepresentation : (pf : DParaAddDLens a b) -> {auto {conArg:13498} : IsNotDependent pf} -> GetParam pf =%> InternalLensAdditive a b

Visibility: public export

composeNTimes : Nat -> a =\\=> a -> a =\\=> a

Visibility: public export

fromNonDepProduct : (a >< p) =%> b -> DepHancockProduct a (const p) =%> b

  Convert a morphism from product container to one from DepHancockProduct
  This witnesses the isomorphism (a >< p) ≅ DepHancockProduct a (const p)

Visibility: public export

binaryOpToPara : (a >< p) =%> b -> a =\\==> b

Visibility: public export