Nuprl Lemma : constant-A-open-box
∀Gamma,X,I,alpha:Top. ∀[J,x,i:Top]. (A-open-box(Gamma;(X);I;alpha;J;x;i) ~ open_box(X;I;J;x;i))
Proof
Definitions occuring in Statement :
A-open-box: A-open-box(X;A;I;alpha;J;x;i),
open_box: open_box(X;I;J;x;i),
constant-cubical-type: (X),
uall: ∀[x:A]. B[x],
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
member: t ∈ T,
open_box: open_box(X;I;J;x;i),
A-open-box: A-open-box(X;A;I;alpha;J;x;i),
I-face: I-face(X;I),
constant-cubical-type: (X),
A-face: A-face(X;A;I;alpha),
cubical-type-at: A(a),
pi1: fst(t),
adjacent-compatible: adjacent-compatible(X;I;L),
A-adjacent-compatible: A-adjacent-compatible(X;A;I;alpha;L),
face-compatible: face-compatible(X;I;f1;f2),
A-face-compatible: A-face-compatible(X;A;I;alpha;f1;f2),
cubical-type-ap-morph: (u a f),
pi2: snd(t),
face-name: face-name(f),
A-face-name: A-face-name(f)
Lemmas referenced :
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
isect_memberFormation,
introduction,
cut,
sqequalRule,
hypothesis,
sqequalAxiom,
lemma_by_obid,
sqequalHypSubstitution,
isect_memberEquality,
isectElimination,
thin,
hypothesisEquality,
because_Cache
Latex:
\mforall{}Gamma,X,I,alpha:Top. \mforall{}[J,x,i:Top]. (A-open-box(Gamma;(X);I;alpha;J;x;i) \msim{} open\_box(X;I;J;x;i))
Date html generated:
2016_06_16-PM-05_56_31
Last ObjectModification:
2015_12_28-PM-04_27_41
Theory : cubical!sets
Home
Index