Nuprl Lemma : csm-ap-type-fst-id-adjoin

[X:j⊢]. ∀[B:{X ⊢ _}]. ∀[u:Top].  (((B)p)[u] B ∈ {X ⊢ _})


Proof




Definitions occuring in Statement :  csm-id-adjoin: [u] cc-fst: p csm-ap-type: (AF)s cubical-type: {X ⊢ _} cubical_set: CubicalSet uall: [x:A]. B[x] top: Top equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T cubical_set: CubicalSet csm-ap-type: (AF)s pscm-ap-type: (AF)s csm-ap: (s)x pscm-ap: (s)x cc-fst: p psc-fst: p csm-id-adjoin: [u] pscm-id-adjoin: [u] csm-adjoin: (s;u) pscm-adjoin: (s;u) csm-id: 1(X) pscm-id: 1(X)
Lemmas referenced :  pscm-ap-type-fst-id-adjoin cube-cat_wf cubical-type-sq-presheaf-type
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesis sqequalRule Error :memTop

Latex:
\mforall{}[X:j\mvdash{}].  \mforall{}[B:\{X  \mvdash{}  \_\}].  \mforall{}[u:Top].    (((B)p)[u]  =  B)



Date html generated: 2020_05_20-PM-01_57_36
Last ObjectModification: 2020_04_03-PM-08_31_37

Theory : cubical!type!theory


Home Index