Packages

case class SigmaTyp[W <: Term with Subs[W], U <: Term with Subs[U]](fibers: TypFamily[W, U]) extends Typ[AbsPair[W, U]] with Subs[SigmaTyp[W, U]] with Product with Serializable

Sigma Type, i.e., dependent pair type.

Self Type
SigmaTyp[W, U]
Linear Supertypes
Serializable, Product, Equals, Typ[AbsPair[W, U]], Term, Subs[SigmaTyp[W, U]], AnyRef, Any
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. SigmaTyp
  2. Serializable
  3. Product
  4. Equals
  5. Typ
  6. Term
  7. Subs
  8. AnyRef
  9. Any
Implicitly
  1. by RichTerm
  2. by any2stringadd
  3. by StringFormat
  4. by Ensuring
  5. by ArrowAssoc
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Instance Constructors

  1. new SigmaTyp(fibers: TypFamily[W, U])

Type Members

  1. case class InducFn[V <: Term with Subs[V]](targetFmly: FuncLike[W, Func[U, Typ[V]]], data: FuncLike[W, FuncLike[U, V]]) extends InducFuncLike[AbsPair[W, U], V] with Product with Serializable

    inductive definition on the Sigma-type

  2. type Obj = AbsPair[W, U]

    scala type of objects with this HoTT-type (refining U)

    scala type of objects with this HoTT-type (refining U)

    Definition Classes
    SigmaTyp → Typ
  3. case class RecFn[V <: Term with Subs[V]](codom: Typ[V], data: FuncLike[W, Func[U, V]]) extends RecFunc[AbsPair[W, U], V] with Product with Serializable

    recursively defined function on this

Value Members

  1. def !:(term: Term): AbsPair[W, U]

    checks term is of this type and returns it; useful for documentation.

    checks term is of this type and returns it; useful for documentation.

    Definition Classes
    Typ
  2. def &&[UU >: AbsPair[W, U] <: Term with Subs[UU], V <: Term with Subs[V]](that: Typ[V]): ProdTyp[UU, V]

    returns product type, mainly to use for "and" for structures

    returns product type, mainly to use for "and" for structures

    Definition Classes
    Typ
  3. def &:[UU >: AbsPair[W, U] <: Term with Subs[UU], V <: Term with Subs[V]](variable: V): SigmaTyp[V, UU]
    Definition Classes
    Typ
  4. def ++[UU >: Typ[AbsPair[W, U]] <: Typ[Term] with Subs[UU], VV <: Term with Subs[VV], V <: Typ[VV] with Subs[V]](those: V): SigmaTyp[UU, VV]

    returns Sigma-Type, mainly to use as "such that", for example a group type is this with product etc.

    returns Sigma-Type, mainly to use as "such that", for example a group type is this with product etc. dependent on this.

    Definition Classes
    Typ
  5. def ->:[W <: Term with Subs[W], UU >: AbsPair[W, U] <: Term with Subs[UU]](that: Typ[W]): FuncTyp[W, UU]

    function type: this -> that

    function type: this -> that

    Definition Classes
    Typ
  6. def :->[V <: Term with Subs[V]](that: V): Func[SigmaTyp[W, U], V]

    constructor for (pure) lambda functions, see lmbda

    constructor for (pure) lambda functions, see lmbda

    Implicit
    This member is added by an implicit conversion from SigmaTyp[W, U] toRichTerm[SigmaTyp[W, U]] performed by method RichTerm in provingground.HoTT.
    Definition Classes
    RichTerm
  7. def ::(name: String): AbsPair[W, U]

    symbolic object with given name

    symbolic object with given name

    Definition Classes
    Typ
  8. def :~>[V <: Term with Subs[V]](that: V): FuncLike[SigmaTyp[W, U], V]

    constructor for (in general dependent) lambda functions, see lambda

    constructor for (in general dependent) lambda functions, see lambda

    Implicit
    This member is added by an implicit conversion from SigmaTyp[W, U] toRichTerm[SigmaTyp[W, U]] performed by method RichTerm in provingground.HoTT.
    Definition Classes
    RichTerm
  9. def =:=(rhs: SigmaTyp[W, U]): IdentityTyp[SigmaTyp[W, U]]

    equality type 'term = rhs'

    equality type 'term = rhs'

    Implicit
    This member is added by an implicit conversion from SigmaTyp[W, U] toRichTerm[SigmaTyp[W, U]] performed by method RichTerm in provingground.HoTT.
    Definition Classes
    RichTerm
  10. def Var(implicit factory: NameFactory): AbsPair[W, U]

    new variable from a factory.

    new variable from a factory.

    Definition Classes
    Typ
  11. def dependsOn(that: Term): Boolean

    returns whether this depends on that

    returns whether this depends on that

    Definition Classes
    Term
  12. lazy val fib: LambdaFixed[W, Typ[U]]
  13. val fibers: TypFamily[W, U]
  14. def indepOf(that: Term): Boolean

    returns whether this is independent of that.

    returns whether this is independent of that.

    Definition Classes
    Term
  15. def induc[V <: Term with Subs[V]](targetFmly: FuncLike[W, Func[U, Typ[V]]]): Func[FuncLike[W, FuncLike[U, V]], FuncLike[AbsPair[W, U], V]]

    inductive definition

    inductive definition

    targetFmly

    the codomain

  16. def newobj: SigmaTyp[W, U]

    A new object with the same type, to be used in place of a variable to avoid name clashes.

    A new object with the same type, to be used in place of a variable to avoid name clashes. Should throw exception when invoked for constants.

    Definition Classes
    SigmaTyp → Subs
  17. def obj: AbsPair[W, U]

    factory for producing objects of the given type.

    factory for producing objects of the given type. can use {{innervar}} if one wants name unchanged.

    Definition Classes
    Typ
  18. lazy val paircons: FuncLike[W, Func[U, AbsPair[W, U]]]

    introduction rule for the Sigma type

  19. def productElementNames: Iterator[String]
    Definition Classes
    Product
  20. lazy val proj1: Func[AbsPair[W, U], W]

    projections from the Sigma-Type

  21. lazy val proj2: FuncLike[AbsPair[W, U], U]

    projections from the Sigma-Type

  22. def rec[V <: Term with Subs[V]](target: Typ[V]): Func[FuncLike[W, Func[U, V]], FuncLike[AbsPair[W, U], V]]

    recursive definition

    recursive definition

    target

    the codomain

  23. def refl: Refl[SigmaTyp[W, U]]

    reflexivity term refl : term = term

    reflexivity term refl : term = term

    Implicit
    This member is added by an implicit conversion from SigmaTyp[W, U] toRichTerm[SigmaTyp[W, U]] performed by method RichTerm in provingground.HoTT.
    Definition Classes
    RichTerm
  24. def replace(x: Term, y: Term): SigmaTyp[W, U] with Subs[SigmaTyp[W, U]]

    refine substitution so if x and y are both of certain forms such as pairs or formal applications, components are substituted.

    refine substitution so if x and y are both of certain forms such as pairs or formal applications, components are substituted.

    Definition Classes
    Subs
  25. def subs(x: Term, y: Term): SigmaTyp[W, U]

    substitute x by y recursively in this.

    substitute x by y recursively in this.

    Definition Classes
    SigmaTyp → Subs
  26. def sym(implicit name: sourcecode.Name): AbsPair[W, U]

    shortcut for symbolic object

    shortcut for symbolic object

    Definition Classes
    Typ
  27. def symbObj(name: AnySym): AbsPair[W, U] with Subs[AbsPair[W, U]]

    A symbolic object with this HoTT type, and with scala-type Obj

    A symbolic object with this HoTT type, and with scala-type Obj

    Definition Classes
    Typ
  28. def toString(): String
    Definition Classes
    SigmaTyp → AnyRef → Any
  29. lazy val typ: Universe

    type of a type is a universe.

    type of a type is a universe.

    Definition Classes
    SigmaTyp → Typ → Term
  30. lazy val typlevel: Int
    Definition Classes
    Typ
  31. def usesVar(t: Term): Boolean

    returns whether the variable t is used as a variable in a lambda definition.

    returns whether the variable t is used as a variable in a lambda definition.

    Definition Classes
    Term
  32. def variable(name: AnySym): AbsPair[W, U]

    A symbolic object with this HoTT type, and with scala-type Obj

    A symbolic object with this HoTT type, and with scala-type Obj

    Definition Classes
    SigmaTyp → Typ
  33. def ||[UU >: AbsPair[W, U] <: Term with Subs[UU], V <: Term with Subs[V]](that: Typ[V]): PlusTyp[UU, V]

    returns coproduct type, mainly to use for "or".

    returns coproduct type, mainly to use for "or".

    Definition Classes
    Typ
  34. def ~>:[UU >: AbsPair[W, U] <: Term with Subs[UU], V <: Term with Subs[V]](variable: V): GenFuncTyp[V, UU]

    dependent function type (Pi-Type) define by a lambda: this depends on the variable, which hence gives a type family; note that a new variable is created and substituted in this to avoid name clashes.

    dependent function type (Pi-Type) define by a lambda: this depends on the variable, which hence gives a type family; note that a new variable is created and substituted in this to avoid name clashes.

    Definition Classes
    Typ
  35. object Elem

    Pattern for element of the given type.

    Pattern for element of the given type.

    Definition Classes
    Typ