---

Step * 1 of Lemma composition-term_wf


1. [Gamma] : CubicalSet{j}
2. [phi] : {Gamma ⊢ _:𝔽}
3. [A] : {Gamma.𝕀 ⊢ _}
4. [cA] : Gamma.𝕀 ⊢ CompOp(A)
⊢ ∀[u:{Gamma, phi.𝕀 ⊢ _:A}]. ∀[a0:{Gamma ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}].
    (comp cA [phi ⊢→ u] a0 ∈ {Gamma ⊢ _:(A)[1(𝕀)][phi |⟶ (u)[1(𝕀)]]})
BY
{ ((InstLemma `context-subset-adjoin-subtype` [⌜Gamma⌝;⌜𝕀⌝;⌜phi⌝]⋅ THENA Auto)
   THEN Assert ⌜∀u:{Gamma, phi.𝕀 ⊢ _:A}. ({Gamma ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]} ∈ 𝕌{[i' | j']})⌝⋅
   ) }

1
.....assertion..... 
1. [Gamma] : CubicalSet{j}
2. [phi] : {Gamma ⊢ _:𝔽}
3. [A] : {Gamma.𝕀 ⊢ _}
4. [cA] : Gamma.𝕀 ⊢ CompOp(A)
5. {Gamma.𝕀 ⊢ _} ⊆r {Gamma, phi.𝕀 ⊢ _}
⊢ ∀u:{Gamma, phi.𝕀 ⊢ _:A}. ({Gamma ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]} ∈ 𝕌{[i' | j']})

2
1. [Gamma] : CubicalSet{j}
2. [phi] : {Gamma ⊢ _:𝔽}
3. [A] : {Gamma.𝕀 ⊢ _}
4. [cA] : Gamma.𝕀 ⊢ CompOp(A)
5. {Gamma.𝕀 ⊢ _} ⊆r {Gamma, phi.𝕀 ⊢ _}
6. ∀u:{Gamma, phi.𝕀 ⊢ _:A}. ({Gamma ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]} ∈ 𝕌{[i' | j']})
⊢ ∀[u:{Gamma, phi.𝕀 ⊢ _:A}]. ∀[a0:{Gamma ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}].
    (comp cA [phi ⊢→ u] a0 ∈ {Gamma ⊢ _:(A)[1(𝕀)][phi |⟶ (u)[1(𝕀)]]})

---

Latex:

---

Latex:

1.  [Gamma]  :  CubicalSet\{j\}
2.  [phi]  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
3.  [A]  :  \{Gamma.\mBbbI{}  \mvdash{}  \_\}
4.  [cA]  :  Gamma.\mBbbI{}  \mvdash{}  CompOp(A)
\mvdash{}  \mforall{}[u:\{Gamma,  phi.\mBbbI{}  \mvdash{}  \_:A\}].  \mforall{}[a0:\{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}].
        (comp  cA  [phi  \mvdash{}\mrightarrow{}  u]  a0  \mmember{}  \{Gamma  \mvdash{}  \_:(A)[1(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[1(\mBbbI{})]]\})


By

---

Latex:
((InstLemma  `context-subset-adjoin-subtype`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}\mBbbI{}\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Assert  \mkleeneopen{}\mforall{}u:\{Gamma,  phi.\mBbbI{}  \mvdash{}  \_:A\}.  (\{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}  \mmember{}  \mBbbU{}\{[i'  |  j']\})\mkleeneclose{}\mcdot{}
  )

---

Home Index