Nuprl Definition : case-type-comp
case-type-comp(G; phi; psi; A; B; cA; cB) ==
λH,sigma,chi,u,a0. (cA H, (∀ (phi)sigma) sigma chi u a0 ∨ cB H, (∀ (psi)sigma) sigma chi u a0)
Definitions occuring in Statement :
case-term: (u ∨ v),
face-forall: (∀ phi),
context-subset: Gamma, phi,
csm-ap-term: (t)s,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
csm-ap-term: (t)s,
face-forall: (∀ phi),
context-subset: Gamma, phi,
apply: f a,
case-term: (u ∨ v),
lambda: λx.A[x]
Latex:
case-type-comp(G; phi; psi; A; B; cA; cB) ==
\mlambda{}H,sigma,chi,u,a0. (cA H, (\mforall{} (phi)sigma) sigma chi u a0 \mvee{} cB H, (\mforall{} (psi)sigma) sigma chi u a0)
Date html generated:
2017_01_10-AM-10_12_48
Last ObjectModification:
2016_12_29-PM-00_42_25
Theory : cubical!type!theory
Home
Index