---

Step * of Lemma comp-to-fill_wf

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[cA:composition-function{j:l,i:l}(Gamma;A)].
  (comp-to-fill(Gamma;cA) ∈ filling-function{j:l, i:l}(Gamma;A))
BY
{ (Auto
   THEN Unfold `composition-function` -1
   THEN Unfolds ``comp-to-fill filling-function`` 0
   THEN RepeatFor 5 (((FunExt THENA Auto) THEN Reduce 0))
   THEN (Assert ((phi)p)m ∈ {H.𝕀.𝕀 ⊢ _:𝔽} BY
               ((Assert p ∈ H.𝕀 j⟶ H BY Auto) THEN (Assert m ∈ H.𝕀.𝕀 j⟶ H.𝕀 BY Auto) THEN Auto))
   THEN (Assert (u)m ∈ {H.𝕀.𝕀, ((phi)p)m ⊢ _:((A)sigma)m} BY
               ((MemCD THEN Try (Trivial) THEN Thin (-2)) THEN Auto))
   THEN Assert ⌜((a0)p)m ∈ {H.𝕀.𝕀, ((q=0))p ⊢ _:(A)sigma o m}⌝⋅) }

1
.....assertion..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : H:CubicalSet{j}
⟶ sigma:H.𝕀 j⟶ Gamma
⟶ phi:{H ⊢ _:𝔽}
⟶ u:{H, phi.𝕀 ⊢ _:(A)sigma}
⟶ a0:{H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
⟶ {H ⊢ _:((A)sigma)[1(𝕀)][phi |⟶ (u)[1(𝕀)]]}
4. H : CubicalSet{j}
5. sigma : H.𝕀 j⟶ Gamma
6. phi : {H ⊢ _:𝔽}
7. u : {H.𝕀, (phi)p ⊢ _:(A)sigma}
8. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ u[0]]}
9. ((phi)p)m ∈ {H.𝕀.𝕀 ⊢ _:𝔽}
10. (u)m ∈ {H.𝕀.𝕀, ((phi)p)m ⊢ _:((A)sigma)m}
⊢ ((a0)p)m ∈ {H.𝕀.𝕀, ((q=0))p ⊢ _:(A)sigma o m}

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[cA:composition-function\{j:l,i:l\}(Gamma;A)].
    (comp-to-fill(Gamma;cA)  \mmember{}  filling-function\{j:l,  i:l\}(Gamma;A))


By

---

Latex:
(Auto
  THEN  Unfold  `composition-function`  -1
  THEN  Unfolds  ``comp-to-fill  filling-function``  0
  THEN  RepeatFor  5  (((FunExt  THENA  Auto)  THEN  Reduce  0))
  THEN  (Assert  ((phi)p)m  \mmember{}  \{H.\mBbbI{}.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}  BY
                          ((Assert  p  \mmember{}  H.\mBbbI{}  j{}\mrightarrow{}  H  BY  Auto)  THEN  (Assert  m  \mmember{}  H.\mBbbI{}.\mBbbI{}  j{}\mrightarrow{}  H.\mBbbI{}  BY  Auto)  THEN  Auto))
  THEN  (Assert  (u)m  \mmember{}  \{H.\mBbbI{}.\mBbbI{},  ((phi)p)m  \mvdash{}  \_:((A)sigma)m\}  BY
                          ((MemCD  THEN  Try  (Trivial)  THEN  Thin  (-2))  THEN  Auto))
  THEN  Assert  \mkleeneopen{}((a0)p)m  \mmember{}  \{H.\mBbbI{}.\mBbbI{},  ((q=0))p  \mvdash{}  \_:(A)sigma  o  m\}\mkleeneclose{}\mcdot{})

---

Home Index