Nuprl Definition : cubical-type-ap-morph

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


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_05_18-PM-01_38_21
Last ObjectModification: 2015_10_28-PM-04_25_20

Theory : cubical!type!theory


Home Index