Packages

abstract class GenFuncTyp[W <: Term with Subs[W], U <: Term with Subs[U]] extends Typ[FuncLike[W, U]] with Subs[GenFuncTyp[W, U]]

Possibly dependent function type. Meant to override equality so that an object with scala type a Pi-Type but with fiber a constant is equal to the corresponding function type.

Linear Supertypes
Typ[FuncLike[W, U]], Term, Subs[GenFuncTyp[W, U]], AnyRef, Any
Known Subclasses
FuncTyp, PiDefn, PiTyp
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. GenFuncTyp
  2. Typ
  3. Term
  4. Subs
  5. AnyRef
  6. 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 GenFuncTyp(domain: Typ[W], fib: (W) => Typ[U])

    domain

    the domain

    fib

    fiber of the codomain

Type Members

  1. abstract type Obj <: FuncLike[W, U] with Subs[Obj]

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

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

    Definition Classes
    Typ

Abstract Value Members

  1. abstract def newobj: GenFuncTyp[W, U] with Subs[GenFuncTyp[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
    Subs
  2. abstract def subs(x: Term, y: Term): GenFuncTyp[W, U] with Subs[GenFuncTyp[W, U]]

    substitute x by y recursively in this.

    substitute x by y recursively in this.

    Definition Classes
    Subs
  3. abstract val typ: Univ

    type of a type is a universe.

    type of a type is a universe.

    Definition Classes
    Typ → Term
  4. abstract def variable(name: AnySym): Obj with Subs[Obj]

    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

Concrete Value Members

  1. def !:(term: Term): FuncLike[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 >: FuncLike[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 >: FuncLike[W, U] <: Term with Subs[UU], V <: Term with Subs[V]](variable: V): SigmaTyp[V, UU]
    Definition Classes
    Typ
  4. def ++[UU >: Typ[FuncLike[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 >: FuncLike[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[GenFuncTyp[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 GenFuncTyp[W, U] toRichTerm[GenFuncTyp[W, U]] performed by method RichTerm in provingground.HoTT.
    Definition Classes
    RichTerm
  7. def ::(name: String): FuncLike[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[GenFuncTyp[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 GenFuncTyp[W, U] toRichTerm[GenFuncTyp[W, U]] performed by method RichTerm in provingground.HoTT.
    Definition Classes
    RichTerm
  9. def =:=(rhs: GenFuncTyp[W, U]): IdentityTyp[GenFuncTyp[W, U]]

    equality type 'term = rhs'

    equality type 'term = rhs'

    Implicit
    This member is added by an implicit conversion from GenFuncTyp[W, U] toRichTerm[GenFuncTyp[W, U]] performed by method RichTerm in provingground.HoTT.
    Definition Classes
    RichTerm
  10. def Var(implicit factory: NameFactory): FuncLike[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. val domain: Typ[W]
  13. def equals(that: Any): Boolean
    Definition Classes
    GenFuncTyp → AnyRef → Any
  14. val fib: (W) => Typ[U]
  15. lazy val hashCode: Int
    Definition Classes
    GenFuncTyp → AnyRef → Any
  16. def indepOf(that: Term): Boolean

    returns whether this is independent of that.

    returns whether this is independent of that.

    Definition Classes
    Term
  17. def obj: FuncLike[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. def refl: Refl[GenFuncTyp[W, U]]

    reflexivity term refl : term = term

    reflexivity term refl : term = term

    Implicit
    This member is added by an implicit conversion from GenFuncTyp[W, U] toRichTerm[GenFuncTyp[W, U]] performed by method RichTerm in provingground.HoTT.
    Definition Classes
    RichTerm
  19. def replace(x: Term, y: Term): GenFuncTyp[W, U] with Subs[GenFuncTyp[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
  20. def sym(implicit name: sourcecode.Name): FuncLike[W, U]

    shortcut for symbolic object

    shortcut for symbolic object

    Definition Classes
    Typ
  21. def symbObj(name: AnySym): FuncLike[W, U] with Subs[FuncLike[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
  22. lazy val typlevel: Int
    Definition Classes
    Typ
  23. 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
  24. def ||[UU >: FuncLike[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
  25. def ~>:[UU >: FuncLike[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
  26. object Elem

    Pattern for element of the given type.

    Pattern for element of the given type.

    Definition Classes
    Typ