gistfile1.txt

@ val Circle = "S" :: Type 
Circle: Typ[Term] with Subs[Typ[Term]] = S : 𝒰 _0
@   val base = "base" :: Circle 
base: Term with Subs[Term] = base : (S : 𝒰 _0)
@   val loop = "loop" :: (base =:= base) 
loop: Term with Subs[Term] = loop : (base : (S : 𝒰 _0) = base : (S : 𝒰 _0))
@   val X = "X" :: Type 
X: Typ[Term] with Subs[Typ[Term]] = X : 𝒰 _0
@   val a = "a" :: X 
a: Term with Subs[Term] = a : (X : 𝒰 _0)
@   val l = "l" :: (a =:= a) 
l: Term with Subs[Term] = l : (a : (X : 𝒰 _0) = a : (X : 𝒰 _0))
@   val recS = "rec_S" :: X ~>: (a ~>: (l ~>: (Circle ->: X))) 
recS: FuncLike[Typ[Term] with Subs[Typ[Term]], FuncLike[Term with Subs[Term], FuncLike[Term with Subs[Term], Func[Term, Term]]]] with Subs[FuncLike[Typ[Term] with Subs[Typ[Term]], FuncLike[Term with Subs[Term], FuncLike[Term with Subs[Term], Func[Term, Term]]]]] = rec_S : (X : 𝒰 _0 ~> a : (X : 𝒰 _0) ~> l : (a : (X : 𝒰 _0) = a : (X : 𝒰 _0)) ~> (S : 𝒰 _0) → (X : 𝒰 _0))