Nuprl Definition : cubical-type-ap-morph

(u a f) ==  (snd(A)) I J f a u


Wellformedness Lemmas :  cubical-type-ap-morph_wf
Definitions occuring in Statement :  pi2: snd(t),  apply: f a
Definitions occuring in definition :  apply: f a,  pi2: snd(t)
FDL editor aliases :  cubical-type-ap-morph cubical-type-ap-morph
Latex:
(u  a  f)  ==    (snd(A))  I  J  f  a  u


Date html generated: 2016_06_16-PM-05_38_50
Last ObjectModification: 2015_09_23-AM-09_30_16

Theory : cubical!sets


Home Index