Nuprl Lemma : csm-comp-structure_wf2

[Gamma,Delta:j⊢]. ∀[tau:Delta j⟶ Gamma]. ∀[A:{Gamma ⊢ _}]. ∀[cA:Gamma +⊢ Compositon(A)].
  ((cA)tau ∈ Delta +⊢ Compositon((A)tau))


Proof




Definitions occuring in Statement :  csm-comp-structure: (cA)tau composition-structure: Gamma ⊢ Compositon(A) csm-ap-type: (AF)s cubical-type: {X ⊢ _} cube_set_map: A ⟶ B cubical_set: CubicalSet uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B csm-comp-structure: (cA)tau interval-type: 𝕀 csm-comp: F compose: g
Lemmas referenced :  csm-comp-structure_wf cubical_set_cumulativity-i-j cube_set_map_cumulativity-i-j composition-structure_wf cubical-type_wf cube_set_map_wf cubical_set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut thin instantiate extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality applyEquality hypothesis sqequalRule because_Cache axiomEquality equalityTransitivity equalitySymmetry universeIsType isect_memberEquality_alt isectIsTypeImplies inhabitedIsType

Latex:
\mforall{}[Gamma,Delta:j\mvdash{}].  \mforall{}[tau:Delta  j{}\mrightarrow{}  Gamma].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[cA:Gamma  +\mvdash{}  Compositon(A)].
    ((cA)tau  \mmember{}  Delta  +\mvdash{}  Compositon((A)tau))



Date html generated: 2020_05_20-PM-04_35_36
Last ObjectModification: 2020_04_23-PM-01_10_44

Theory : cubical!type!theory


Home Index