Nuprl Lemma : uabetatype_wf
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}]. ∀[f:G:CubicalSet{i|j} ⟶ A:{G ⊢ _:c𝕌} ⟶ TransportType(A)]. G ⊢ uabetatype(G;A;B;f)
Proof
Definitions occuring in Statement :
uabetatype: uabetatype(G;A;B;f),
transport-type: TransportType(A),
cubical-universe: c𝕌,
cubical-term: {X ⊢ _:A},
cubical-type: {X ⊢ _},
cubical_set: CubicalSet,
uall: ∀[x:A]. B[x],
member: t ∈ T,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
subtype_rel: A ⊆r B,
guard: {T},
uimplies: b supposing a,
all: ∀x:A. B[x],
true: True,
squash: ↓T,
prop: ℙ,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
implies: P ⇒ Q,
uabetatype: uabetatype(G;A;B;f),
transport-type: TransportType(A)
Lemmas referenced :
cubical-equiv_wf,
universe-decode_wf,
csm-ap-type_wf,
cubical_set_cumulativity-i-j,
cube-context-adjoin_wf,
cubical-type-cumulativity2,
cc-fst_wf,
path-type_wf,
csm-ap-term_wf,
cc-snd_wf,
cubical-term-eqcd,
equiv-fun_wf,
cubical-app_wf_fun,
cubical_set_wf,
istype-cubical-universe-term,
transport-type_wf,
cubical-type_wf,
equal_wf,
squash_wf,
true_wf,
istype-universe,
cubical-equiv-p,
cube_set_map_wf,
subtype_rel_self,
iff_weakening_equal,
univ-a_wf,
cubical-universe-p,
cubical-universe_wf,
csm-universe-decode,
csm-ap-term-universe,
cubical-term_wf,
cubical-fun_wf,
cubical-pi_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
instantiate,
applyEquality,
sqequalRule,
because_Cache,
equalityTransitivity,
equalitySymmetry,
independent_isectElimination,
lambdaEquality_alt,
hyp_replacement,
universeIsType,
functionIsType,
dependent_functionElimination,
natural_numberEquality,
imageElimination,
universeEquality,
inhabitedIsType,
imageMemberEquality,
baseClosed,
productElimination,
independent_functionElimination,
Error :memTop,
cumulativity,
lambdaFormation_alt,
equalityIstype
Latex:
\mforall{}[G:j\mvdash{}]. \mforall{}[A,B:\{G \mvdash{} \_:c\mBbbU{}\}]. \mforall{}[f:G:CubicalSet\{i|j\} {}\mrightarrow{} A:\{G \mvdash{} \_:c\mBbbU{}\} {}\mrightarrow{} TransportType(A)].
G \mvdash{} uabetatype(G;A;B;f)
Date html generated:
2020_05_20-PM-07_42_51
Last ObjectModification:
2020_04_30-AM-11_39_45
Theory : cubical!type!theory
Home
Index