Type Members

1.  trait ConstTerm[T] extends Term

   constant term.

2.  case class DepFuncRep[U <: Term with Subs[U], V, X <: Term with Subs[X], Y](domrep: ScalaRep[U, V], codomreps: (V) => ScalaRep[X, Y], fibers: TypFamily[U, X]) extends ScalaRep[FuncLike[U, X], (V) => Y] with Product with Serializable

   Formal extendsion of a dependent function given scalareps for the domain and codomains.

3.  case class ExtendedDepFunction[U <: Term with Subs[U], V, X <: Term with Subs[X], Y](dfn: (V) => Y, domrep: ScalaRep[U, V], codomreps: (V) => ScalaRep[X, Y], fibers: TypFamily[U, X]) extends FuncLike[U, X] with Product with Serializable

   formal extension of a dependent function.

4.  case class ExtendedFunction[U <: Term with Subs[U], V, X <: Term with Subs[X], Y](dfn: (V) => Y, domrep: ScalaRep[U, V], codomrep: ScalaRep[X, Y]) extends Func[U, X] with Product with Serializable

   Formal extension of a function given by a definition and representations for domain and codomain.

5.  implicit class FmlyReps[U <: Term with Subs[U], X <: Term with Subs[X]] extends AnyRef

   implicit class associated to a type family to create dependent functions scalareps.

6.  case class FuncRep[U <: Term with Subs[U], V, X <: Term with Subs[X], Y](domrep: ScalaRep[U, V], codomrep: ScalaRep[X, Y]) extends ScalaRep[Func[U, X], (V) => Y] with Product with Serializable

   Representations for functions given ones for the domain and codomain.

7.  case class IdRep[U <: Term with Subs[U]](typ: Typ[U]) extends ScalaRep[U, U] with Product with Serializable

   A term representing itself.

8.  case class IdTypRep[U <: Term with Subs[U]]()(implicit univ: Typ[Typ[U]]) extends ScalaRep[Typ[U], Typ[U]] with Product with Serializable
9.  implicit class RepSection[V, X <: Term with Subs[X], Y] extends AnyRef

   implicit class associated to a family of scalareps to create dependent functions scalareps.

   implicit class associated to a family of scalareps to create dependent functions scalareps. Not much use since U ends up having strange bounds such as Term with Long.

10.  case class RepSymbObj[A, +U <: RepTerm[A] with Subs[U]](name: AnySym, typ: Typ[U]) extends RepTerm[A] with Symbolic with Product with Serializable
11.  class ScalaSym[U <: Term with Subs[U], V] extends AnyRef
12.  case class ScalaSymbol[X](value: X) extends AtomicSym with Product with Serializable
13.  implicit class ScalaTerm[U <: Term with Subs[U], W] extends AnyRef
14.  case class SigmaRep[U <: Term with Subs[U], V, X <: Term with Subs[X], Y](domrep: ScalaRep[U, V], codrepfmly: (V) => ScalaRep[X, Y]) extends ScalaRep[Term, (V, Y)] with Product with Serializable
15.  case class SimpleConst[V](value: V, typ: Typ[Term]) extends ConstTerm[V] with Product with Serializable

    scala object wrapped to give a HoTT constant with type declared.

16.  case class SimpleExtendedFunction[U <: Term with Subs[U], V, X <: Term with Subs[X]](dfn: (V) => X, domrep: ScalaRep[U, V], codom: Typ[X]) extends Func[U, X] with Subs[SimpleExtendedFunction[U, V, X]] with Product with Serializable

    Extended function with codomain a type.

    Extended function with codomain a type. Perhaps use IdRep.

17.  case class SimpleRep[U <: Term with Subs[U], V](typ: Typ[U]) extends ScalaRep[U, V] with Product with Serializable
18.  case class SmpleFuncRep[U <: Term with Subs[U], V, X <: Term with Subs[X]](domrep: ScalaRep[U, V], codom: Typ[X]) extends ScalaRep[FuncLike[U, X], (V) => X] with Product with Serializable

    Function rep with codomain representing itself.

    Function rep with codomain representing itself. Should perhaps use IdRep instead.

19.  implicit class TermScala[U <: Term with Subs[U]] extends AnyRef