In [18]:
import $ivy.`in.ac.iisc::provingground-core:0.1.0`
Out[18]:
import $ivy.$
In [ ]:
In [19]:
import provingground._, functionfinder._
Out[19]:
import provingground._, functionfinder._
In [20]:
import spire.math._
Out[20]:
import spire.math._
In [21]:
1 : SafeLong
Out[21]:
res20: SafeLong = 1
In [22]:
import NatRing._
Out[22]:
import NatRing._
In [23]:
1 : Nat
Out[23]:
res22: Nat = ScalaSymbol(1) : (Nat.Typ)
In [24]:
import HoTT._
val A = "A" :: Type
val B = "B" :: Type
Out[24]:
import HoTT._

A: Typ[Term] with Subs[Typ[Term]] = A : 𝒰 _0
B: Typ[Term] with Subs[Typ[Term]] = B : 𝒰 _0
In [25]:
val a ="a" :: A
val f ="f" :: A ->: B
val mp = lambda(A)(lambda(B)(lmbda(a)(lmbda(f)(f(a)))))
Out[25]:
a: Term with Subs[Term] = a : (A : 𝒰 _0)
f: Func[Term, Term] with Subs[Func[Term, Term]] = f : ((A : 𝒰 _0) → (B : 𝒰 _0))
mp: FuncLike[Typ[Term] with Subs[Typ[Term]], FuncLike[Typ[Term] with Subs[Typ[Term]], Func[Term with Subs[Term], Func[Func[Term, Term] with Subs[Func[Term, Term]], Term]]]] = (A : 𝒰 _0) ↦ ((B : 𝒰 _0) ↦ ((a : (A : 𝒰 _0)) ↦ ((f : ((A : 𝒰 _0) → (B : 𝒰 _0))) ↦ ((f : ((A : 𝒰 _0) → (B : 𝒰 _0))) (a : (A : 𝒰 _0)) : (B : 𝒰 _0)))))
In [26]:
val mpPf = mp(B)(A)
Out[26]:
mpPf: Func[Term with Subs[Term], Func[Func[Term, Term] with Subs[Func[Term, Term]], Term]] = (a : (B : 𝒰 _0)) ↦ ((f : ((B : 𝒰 _0) → (A : 𝒰 _0))) ↦ ((f : ((B : 𝒰 _0) → (A : 𝒰 _0))) (a : (B : 𝒰 _0)) : (A : 𝒰 _0)))
In [27]:
mpPf.typ
Out[27]:
res26: Typ[Func[Term with Subs[Term], Func[Func[Term, Term] with Subs[Func[Term, Term]], Term]]] = (B : 𝒰 _0) → (((B : 𝒰 _0) → (A : 𝒰 _0)) → (A : 𝒰 _0))
In [ ]: