Nuprl Definition : presheaf-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 : presheaf-type-ap-morph

Latex:
(u a f) == (snd(A)) I J f a u Date html generated: 2018_05_22-PM-10_02_35 Last ObjectModification: 2018_02_21-AM-11_32_29 Theory : presheaf!models!of!type!theory Home Index