---

Step * 1 1 of Lemma p+-swap-interval


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))))
BY
{ ((RW (AddrC [2] (UnfoldC `csm-ap-type`)) 0 THEN RW (AddrC [3] (UnfoldC `csm-ap-type`)) 0)
   THEN Reduce 0
   THEN EqCDA
   THEN RepeatFor 2 (((FunExt THENA Auto) THEN Reduce 0))) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. B : {Gamma ⊢ _}
4. I : fset(ℕ)
5. x : Gamma.𝕀.(B)p(I)
⊢ ((fst(A)) I (p)x) = ((fst(A)) I (p+)(swap-interval(Gamma;B))x) ∈ Type

2
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. B : {Gamma ⊢ _}
4. I : fset(ℕ)
5. J : fset(ℕ)
⊢ (λf,a,u. ((snd(A)) I J f (p)a u))
= (λf,a,u. ((snd(A)) I J f (p+)(swap-interval(Gamma;B))a u))
∈ (f:J ⟶ I ⟶ a:Gamma.𝕀.(B)p(I) ⟶ ((fst(A)) I (p)a) ⟶ ((fst(A)) J (p)f(a)))

---

Latex:

---

Latex:

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


By

---

Latex:
((RW  (AddrC  [2]  (UnfoldC  `csm-ap-type`))  0  THEN  RW  (AddrC  [3]  (UnfoldC  `csm-ap-type`))  0)
  THEN  Reduce  0
  THEN  EqCDA
  THEN  RepeatFor  2  (((FunExt  THENA  Auto)  THEN  Reduce  0)))

---

Home Index