Nuprl Lemma : csm-pi_comp
∀[X,Y,tau,A,cA,cB:Top]. ((pi_comp(X;A;cA;cB))tau ~ pi_comp(Y;(A)tau;(cA)tau;(cB)tau+))
Proof
Definitions occuring in Statement :
pi_comp: pi_comp(X;A;cA;cB),
csm-comp-structure: (cA)tau,
csm+: tau+,
cube-context-adjoin: X.A,
csm-ap-type: (AF)s,
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
csm-comp-structure: (cA)tau,
pi_comp: pi_comp(X;A;cA;cB),
let: let,
cubical-lambda: (λb),
comp_term: comp cA [phi ⟶ u] a0,
csm-ap-type: (AF)s,
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
so_apply: x[s1;s2;s3;s4],
so_lambda: λ2x y.t[x; y],
top: Top,
so_apply: x[s1;s2],
uimplies: b supposing a,
csm-ap: (s)x,
csm-comp: G o F,
compose: f o g,
csm-id-adjoin: [u],
csm-adjoin: (s;u),
csm-id: 1(X),
interval-1: 1(𝕀),
dM1: 1,
lattice-1: 1,
record-select: r.x,
dM: dM(I),
free-DeMorgan-algebra: free-DeMorgan-algebra(T;eq),
mk-DeMorgan-algebra: mk-DeMorgan-algebra(L;n),
record-update: r[x := v],
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
bfalse: ff,
free-DeMorgan-lattice: free-DeMorgan-lattice(T;eq),
free-dist-lattice: free-dist-lattice(T; eq),
mk-bounded-distributive-lattice: mk-bounded-distributive-lattice,
mk-bounded-lattice: mk-bounded-lattice(T;m;j;z;o),
btrue: tt,
fset-singleton: {x},
cons: [a / b],
empty-fset: {},
nil: [],
it: ⋅,
cc-fst: p,
csm+: tau+,
cc-snd: q,
all: ∀x:A. B[x],
implies: P ⇒ Q,
prop: ℙ,
pi2: snd(t),
pi1: fst(t),
csm-ap-term: (t)s,
revfill: revfill(Gamma;cA;a1),
rev_fill_term: rev_fill_term(Gamma;cA;phi;u;a1)
Lemmas referenced :
top_wf,
lifting-strict-spread,
strict4-spread,
equal_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
because_Cache,
cut,
introduction,
extract_by_obid,
hypothesis,
sqequalRule,
sqequalHypSubstitution,
isectElimination,
thin,
baseClosed,
isect_memberEquality,
voidElimination,
voidEquality,
independent_isectElimination,
lambdaFormation,
equalityTransitivity,
equalitySymmetry,
hypothesisEquality,
dependent_functionElimination,
independent_functionElimination
Latex:
\mforall{}[X,Y,tau,A,cA,cB:Top]. ((pi\_comp(X;A;cA;cB))tau \msim{} pi\_comp(Y;(A)tau;(cA)tau;(cB)tau+))
Date html generated:
2017_10_05-AM-07_15_01
Last ObjectModification:
2017_07_28-AM-10_48_06
Theory : cubical!type!theory
Home
Index