Nuprl Lemma : path-eta_wf

[G:j⊢]. ∀[A:{G ⊢ _}]. ∀[pth:{G ⊢ _:Path(A)}].  (path-eta(pth) ∈ {G.𝕀 ⊢ _:(A)p})


Proof




Definitions occuring in Statement :  path-eta: path-eta(pth) pathtype: Path(A) interval-type: 𝕀 cc-fst: p cube-context-adjoin: X.A cubical-term: {X ⊢ _:A} csm-ap-type: (AF)s cubical-type: {X ⊢ _} cubical_set: CubicalSet uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T path-eta: path-eta(pth) subtype_rel: A ⊆B squash: T all: x:A. B[x] true: True cc-snd: q interval-type: 𝕀 cc-fst: p csm-ap-type: (AF)s constant-cubical-type: (X)
Lemmas referenced :  cubicalpath-app_wf cube-context-adjoin_wf cubical_set_cumulativity-i-j interval-type_wf csm-ap-type_wf cc-fst_wf csm-ap-term_wf pathtype_wf cubical-term_wf csm-pathtype cubical-type-cumulativity2 cc-snd_wf cubical-type_wf cubical_set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule thin instantiate extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality applyEquality hypothesis because_Cache lambdaEquality_alt imageElimination dependent_functionElimination natural_numberEquality imageMemberEquality baseClosed equalityTransitivity equalitySymmetry hyp_replacement universeIsType axiomEquality isect_memberEquality_alt isectIsTypeImplies inhabitedIsType

Latex:
\mforall{}[G:j\mvdash{}].  \mforall{}[A:\{G  \mvdash{}  \_\}].  \mforall{}[pth:\{G  \mvdash{}  \_:Path(A)\}].    (path-eta(pth)  \mmember{}  \{G.\mBbbI{}  \mvdash{}  \_:(A)p\})



Date html generated: 2020_05_20-PM-03_16_19
Last ObjectModification: 2020_04_06-PM-05_37_55

Theory : cubical!type!theory


Home Index