Nuprl Lemma : csm-comp-op-to-comp-fun
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[cA:Gamma ⊢ CompOp(A)]. ∀[H,K:j⊢]. ∀[tau:K j⟶ H]. ∀[sigma:H.𝕀 j⟶ Gamma].
∀[phi:{H ⊢ _:𝔽}]. ∀[u:{H, phi.𝕀 ⊢ _:(A)sigma}]. ∀[a0:{H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}].
((cop-to-cfun(cA) H sigma phi u a0)tau
= (cop-to-cfun(cA) K sigma o tau+ (phi)tau (u)tau+ (a0)tau)
∈ {K ⊢ _:(((A)sigma)[1(𝕀)])tau[(phi)tau |⟶ ((u)[1(𝕀)])tau]})
Proof
Definitions occuring in Statement :
comp-op-to-comp-fun: cop-to-cfun(cA),
composition-op: Gamma ⊢ CompOp(A),
constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]},
context-subset: Gamma, phi,
face-type: 𝔽,
interval-1: 1(𝕀),
interval-0: 0(𝕀),
interval-type: 𝕀,
csm+: tau+,
csm-id-adjoin: [u],
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
cubical-term: {X ⊢ _:A},
csm-ap-type: (AF)s,
cubical-type: {X ⊢ _},
csm-comp: G o F,
cube_set_map: A ⟶ B,
cubical_set: CubicalSet,
uall: ∀[x:A]. B[x],
apply: f a,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
csm-id-adjoin: [u],
csm-id: 1(X),
uimplies: b supposing a,
subtype_rel: A ⊆r B,
and: P ∧ Q,
cand: A c∧ B,
constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]},
comp-op-to-comp-fun: cop-to-cfun(cA),
csm+: tau+,
csm-comp: G o F,
implies: P ⇒ Q,
all: ∀x:A. B[x],
guard: {T},
csm-ap: (s)x,
csm-adjoin: (s;u),
interval-0: 0(𝕀),
prop: ℙ,
squash: ↓T,
true: True,
compose: f o g,
constant-cubical-type: (X),
cc-fst: p,
cc-snd: q,
csm-ap-type: (AF)s,
interval-type: 𝕀,
cubical-type: {X ⊢ _},
pi2: snd(t),
pi1: fst(t),
csm-ap-term: (t)s,
interval-1: 1(𝕀),
composition-function: composition-function{j:l,i:l}(Gamma;A),
subset-iota: iota
Lemmas referenced :
csm-ap-type_wf,
cube-context-adjoin_wf,
interval-type_wf,
csm-id-adjoin_wf,
interval-0_wf,
csm-ap-term_wf,
context-subset_wf,
thin-context-subset-adjoin,
csm-id-adjoin_wf-interval-0,
constrained-cubical-term-eqcd,
istype-cubical-term,
face-type_wf,
cube_set_map_wf,
composition-op_wf,
cubical_set_cumulativity-i-j,
cubical-type-cumulativity2,
cubical-type_wf,
cubical_set_wf,
interval-1_wf,
csm-id-adjoin_wf-interval-1,
csm-composition-comp,
csm+_wf_interval,
csm-composition_wf,
composition-term-uniformity,
constrained-cubical-term_wf,
equal_wf,
squash_wf,
true_wf,
istype-universe,
cubical-term_wf,
composition-term_wf,
csm-face-type,
csm-comp_wf,
context-subset-map,
csm-context-subset-subtype3,
csm-constrained-cubical-term,
cubical-term-eqcd,
csm-context-subset-subtype2,
subset-cubical-term2,
sub_cubical_set_self,
thin-context-subset,
subset-cubical-type,
context-subset-is-subset,
equal_functionality_wrt_subtype_rel2,
cubical-type-cumulativity,
subtype_rel_self,
comp-op-to-comp-fun_wf,
context-subset-term-subtype
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
universeIsType,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
instantiate,
hypothesis,
hypothesisEquality,
equalityTransitivity,
equalitySymmetry,
independent_isectElimination,
because_Cache,
inhabitedIsType,
applyEquality,
sqequalRule,
lambdaEquality_alt,
cumulativity,
universeEquality,
independent_pairFormation,
promote_hyp,
productElimination,
dependent_set_memberEquality_alt,
independent_functionElimination,
dependent_functionElimination,
equalityIstype,
lambdaFormation_alt,
rename,
hyp_replacement,
imageElimination,
natural_numberEquality,
imageMemberEquality,
baseClosed,
applyLambdaEquality,
Error :memTop,
setElimination,
functionEquality
Latex:
\mforall{}[Gamma:j\mvdash{}]. \mforall{}[A:\{Gamma \mvdash{} \_\}]. \mforall{}[cA:Gamma \mvdash{} CompOp(A)]. \mforall{}[H,K:j\mvdash{}]. \mforall{}[tau:K j{}\mrightarrow{} H].
\mforall{}[sigma:H.\mBbbI{} j{}\mrightarrow{} Gamma]. \mforall{}[phi:\{H \mvdash{} \_:\mBbbF{}\}]. \mforall{}[u:\{H, phi.\mBbbI{} \mvdash{} \_:(A)sigma\}].
\mforall{}[a0:\{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})][phi |{}\mrightarrow{} (u)[0(\mBbbI{})]]\}].
((cop-to-cfun(cA) H sigma phi u a0)tau
= (cop-to-cfun(cA) K sigma o tau+ (phi)tau (u)tau+ (a0)tau))
Date html generated:
2020_05_20-PM-04_26_48
Last ObjectModification:
2020_05_02-AM-09_29_47
Theory : cubical!type!theory
Home
Index