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))
)