---

Step * 1 of Lemma p+-swap-interval

.....assertion..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. B : {Gamma ⊢ _}
⊢ (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))))
BY
{ (Subst' A ~ <fst(A), snd(A)> 0 THENA (RepeatFor 2 (DVar `A') THEN Reduce 0 THEN Auto)) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. B : {Gamma ⊢ _}
⊢ (<fst(A), snd(A)>)p
= ((<fst(A), snd(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))))

---

Latex:

---

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


By

---

Latex:
(Subst'  A  \msim{}  <fst(A),  snd(A)>  0  THENA  (RepeatFor  2  (DVar  `A')  THEN  Reduce  0  THEN  Auto))

---

Home Index