---

Step * of Lemma p+-swap-interval

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[B:{Gamma ⊢ _}].  (((A)p+)swap-interval(Gamma;B) = (A)p ∈ {Gamma.𝕀.(B)p ⊢ _})
BY
{ (Intros
   THEN Symmetry
   THEN Assert ⌜(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))))⌝⋅) }

1
.....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))))

2
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 ⊢ _}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[B:\{Gamma  \mvdash{}  \_\}].    (((A)p+)swap-interval(Gamma;B)  =  (A)p)


By

---

Latex:
(Intros  THEN  Symmetry  THEN  Assert  \mkleeneopen{}(A)p  =  ((A)p+)swap-interval(Gamma;B)\mkleeneclose{}\mcdot{})

---

Home Index