Packages

object IdentityTyp extends Serializable

Linear Supertypes
Serializable, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. IdentityTyp
  2. Serializable
  3. AnyRef
  4. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Type Members

  1. case class InducFn[U <: Term with Subs[U], V <: Term with Subs[V]](domain: Typ[U], targetFmly: FuncLike[U, FuncLike[U, FuncLike[Equality[U], Typ[V]]]], data: FuncLike[U, V], start: U, end: U) extends IndInducFuncLike[Equality[U], V, Func[U, Func[U, Typ[Term]]], FuncLike[U, FuncLike[U, FuncLike[Equality[U], Typ[V]]]]] with Product with Serializable

    inductive definition for identity type family.

  2. case class RecFn[U <: Term with Subs[U], V <: Term with Subs[V]](domain: Typ[U], target: Typ[V], data: Func[U, V], start: U, end: U) extends IndRecFunc[Term, V, Func[U, Func[U, Typ[Term]]]] with Product with Serializable

    recursive definition on identity type families

Value Members

  1. lazy val A: Typ[Term]
  2. lazy val B: Typ[Term]
  3. def apf[U <: Term with Subs[U], V <: Term with Subs[V]](f: Func[U, V]): FuncLike[U, FuncLike[U, Func[Equality[U], Equality[V]]]]
  4. lazy val apfTerm: FuncLike[Typ[Term], FuncLike[Typ[Term], FuncLike[Func[Term, Term], FuncLike[Term, FuncLike[Term, Func[Equality[Term], Equality[Term]]]]]]]
  5. lazy val f: Func[Term, Term]
  6. def get[U <: Term with Subs[U]](lhs: U, rhs: U): IdentityTyp[U]
  7. lazy val idFunc: FuncLike[Typ[Term], Func[Term, Func[Term, IdentityTyp[Term]]]]
  8. def induc[U <: Term with Subs[U], V <: Term with Subs[V]](domain: Typ[U], targetFmly: FuncLike[U, FuncLike[U, FuncLike[Equality[U], Typ[V]]]]): Func[FuncLike[U, V], FuncLike[U, FuncLike[U, Func[Equality[U], V]]]]

    inductive definition for identity type family.

  9. def induced[U <: Term with Subs[U], V <: Term with Subs[V]](f: Func[U, V]): FuncLike[U, FuncLike[U, Func[Equality[U], Equality[V]]]]

    equality induced by a (pure) function term with type x =y -> f(x) = f(y) as function of x and y

  10. def inducedWit[U <: Term with Subs[U], V <: Term with Subs[V]](f: Func[U, V]): FuncLike[U, FuncLike[U, Func[Equality[U], Equality[V]]]]
  11. def preTrans[U <: Term with Subs[U]](dom: Typ[U]): FuncLike[U, FuncLike[U, FuncLike[U, Func[Equality[U], Func[Equality[U], Equality[U]]]]]]
  12. def rec[U <: Term with Subs[U], V <: Term with Subs[V]](dom: Typ[U], target: Typ[V]): Func[Func[U, V], FuncLike[U, FuncLike[U, Func[Equality[U], V]]]]

    recursive definition for identity type family

  13. lazy val reflTerm: FuncLike[Typ[Term], FuncLike[Term, Refl[Term]]]
  14. def symm[U <: Term with Subs[U]](dom: Typ[U]): FuncLike[U, FuncLike[U, Func[Equality[U], Equality[U]]]]

    symmetry term of type x = y -> y = x as a function of x and y

  15. lazy val symmTerm: FuncLike[Typ[Term], FuncLike[Term, FuncLike[Term, Func[Equality[Term], Equality[Term]]]]]
  16. def symmWit[U <: Term with Subs[U]](dom: Typ[U]): FuncLike[U, FuncLike[U, Func[Equality[U], Equality[U]]]]
  17. def trans[U <: Term with Subs[U]](dom: Typ[U]): FuncLike[U, FuncLike[U, FuncLike[U, Func[Equality[U], Func[Equality[U], Equality[U]]]]]]

    transitivity term of type x = y -> y = z -> x = z as a function of x, y and z

  18. lazy val transTerm: FuncLike[Typ[Term], FuncLike[Term, FuncLike[Term, FuncLike[Term, Func[Equality[Term], Func[Equality[Term], Equality[Term]]]]]]]
  19. def transWit[U <: Term with Subs[U]](dom: Typ[U]): FuncLike[U, FuncLike[U, FuncLike[U, Func[Equality[U], Func[Equality[U], Equality[U]]]]]]
  20. def transport[U <: Term with Subs[U], V <: Term with Subs[V]](f: Func[U, Typ[V]]): FuncLike[U, FuncLike[U, Func[Equality[U], Func[V, V]]]]

    transport: term with type x = y -> f(x) -> f(y) as function of x and y

  21. def transportWit[U <: Term with Subs[U], V <: Term with Subs[V]](f: Func[U, Typ[V]]): FuncLike[U, FuncLike[U, Func[Equality[U], Func[V, V]]]]
  22. lazy val x: Term
  23. lazy val y: Term