Nuprl Lemma : face-one-interval-1

[H:j⊢]. ((1(𝕀)=1) 1(𝔽) ∈ {H ⊢ _:𝔽})


Proof




Definitions occuring in Statement :  face-one: (i=1) face-1: 1(𝔽) face-type: 𝔽 interval-1: 1(𝕀) cubical-term: {X ⊢ _:A} cubical_set: CubicalSet uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] face-1: 1(𝔽) interval-1: 1(𝕀) face-one: (i=1) cubical-term-at: u(a) member: t ∈ T subtype_rel: A ⊆B lattice-point: Point(l) record-select: r.x face_lattice: face_lattice(I) face-lattice: face-lattice(T;eq) free-dist-lattice-with-constraints: free-dist-lattice-with-constraints(T;eq;x.Cs[x]) constrained-antichain-lattice: constrained-antichain-lattice(T;eq;P) mk-bounded-distributive-lattice: mk-bounded-distributive-lattice mk-bounded-lattice: mk-bounded-lattice(T;m;j;z;o) record-update: r[x := v] ifthenelse: if then else fi  eq_atom: =a y bfalse: ff btrue: tt cubical-type-at: A(a) pi1: fst(t) face-type: 𝔽 constant-cubical-type: (X) I_cube: A(I) functor-ob: ob(F) face-presheaf: 𝔽 uimplies: supposing a
Lemmas referenced :  dM-to-FL-dM1 subtype_rel_self cubical-type-at_wf_face-type I_cube_wf fset_wf nat_wf cubical-term-equal face-type_wf face-one_wf interval-1_wf cubical_set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut functionExtensionality sqequalRule introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality Error :memTop,  equalityTransitivity equalitySymmetry independent_isectElimination universeIsType instantiate

Latex:
\mforall{}[H:j\mvdash{}].  ((1(\mBbbI{})=1)  =  1(\mBbbF{}))



Date html generated: 2020_05_20-PM-02_44_05
Last ObjectModification: 2020_04_04-PM-04_58_13

Theory : cubical!type!theory


Home Index