Nuprl Lemma : context-adjoin-subset

∀[X,Y:j⊢]. ∀[A:{Y ⊢ _}]. sub_cubical_set{[i | j]:l}(X.A; Y.A) supposing sub_cubical_set{j:l}(X; Y)

Proof

Error : references

Latex:
\mforall{}[X,Y:j\mvdash{}]. \mforall{}[A:\{Y \mvdash{} \_\}]. sub\_cubical\_set\{[i | j]:l\}(X.A; Y.A) supposing sub\_cubical\_set\{j:l\}(X; Y) Date html generated: 2020_05_21-AM-10_30_29 Last ObjectModification: 2020_04_06-PM-00_23_44 Theory : cubical!type!theory Home Index