Nuprl Definition : ctt-type-type

type(T) ==  fst(snd(T))


Definitions occuring in Statement :  pi1: fst(t),  pi2: snd(t)
Definitions occuring in definition :  pi1: fst(t),  pi2: snd(t)
FDL editor aliases :  cttyt cttyt
Latex:
type(T)  ==    fst(snd(T))


Date html generated: 2020_05_20-PM-07_57_22
Last ObjectModification: 2020_05_05-PM-05_25_28

Theory : cubical!type!theory


Home Index