Nuprl Lemma : trivial-same-cubical-context

∀X,Y:?CubicalContext.  ((Y = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext) ⇒ (X = Y ∈ ?CubicalContext))


Proof

Error : references
Latex:
\mforall{}X,Y:?CubicalContext.    ((Y  =  bind-provision(X;ctxt.OK(ctxt)))  {}\mRightarrow{}  (X  =  Y))


Date html generated: 2020_05_21-AM-10_31_32
Last ObjectModification: 2020_05_18-AM-11_09_17

Theory : cubical!type!theory


Home Index