---

Step * 1 of Lemma comp-to-fill_wf2

.....set predicate..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : composition-function{j:l,i:l}(Gamma;A)
4. uniform-comp-function{j:l, i:l}(Gamma; A; cA)
⊢ uniform-filling-function{j:l, i:l}(Gamma;A;comp-to-fill(Gamma;cA))
BY
{ (D 0 THEN Intros THEN Try (MemCD) THEN RepUR ``comp-to-fill`` 0) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : composition-function{j:l,i:l}(Gamma;A)
4. uniform-comp-function{j:l, i:l}(Gamma; A; cA)
5. H : CubicalSet{j}
6. K : CubicalSet{j}
7. tau : K j⟶ H
8. sigma : H.𝕀 j⟶ Gamma
9. phi : {H ⊢ _:𝔽}
10. u : {H.𝕀, (phi)p ⊢ _:(A)sigma}
11. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ u[0]]}
⊢ (cA H.𝕀 sigma o m ((phi)p ∨ (q=0)) ((u)m ∨ ((a0)p)m) (a0)p)tau+
= (cA K.𝕀 sigma o tau+ o m (((phi)tau)p ∨ (q=0)) (((u)tau+)m ∨ (((a0)tau)p)m) ((a0)tau)p)
∈ {K.𝕀 ⊢ _:((A)sigma)tau+}

2
.....wf..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : composition-function{j:l,i:l}(Gamma;A)
4. uniform-comp-function{j:l, i:l}(Gamma; A; cA)
⊢ istype(CubicalSet{j})

---

Latex:

---

Latex:
.....set  predicate..... 
1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  cA  :  composition-function\{j:l,i:l\}(Gamma;A)
4.  uniform-comp-function\{j:l,  i:l\}(Gamma;  A;  cA)
\mvdash{}  uniform-filling-function\{j:l,  i:l\}(Gamma;A;comp-to-fill(Gamma;cA))


By

---

Latex:
(D  0  THEN  Intros  THEN  Try  (MemCD)  THEN  RepUR  ``comp-to-fill``  0)

---

Home Index