---

Step * 1 1 2 3 1 of Lemma fill-type-up_wf


1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. Gamma.𝕀 ⊢ ((A)[0(𝕀)])p
5. ∀[b:{Gamma.𝕀.((A)[0(𝕀)])p ⊢ _:(A)p}]. ((λb) ∈ {Gamma.𝕀 ⊢ _:Π((A)[0(𝕀)])p (A)p})
6. Gamma.(A)[0(𝕀)].𝕀 ⊢ (A)p+ ∧ ((cA)p+ ∈ Gamma.(A)[0(𝕀)].𝕀 ⊢ CompOp((A)p+))
7. ∀[u:{Gamma.(A)[0(𝕀)].𝕀, (0(𝔽))p ⊢ _:(A)p+}]. ∀[a0:{Gamma.(A)[0(𝕀)] ⊢ _:((A)p+)[0(𝕀)][0(𝔽) |⟶ u[0]]}].
     (fill (cA)p+ [0(𝔽) ⊢→ u] a0 ∈ {Gamma.(A)[0(𝕀)].𝕀 ⊢ _:(A)p+[(0(𝔽))p |⟶ u]})
8. fill (cA)p+ [0(𝔽) ⊢→ discr(⋅)] q = fill (cA)p+ [0(𝔽) ⊢→ discr(⋅)] q ∈ {Gamma.(A)[0(𝕀)].𝕀 ⊢ _:(A)p+}
9. discr(⋅) = fill (cA)p+ [0(𝔽) ⊢→ discr(⋅)] q ∈ {Gamma.(A)[0(𝕀)].𝕀, (0(𝔽))p ⊢ _:(A)p+}
⊢ (fill (cA)p+ [0(𝔽) ⊢→ discr(⋅)] q)swap-interval(Gamma;(A)[0(𝕀)]) ∈ {Gamma.𝕀.((A)[0(𝕀)])p ⊢ _:(A)p}
BY
{ Fold `member` (-2) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. Gamma.𝕀 ⊢ ((A)[0(𝕀)])p
5. ∀[b:{Gamma.𝕀.((A)[0(𝕀)])p ⊢ _:(A)p}]. ((λb) ∈ {Gamma.𝕀 ⊢ _:Π((A)[0(𝕀)])p (A)p})
6. Gamma.(A)[0(𝕀)].𝕀 ⊢ (A)p+ ∧ ((cA)p+ ∈ Gamma.(A)[0(𝕀)].𝕀 ⊢ CompOp((A)p+))
7. ∀[u:{Gamma.(A)[0(𝕀)].𝕀, (0(𝔽))p ⊢ _:(A)p+}]. ∀[a0:{Gamma.(A)[0(𝕀)] ⊢ _:((A)p+)[0(𝕀)][0(𝔽) |⟶ u[0]]}].
     (fill (cA)p+ [0(𝔽) ⊢→ u] a0 ∈ {Gamma.(A)[0(𝕀)].𝕀 ⊢ _:(A)p+[(0(𝔽))p |⟶ u]})
8. fill (cA)p+ [0(𝔽) ⊢→ discr(⋅)] q ∈ {Gamma.(A)[0(𝕀)].𝕀 ⊢ _:(A)p+}
9. discr(⋅) = fill (cA)p+ [0(𝔽) ⊢→ discr(⋅)] q ∈ {Gamma.(A)[0(𝕀)].𝕀, (0(𝔽))p ⊢ _:(A)p+}
⊢ (fill (cA)p+ [0(𝔽) ⊢→ discr(⋅)] q)swap-interval(Gamma;(A)[0(𝕀)]) ∈ {Gamma.𝕀.((A)[0(𝕀)])p ⊢ _:(A)p}

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma.\mBbbI{}  \mvdash{}  \_\}
3.  cA  :  Gamma.\mBbbI{}  \mvdash{}  CompOp(A)
4.  Gamma.\mBbbI{}  \mvdash{}  ((A)[0(\mBbbI{})])p
5.  \mforall{}[b:\{Gamma.\mBbbI{}.((A)[0(\mBbbI{})])p  \mvdash{}  \_:(A)p\}].  ((\mlambda{}b)  \mmember{}  \{Gamma.\mBbbI{}  \mvdash{}  \_:\mPi{}((A)[0(\mBbbI{})])p  (A)p\})
6.  Gamma.(A)[0(\mBbbI{})].\mBbbI{}  \mvdash{}  (A)p+  \mwedge{}  ((cA)p+  \mmember{}  Gamma.(A)[0(\mBbbI{})].\mBbbI{}  \mvdash{}  CompOp((A)p+))
7.  \mforall{}[u:\{Gamma.(A)[0(\mBbbI{})].\mBbbI{},  (0(\mBbbF{}))p  \mvdash{}  \_:(A)p+\}].
      \mforall{}[a0:\{Gamma.(A)[0(\mBbbI{})]  \mvdash{}  \_:((A)p+)[0(\mBbbI{})][0(\mBbbF{})  |{}\mrightarrow{}  u[0]]\}].
          (fill  (cA)p+  [0(\mBbbF{})  \mvdash{}\mrightarrow{}  u]  a0  \mmember{}  \{Gamma.(A)[0(\mBbbI{})].\mBbbI{}  \mvdash{}  \_:(A)p+[(0(\mBbbF{}))p  |{}\mrightarrow{}  u]\})
8.  fill  (cA)p+  [0(\mBbbF{})  \mvdash{}\mrightarrow{}  discr(\mcdot{})]  q  =  fill  (cA)p+  [0(\mBbbF{})  \mvdash{}\mrightarrow{}  discr(\mcdot{})]  q
9.  discr(\mcdot{})  =  fill  (cA)p+  [0(\mBbbF{})  \mvdash{}\mrightarrow{}  discr(\mcdot{})]  q
\mvdash{}  (fill  (cA)p+  [0(\mBbbF{})  \mvdash{}\mrightarrow{}  discr(\mcdot{})]  q)swap-interval(Gamma;(A)[0(\mBbbI{})])  \mmember{}  \{Gamma.\mBbbI{}.((A)[0(\mBbbI{})])p  \mvdash{}  \_:(A)p\}


By

---

Latex:
Fold  `member`  (-2)

---

Home Index