In [3]:
import $ivy.`io.github.siddhartha-gadgil::provingground-core-jvm:0.1.0`
Out[3]:
import $ivy.$
In [4]:
import provingground._, scalahott._, HoTT._
import NatRing._
import NatVecTyps._
Out[4]:
import provingground._, scalahott._, HoTT._

import NatRing._

import NatVecTyps._
In [5]:
Vec
Out[5]:
res4: Func[RepTerm[spire.math.SafeLong], Typ[RepTerm[Vector[spire.math.SafeLong]]]] = ExtendedFunction(
  provingground.scalahott.VecTyps$$Lambda$2272/582082758@6c76fc47,
  SimpleRep(Nat.Typ),
  IdRep(ScalaTypUniv())
)
In [6]:
Vec(1)
Out[6]:
res5: Typ[RepTerm[Vector[spire.math.SafeLong]]] = IndexedVecTyp(
  Nat.Typ,
  SafeLongLong(1L)
)
In [7]:
NilVec
Out[7]:
res6: RepTerm[Vector[spire.math.SafeLong]] = RepSymbObj(
  ScalaSymbol(Vector()),
  IndexedVecTyp(Nat.Typ, SafeLongLong(0L))
)
In [8]:
cons
cons(0)
cons(0).typ
consFn(0)
Out[8]:
res7_0: FuncLike[Nat, Func[Nat, Func[RepTerm[Vector[spire.math.SafeLong]], RepTerm[Vector[spire.math.SafeLong]]]]] = ExtendedDepFunction(
  provingground.scalahott.VecTyps$$Lambda$2277/394286158@688ada97,
  ScalaRepWrap(SimpleRep(Nat.Typ)),
  DepFuncPolyRep(
    ScalaRepWrap(SimpleRep(Nat.Typ)),
    DepFuncPolyRep(VecPolyRep(), VecPolyRep())
  ),
  LambdaFixed(
    RepSymbObj(n, Nat.Typ),
    FuncTyp(
      Nat.Typ,
      FuncTyp(
        SymbScalaTyp(
          ApplnSym(
            ExtendedFunction(
              provingground.scalahott.VecTyps$$Lambda$2272/582082758@6c76fc47,
              SimpleRep(Nat.Typ),
              IdRep(ScalaTypUniv())
            ),
            RepSymbObj(n, Nat.Typ)
          )
        ),
        SymbScalaTyp(
          ApplnSym(
            ExtendedFunction(
              provingground.scalahott.VecTyps$$Lambda$2272/582082758@6c76fc47,
              SimpleRep(Nat.Typ),
              IdRep(ScalaTypUniv())
            ),
            RepSymbObj(
              ApplnSym(AddLiteral(SafeLongLong(1L)), RepSymbObj(n, Nat.Typ)),
              Nat.Typ
            )
          )
        )
      )
    )
  )
)
res7_1: Func[Nat, Func[RepTerm[Vector[spire.math.SafeLong]], RepTerm[Vector[spire.math.SafeLong]]]] = ExtendedFunction(
  provingground.scalahott.VecTyps$$Lambda$2390/41662712@61808682,
  ScalaRepWrap(SimpleRep(Nat.Typ)),
  DepFuncPolyRep(VecPolyRep(), VecPolyRep()),
  FuncTyp(
    Nat.Typ,
    FuncTyp(
      IndexedVecTyp(Nat.Typ, SafeLongLong(0L)),
      IndexedVecTyp(Nat.Typ, SafeLongLong(1L))
    )
  )
)
res7_2: Typ[Func[Nat, Func[RepTerm[Vector[spire.math.SafeLong]], RepTerm[Vector[spire.math.SafeLong]]]]] = FuncTyp(
  Nat.Typ,
  FuncTyp(
    IndexedVecTyp(Nat.Typ, SafeLongLong(0L)),
    IndexedVecTyp(Nat.Typ, SafeLongLong(1L))
  )
)
res7_3: spire.math.SafeLong => Vector[spire.math.SafeLong] => Vector[spire.math.SafeLong] = provingground.scalahott.VecTyps$$Lambda$2390/41662712@61808682
In [9]:
cons(0)(2)(NilVec)
Out[9]:
res8: RepTerm[Vector[spire.math.SafeLong]] = RepSymbObj(
  ScalaSymbol(Vector(SafeLongLong(2L))),
  IndexedVecTyp(Nat.Typ, SafeLongLong(1L))
)
In [10]:
cons(1)(3)(cons(0)(2)(NilVec)) !: Vec(2)
Out[10]:
res9: RepTerm[Vector[spire.math.SafeLong]] = RepSymbObj(
  ScalaSymbol(Vector(SafeLongLong(3L), SafeLongLong(2L))),
  IndexedVecTyp(Nat.Typ, SafeLongLong(2L))
)
In [11]:
n
Out[11]:
res10: RepTerm[spire.math.SafeLong] = RepSymbObj(Name("n"), Nat.Typ)
In [12]:
val k ="k" :: NatTyp
Out[12]:
k: RepTerm[spire.math.SafeLong] = RepSymbObj(Name("k"), Nat.Typ)
In [13]:
import HoTT._
val g = lambda(n)(cons(n)(succ(n)))
Out[13]:
import HoTT._

g: FuncLike[RepTerm[spire.math.SafeLong], Func[RepTerm[Vector[spire.math.SafeLong]], RepTerm[Vector[spire.math.SafeLong]]]] = LambdaTerm(
  RepSymbObj(n, Nat.Typ),
  SymbolicFunc(
    ApplnSym(
      SymbolicFunc(
        ApplnSym(
          ExtendedDepFunction(
            provingground.scalahott.VecTyps$$Lambda$2277/394286158@688ada97,
            ScalaRepWrap(SimpleRep(Nat.Typ)),
            DepFuncPolyRep(
              ScalaRepWrap(SimpleRep(Nat.Typ)),
              DepFuncPolyRep(VecPolyRep(), VecPolyRep())
            ),
            LambdaFixed(
              RepSymbObj(n, Nat.Typ),
              FuncTyp(
                Nat.Typ,
                FuncTyp(
                  SymbScalaTyp(
                    ApplnSym(
                      ExtendedFunction(
                        provingground.scalahott.VecTyps$$Lambda$2272/582082758@6c76fc47,
                        SimpleRep(Nat.Typ),
                        IdRep(ScalaTypUniv())
                      ),
                      RepSymbObj(n, Nat.Typ)
                    )
                  ),
                  SymbScalaTyp(
                    ApplnSym(
                      ExtendedFunction(
                        provingground.scalahott.VecTyps$$Lambda$2272/582082758@6c76fc47,
                        SimpleRep(Nat.Typ),
                        IdRep(ScalaTypUniv())
                      ),
                      RepSymbObj(
...
In [14]:
g(1).typ
Out[14]:
res13: Typ[Func[RepTerm[Vector[spire.math.SafeLong]], RepTerm[Vector[spire.math.SafeLong]]]] = FuncTyp(
  IndexedVecTyp(Nat.Typ, SafeLongLong(1L)),
  IndexedVecTyp(Nat.Typ, SafeLongLong(2L))
)
In [15]:
succ
Out[15]:
res14: Func[LocalTerm, LocalTerm] = LambdaFixed(
  RepSymbObj(x, Nat.Typ),
  RepSymbObj(
    ApplnSym(AddLiteral(SafeLongLong(1L)), RepSymbObj(x, Nat.Typ)),
    Nat.Typ
  )
)
In [16]:
val typFamily = lmbda(n)(Vec(succ(n)))
Out[16]:
typFamily: Func[RepTerm[spire.math.SafeLong], Typ[RepTerm[Vector[spire.math.SafeLong]]]] = LambdaFixed(
  RepSymbObj(n, Nat.Typ),
  SymbScalaTyp(
    ApplnSym(
      ExtendedFunction(
        provingground.scalahott.VecTyps$$Lambda$2272/582082758@6c76fc47,
        SimpleRep(Nat.Typ),
        IdRep(ScalaTypUniv())
      ),
      RepSymbObj(
        ApplnSym(AddLiteral(SafeLongLong(1L)), RepSymbObj(n, Nat.Typ)),
        Nat.Typ
      )
    )
  )
)
In [17]:
val init = NilVec
Out[17]:
init: RepTerm[Vector[spire.math.SafeLong]] = RepSymbObj(
  ScalaSymbol(Vector()),
  IndexedVecTyp(Nat.Typ, SafeLongLong(0L))
)
In [18]:
val countdown = Induc(typFamily, init, g)
Out[18]:
countdown: Induc[RepTerm[Vector[spire.math.SafeLong]]] = Induc(
  LambdaFixed(
    RepSymbObj(n, Nat.Typ),
    SymbScalaTyp(
      ApplnSym(
        ExtendedFunction(
          provingground.scalahott.VecTyps$$Lambda$2272/582082758@6c76fc47,
          SimpleRep(Nat.Typ),
          IdRep(ScalaTypUniv())
        ),
        RepSymbObj(
          ApplnSym(AddLiteral(SafeLongLong(1L)), RepSymbObj(n, Nat.Typ)),
          Nat.Typ
        )
      )
    )
  ),
  RepSymbObj(ScalaSymbol(Vector()), IndexedVecTyp(Nat.Typ, SafeLongLong(0L))),
  LambdaTerm(
    RepSymbObj(n, Nat.Typ),
    SymbolicFunc(
      ApplnSym(
        SymbolicFunc(
          ApplnSym(
            ExtendedDepFunction(
              provingground.scalahott.VecTyps$$Lambda$2277/394286158@688ada97,
              ScalaRepWrap(SimpleRep(Nat.Typ)),
              DepFuncPolyRep(
                ScalaRepWrap(SimpleRep(Nat.Typ)),
                DepFuncPolyRep(VecPolyRep(), VecPolyRep())
              ),
              LambdaFixed(
                RepSymbObj(n, Nat.Typ),
                FuncTyp(
                  Nat.Typ,
                  FuncTyp(
                    SymbScalaTyp(
                      ApplnSym(
                        ExtendedFunction(
...
In [19]:
countdown(0)
Out[19]:
res18: RepTerm[Vector[spire.math.SafeLong]] = RepSymbObj(
  ScalaSymbol(Vector()),
  IndexedVecTyp(Nat.Typ, SafeLongLong(0L))
)
In [20]:
countdown(1)
Out[20]:
res19: RepTerm[Vector[spire.math.SafeLong]] = RepSymbObj(
  ScalaSymbol(Vector(SafeLongLong(1L))),
  IndexedVecTyp(Nat.Typ, SafeLongLong(1L))
)
In [21]:
g(1).typ
g(2).typ
Out[21]:
res20_0: Typ[Func[RepTerm[Vector[spire.math.SafeLong]], RepTerm[Vector[spire.math.SafeLong]]]] = FuncTyp(
  IndexedVecTyp(Nat.Typ, SafeLongLong(1L)),
  IndexedVecTyp(Nat.Typ, SafeLongLong(2L))
)
res20_1: Typ[Func[RepTerm[Vector[spire.math.SafeLong]], RepTerm[Vector[spire.math.SafeLong]]]] = FuncTyp(
  IndexedVecTyp(Nat.Typ, SafeLongLong(2L)),
  IndexedVecTyp(Nat.Typ, SafeLongLong(3L))
)
In [22]:
countdown(2)
Out[22]:
res21: RepTerm[Vector[spire.math.SafeLong]] = RepSymbObj(
  ScalaSymbol(Vector(SafeLongLong(2L), SafeLongLong(1L))),
  IndexedVecTyp(Nat.Typ, SafeLongLong(2L))
)
In [23]:
countdown(10)
Out[23]:
res22: RepTerm[Vector[spire.math.SafeLong]] = RepSymbObj(
  ScalaSymbol(
    Vector(
      SafeLongLong(10L),
      SafeLongLong(9L),
      SafeLongLong(8L),
      SafeLongLong(7L),
      SafeLongLong(6L),
      SafeLongLong(5L),
      SafeLongLong(4L),
      SafeLongLong(3L),
      SafeLongLong(2L),
      SafeLongLong(1L)
    )
  ),
  IndexedVecTyp(Nat.Typ, SafeLongLong(10L))
)