Nuprl Lemma : csm-case-type-comp
∀[H,Gamma,tau,phi,psi,A,B,cA,cB:Top].
((case-type-comp(Gamma; phi; psi; A; B; cA; cB))tau ~ case-type-comp(H;
(phi)tau;
(psi)tau;
(A)tau;
(B)tau;
(cA)tau;
(cB)tau))
Proof
Definitions occuring in Statement :
case-type-comp: case-type-comp(G; phi; psi; A; B; cA; cB),
csm-comp-structure: (cA)tau,
csm-ap-term: (t)s,
csm-ap-type: (AF)s,
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
case-type-comp: case-type-comp(G; phi; psi; A; B; cA; cB),
csm-comp-structure: (cA)tau,
csm-ap-term: (t)s,
csm-comp: G o F,
compose: f o g,
csm-ap: (s)x,
member: t ∈ T
Lemmas referenced :
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
sqequalRule,
because_Cache,
cut,
introduction,
extract_by_obid,
hypothesis
Latex:
\mforall{}[H,Gamma,tau,phi,psi,A,B,cA,cB:Top].
((case-type-comp(Gamma; phi; psi; A; B; cA; cB))tau \msim{} case-type-comp(H;
(phi)tau;
(psi)tau;
(A)tau;
(B)tau;
(cA)tau;
(cB)tau))
Date html generated:
2017_01_10-AM-10_20_49
Last ObjectModification:
2017_01_01-PM-02_04_44
Theory : cubical!type!theory
Home
Index