---

Step * 2 of Lemma p+-swap-interval


1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. B : {Gamma ⊢ _}
4. (A)p
= ((A)p+)swap-interval(Gamma;B)
∈ (A:I:fset(ℕ) ⟶ Gamma.𝕀.(B)p(I) ⟶ Type × (I:fset(ℕ)
                                            ⟶ J:fset(ℕ)
                                            ⟶ f:J ⟶ I
                                            ⟶ a:Gamma.𝕀.(B)p(I)
                                            ⟶ (A I a)
                                            ⟶ (A J f(a))))
⊢ (A)p = ((A)p+)swap-interval(Gamma;B) ∈ {Gamma.𝕀.(B)p ⊢ _}
BY
{ (InstLemma `cubical-type-equal` [⌜parm{i|j}⌝;⌜parm{i}⌝]⋅ THEN BHyp -1 THEN Auto) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma.\mBbbI{}  \mvdash{}  \_\}
3.  B  :  \{Gamma  \mvdash{}  \_\}
4.  (A)p  =  ((A)p+)swap-interval(Gamma;B)
\mvdash{}  (A)p  =  ((A)p+)swap-interval(Gamma;B)


By

---

Latex:
(InstLemma  `cubical-type-equal`  [\mkleeneopen{}parm\{i|j\}\mkleeneclose{};\mkleeneopen{}parm\{i\}\mkleeneclose{}]\mcdot{}  THEN  BHyp  -1  THEN  Auto)

---

Home Index