Nuprl Lemma : csm-path-type-sub-pathtype

[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[H:j⊢]. ∀[tau:H j⟶ X].  ({H ⊢ _:((Path_A b))tau} ⊆{H ⊢ _:(Path(A))tau})


Proof




Definitions occuring in Statement :  path-type: (Path_A b) pathtype: Path(A) cubical-term: {X ⊢ _:A} csm-ap-type: (AF)s cubical-type: {X ⊢ _} cube_set_map: A ⟶ B cubical_set: CubicalSet subtype_rel: A ⊆B uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B cube_set_map: A ⟶ B psc_map: A ⟶ B nat-trans: nat-trans(C;D;F;G) cat-ob: cat-ob(C) pi1: fst(t) op-cat: op-cat(C) spreadn: spread4 cube-cat: CubeCat fset: fset(T) quotient: x,y:A//B[x; y] cat-arrow: cat-arrow(C) pi2: snd(t) type-cat: TypeCat all: x:A. B[x] names-hom: I ⟶ J cat-comp: cat-comp(C) compose: g true: True squash: T prop: uimplies: supposing a guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q
Lemmas referenced :  cube_set_map_wf cubical-term_wf cubical-type-cumulativity2 cubical_set_cumulativity-i-j subtype_rel_self path-type-subtype csm-ap-type_wf csm-ap-term_wf subtype_rel_wf squash_wf true_wf istype-universe csm-path-type csm-pathtype iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule axiomEquality hypothesis universeIsType extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality isect_memberEquality_alt isectIsTypeImplies inhabitedIsType because_Cache instantiate applyEquality natural_numberEquality lambdaEquality_alt imageElimination equalityTransitivity equalitySymmetry universeEquality dependent_functionElimination imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination

Latex:
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].  \mforall{}[H:j\mvdash{}].  \mforall{}[tau:H  j{}\mrightarrow{}  X].
    (\{H  \mvdash{}  \_:((Path\_A  a  b))tau\}  \msubseteq{}r  \{H  \mvdash{}  \_:(Path(A))tau\})



Date html generated: 2020_05_20-PM-03_17_40
Last ObjectModification: 2020_04_06-PM-06_32_56

Theory : cubical!type!theory


Home Index