Department of Mathematics
Indian Institute of Science
Bangalore
Is there a homogeneous, (conjugacy invariant) length function on the free group on two generators?
A Type for Proofs of $l(word)\leq bound$
sealed abstract class LinNormBound(val word: Word,val bound: Double)
final case class Gen(n: Int) extends LinNormBound(Word(Vector(n)), 1)
final case class ConjGen(n: Int,pf: LinNormBound) extends
LinNormBound(n +: pf.word :+ (-n), pf.bound)
final case class Triang(pf1: LinNormBound, pf2: LinNormBound) extends
LinNormBound( pf1.word ++ pf2.word, pf1.bound + pf2.bound)
final case class PowerBound(base: Word, n: Int, pf: LinNormBound) extends
LinNormBound(base, pf.bound/n){require(pf.word == base.pow(n))}
final case object Empty extends LinNormBound(Word(Vector()), 0)
Let $A$ and $B$ be types, regarded as representing propositions.
package provingground.library
import provingground._
import HoTT._
import induction._
import implicits._
import shapeless._
import Fold._
object nat$decidable_eq {
val value = lambda("'ag_1531296106_1367828936" :: "nat" :: Type)(({
val rxyz = pprodInd.value(piDefn("'aj_117702620" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_751289559" :: Type)(FuncTyp("'c_751289559" :: Type, FuncTyp("'c_751289559" :: Type, Prop))))("nat" :: Type)("'ag_1531296106_1367828936" :: "nat" :: Type)("'aj_117702620" :: "nat" :: Type))))(({
val rxyz = natInd.value.rec(Type)
rxyz
})("punit" :: Type)(lmbda("'h_159188406_990306052" :: "nat" :: Type)(lmbda("'i_854809894_325907817" :: Type)(("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(piDefn("'aj_482846896" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_2112253922" :: Type)(FuncTyp("'c_2112253922" :: Type, FuncTyp("'c_2112253922" :: Type, Prop))))("nat" :: Type)("'h_159188406_990306052" :: "nat" :: Type)("'aj_482846896" :: "nat" :: Type))))("'i_854809894_325907817" :: Type))("punit" :: Type))))("'ag_1531296106_1367828936" :: "nat" :: Type)).rec(piDefn("'aj_228954873" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_1303348173" :: Type)(FuncTyp("'c_1303348173" :: Type, FuncTyp("'c_1303348173" :: Type, Prop))))("nat" :: Type)("'ag_1531296106_1367828936" :: "nat" :: Type)("'aj_228954873" :: "nat" :: Type))))
rxyz
})(lmbda("'s_318103601_490050232" :: piDefn("'aj_15078438_215709177" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_517841910" :: Type)(FuncTyp("'c_517841910" :: Type, FuncTyp("'c_517841910" :: Type, Prop))))("nat" :: Type)("'ag_1531296106_1367828936" :: "nat" :: Type)("'aj_15078438_215709177" :: "nat" :: Type))))(lmbda("_" :: ({
val rxyz = natInd.value.rec(Type)
rxyz
})("punit" :: Type)(lmbda("'h_159188406_753078297" :: "nat" :: Type)(lmbda("'i_854809894_590543722" :: Type)(("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(piDefn("'aj_1051336192" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_704808476" :: Type)(FuncTyp("'c_704808476" :: Type, FuncTyp("'c_704808476" :: Type, Prop))))("nat" :: Type)("'h_159188406_753078297" :: "nat" :: Type)("'aj_1051336192" :: "nat" :: Type))))("'i_854809894_590543722" :: Type))("punit" :: Type))))("'ag_1531296106_1367828936" :: "nat" :: Type))("'s_318103601_490050232" :: piDefn("'aj_15078438_215709177" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_517841910" :: Type)(FuncTyp("'c_517841910" :: Type, FuncTyp("'c_517841910" :: Type, Prop))))("nat" :: Type)("'ag_1531296106_1367828936" :: "nat" :: Type)("'aj_15078438_215709177" :: "nat" :: Type))))))(({
val rxyz = natInd.value.induc(lmbda("'v_1087445862_593085322" :: "nat" :: Type)(("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(piDefn("'aj_202430491" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_374127766" :: Type)(FuncTyp("'c_374127766" :: Type, FuncTyp("'c_374127766" :: Type, Prop))))("nat" :: Type)("'v_1087445862_593085322" :: "nat" :: Type)("'aj_202430491" :: "nat" :: Type))))(({
val rxyz = natInd.value.rec(Type)
rxyz
})("punit" :: Type)(lmbda("'h_159188406_283972159" :: "nat" :: Type)(lmbda("'i_854809894_765942027" :: Type)(("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(piDefn("'aj_362557726" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_187883991" :: Type)(FuncTyp("'c_187883991" :: Type, FuncTyp("'c_187883991" :: Type, Prop))))("nat" :: Type)("'h_159188406_283972159" :: "nat" :: Type)("'aj_362557726" :: "nat" :: Type))))("'i_854809894_765942027" :: Type))("punit" :: Type))))("'v_1087445862_593085322" :: "nat" :: Type))))
rxyz
})(("pprod.mk" :: piDefn("'f_858730760" :: Type)(piDefn("'g_84737018" :: Type)(FuncTyp("'f_858730760" :: Type, FuncTyp("'g_84737018" :: Type, ("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))("'f_858730760" :: Type)("'g_84737018" :: Type))))))(piDefn("'aj_1405500650" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_1679528951" :: Type)(FuncTyp("'c_1679528951" :: Type, FuncTyp("'c_1679528951" :: Type, Prop))))("nat" :: Type)("nat.zero" :: "nat" :: Type)("'aj_1405500650" :: "nat" :: Type))))("punit" :: Type)(lambda("'ak_992690145_66345703" :: "nat" :: Type)(({
val rxyz = natInd.value.induc(lmbda("$vuyd_613901509_1138574320" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_51816028" :: Type)(FuncTyp("'c_51816028" :: Type, FuncTyp("'c_51816028" :: Type, Prop))))("nat" :: Type)("nat.zero" :: "nat" :: Type)("$vuyd_613901509_1138574320" :: "nat" :: Type))))
rxyz
})("_" :: ("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_1616709371" :: Type)(FuncTyp("'c_1616709371" :: Type, FuncTyp("'c_1616709371" :: Type, Prop))))("nat" :: Type)("nat.zero" :: "nat" :: Type)("nat.zero" :: "nat" :: Type)))(lambda("'k_621156251_206574004" :: "nat" :: Type)(lmbda("_" :: ("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_1547408363" :: Type)(FuncTyp("'c_1547408363" :: Type, FuncTyp("'c_1547408363" :: Type, Prop))))("nat" :: Type)("nat.zero" :: "nat" :: Type)("'k_621156251_206574004" :: "nat" :: Type)))("_" :: ("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_2022960021" :: Type)(FuncTyp("'c_2022960021" :: Type, FuncTyp("'c_2022960021" :: Type, Prop))))("nat" :: Type)("nat.zero" :: "nat" :: Type)(("nat.succ" :: FuncTyp("nat" :: Type, "nat" :: Type))("'k_621156251_206574004" :: "nat" :: Type))))))("'ak_992690145_66345703" :: "nat" :: Type)))("punit.star" :: "punit" :: Type))(lambda("'v_256405719_429396927" :: "nat" :: Type)(lmbda("'w_566843556_179354281" :: ("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(piDefn("'aj_257559038" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_265527310" :: Type)(FuncTyp("'c_265527310" :: Type, FuncTyp("'c_265527310" :: Type, Prop))))("nat" :: Type)("'v_256405719_429396927" :: "nat" :: Type)("'aj_257559038" :: "nat" :: Type))))(({
val rxyz = natInd.value.rec(Type)
rxyz
})("punit" :: Type)(lmbda("'h_159188406_696790367" :: "nat" :: Type)(lmbda("'i_854809894_317859634" :: Type)(("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(piDefn("'aj_1612878706" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_479764664" :: Type)(FuncTyp("'c_479764664" :: Type, FuncTyp("'c_479764664" :: Type, Prop))))("nat" :: Type)("'h_159188406_696790367" :: "nat" :: Type)("'aj_1612878706" :: "nat" :: Type))))("'i_854809894_317859634" :: Type))("punit" :: Type))))("'v_256405719_429396927" :: "nat" :: Type)))(("pprod.mk" :: piDefn("'f_1605051863" :: Type)(piDefn("'g_1443604027" :: Type)(FuncTyp("'f_1605051863" :: Type, FuncTyp("'g_1443604027" :: Type, ("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))("'f_1605051863" :: Type)("'g_1443604027" :: Type))))))(piDefn("'aj_320897960" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_1411998825" :: Type)(FuncTyp("'c_1411998825" :: Type, FuncTyp("'c_1411998825" :: Type, Prop))))("nat" :: Type)(("nat.succ" :: FuncTyp("nat" :: Type, "nat" :: Type))("'v_256405719_429396927" :: "nat" :: Type))("'aj_320897960" :: "nat" :: Type))))(("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(piDefn("'aj_138014301" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_2131675862" :: Type)(FuncTyp("'c_2131675862" :: Type, FuncTyp("'c_2131675862" :: Type, Prop))))("nat" :: Type)("'v_256405719_429396927" :: "nat" :: Type)("'aj_138014301" :: "nat" :: Type))))(({
val rxyz = natInd.value.rec(Type)
rxyz
})("punit" :: Type)(lmbda("'h_159188406_1856699345" :: "nat" :: Type)(lmbda("'i_854809894_883946601" :: Type)(("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(piDefn("'aj_1842985757" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_1398049368" :: Type)(FuncTyp("'c_1398049368" :: Type, FuncTyp("'c_1398049368" :: Type, Prop))))("nat" :: Type)("'h_159188406_1856699345" :: "nat" :: Type)("'aj_1842985757" :: "nat" :: Type))))("'i_854809894_883946601" :: Type))("punit" :: Type))))("'v_256405719_429396927" :: "nat" :: Type)))("punit" :: Type))(lambda("'ak_992690145_1869838569" :: "nat" :: Type)(({
val rxyz = natInd.value.induc(lmbda("$vuyd_613901509_1095799675" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_2017105073" :: Type)(FuncTyp("'c_2017105073" :: Type, FuncTyp("'c_2017105073" :: Type, Prop))))("nat" :: Type)(("nat.succ" :: FuncTyp("nat" :: Type, "nat" :: Type))("'v_256405719_429396927" :: "nat" :: Type))("$vuyd_613901509_1095799675" :: "nat" :: Type))))
rxyz
})("_" :: ("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_1559678193" :: Type)(FuncTyp("'c_1559678193" :: Type, FuncTyp("'c_1559678193" :: Type, Prop))))("nat" :: Type)(("nat.succ" :: FuncTyp("nat" :: Type, "nat" :: Type))("'v_256405719_429396927" :: "nat" :: Type))("nat.zero" :: "nat" :: Type)))(lambda("'k_217786156_1059286668" :: "nat" :: Type)(lmbda("_" :: ("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_998126858" :: Type)(FuncTyp("'c_998126858" :: Type, FuncTyp("'c_998126858" :: Type, Prop))))("nat" :: Type)(("nat.succ" :: FuncTyp("nat" :: Type, "nat" :: Type))("'v_256405719_429396927" :: "nat" :: Type))("'k_217786156_1059286668" :: "nat" :: Type)))("_" :: ("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_590214278" :: Type)(FuncTyp("'c_590214278" :: Type, FuncTyp("'c_590214278" :: Type, Prop))))("nat" :: Type)(("nat.succ" :: FuncTyp("nat" :: Type, "nat" :: Type))("'v_256405719_429396927" :: "nat" :: Type))(("nat.succ" :: FuncTyp("nat" :: Type, "nat" :: Type))("'k_217786156_1059286668" :: "nat" :: Type))))))("'ak_992690145_1869838569" :: "nat" :: Type)))(("pprod.mk" :: piDefn("'f_14519285" :: Type)(piDefn("'g_88262494" :: Type)(FuncTyp("'f_14519285" :: Type, FuncTyp("'g_88262494" :: Type, ("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))("'f_14519285" :: Type)("'g_88262494" :: Type))))))(("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(piDefn("'aj_161697836" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_257271152" :: Type)(FuncTyp("'c_257271152" :: Type, FuncTyp("'c_257271152" :: Type, Prop))))("nat" :: Type)("'v_256405719_429396927" :: "nat" :: Type)("'aj_161697836" :: "nat" :: Type))))(({
val rxyz = natInd.value.rec(Type)
rxyz
})("punit" :: Type)(lmbda("'h_159188406_1711678532" :: "nat" :: Type)(lmbda("'i_854809894_1639579534" :: Type)(("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(piDefn("'aj_1427415108" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_888554361" :: Type)(FuncTyp("'c_888554361" :: Type, FuncTyp("'c_888554361" :: Type, Prop))))("nat" :: Type)("'h_159188406_1711678532" :: "nat" :: Type)("'aj_1427415108" :: "nat" :: Type))))("'i_854809894_1639579534" :: Type))("punit" :: Type))))("'v_256405719_429396927" :: "nat" :: Type)))("punit" :: Type)("'w_566843556_179354281" :: ("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(piDefn("'aj_257559038" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_265527310" :: Type)(FuncTyp("'c_265527310" :: Type, FuncTyp("'c_265527310" :: Type, Prop))))("nat" :: Type)("'v_256405719_429396927" :: "nat" :: Type)("'aj_257559038" :: "nat" :: Type))))(({
val rxyz = natInd.value.rec(Type)
rxyz
})("punit" :: Type)(lmbda("'h_159188406_696790367" :: "nat" :: Type)(lmbda("'i_854809894_317859634" :: Type)(("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(("pprod" :: FuncTyp(Type, FuncTyp(Type, Type)))(piDefn("'aj_1612878706" :: "nat" :: Type)(("decidable" :: FuncTyp(Prop, Type))(("eq" :: piDefn("'c_479764664" :: Type)(FuncTyp("'c_479764664" :: Type, FuncTyp("'c_479764664" :: Type, Prop))))("nat" :: Type)("'h_159188406_696790367" :: "nat" :: Type)("'aj_1612878706" :: "nat" :: Type))))("'i_854809894_317859634" :: Type))("punit" :: Type))))("'v_256405719_429396927" :: "nat" :: Type)))("punit.star" :: "punit" :: Type)))))("'ag_1531296106_1367828936" :: "nat" :: Type)))
}