---

Step * 1 of Lemma extend-to-contraction_wf

.....subterm..... T:t
3:n
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. ext : H:CubicalSet{i|j}
⟶ sigma:H ij⟶ Gamma
⟶ phi:{H ⊢ _:𝔽}
⟶ u:{H, phi ⊢ _:(A)sigma}
⟶ {H ⊢ _:(A)sigma[phi |⟶ u]}
4. uniform-extension-fun{[i | j]:l}(Gamma; A; ext)
5. (q)p ∈ {Gamma.A.𝕀 ⊢ _:((A)p)p}
6. <>(ext Gamma.A.𝕀 p o p (q=1) (q)p) ∈ {Gamma.A ⊢ _:(Path_(A)p (ext Gamma.A.𝕀 p o p (q=1) (q)p)[0(𝕀)] (ext Gamma.A.𝕀 
                                                                                                        p o p 
                                                                                                        (q=1) 
                                                                                                        (q)p)[1(𝕀)])}
⊢ (ext Gamma.A.𝕀 p o p (q=1) (q)p)[0(𝕀)] = (ext Gamma 1(Gamma) 0(𝔽) discr(⋅))p ∈ {Gamma.A ⊢ _:(A)p}
BY
{ (UnfoldTopAb 4 THEN (InstHyp [⌜Gamma.A.𝕀⌝;⌜Gamma.A⌝;⌜[0(𝕀)]⌝;⌜p o p⌝;⌜(q=1)⌝;⌜(q)p⌝] 4⋅ THENA Auto)) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. ext : H:CubicalSet{i|j}
⟶ sigma:H ij⟶ Gamma
⟶ phi:{H ⊢ _:𝔽}
⟶ u:{H, phi ⊢ _:(A)sigma}
⟶ {H ⊢ _:(A)sigma[phi |⟶ u]}
4. ∀H,K:ij⊢. ∀tau:K ij⟶ H. ∀sigma:H ij⟶ Gamma. ∀phi:{H ⊢ _:𝔽}. ∀u:{H, phi ⊢ _:(A)sigma}.
     ((ext H sigma phi u)tau = (ext K sigma o tau (phi)tau (u)tau) ∈ {K ⊢ _:((A)sigma)tau[(phi)tau |⟶ (u)tau]})
5. (q)p ∈ {Gamma.A.𝕀 ⊢ _:((A)p)p}
6. <>(ext Gamma.A.𝕀 p o p (q=1) (q)p) ∈ {Gamma.A ⊢ _:(Path_(A)p (ext Gamma.A.𝕀 p o p (q=1) (q)p)[0(𝕀)] (ext Gamma.A.𝕀 
                                                                                                        p o p 
                                                                                                        (q=1) 
                                                                                                        (q)p)[1(𝕀)])}
7. (ext Gamma.A.𝕀 p o p (q=1) (q)p)[0(𝕀)]
= (ext Gamma.A p o p o [0(𝕀)] ((q=1))[0(𝕀)] ((q)p)[0(𝕀)])
∈ {Gamma.A ⊢ _:((A)p o p)[0(𝕀)][((q=1))[0(𝕀)] |⟶ ((q)p)[0(𝕀)]]}
⊢ (ext Gamma.A.𝕀 p o p (q=1) (q)p)[0(𝕀)] = (ext Gamma 1(Gamma) 0(𝔽) discr(⋅))p ∈ {Gamma.A ⊢ _:(A)p}

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  ext  :  H:CubicalSet\{i|j\}
{}\mrightarrow{}  sigma:H  ij{}\mrightarrow{}  Gamma
{}\mrightarrow{}  phi:\{H  \mvdash{}  \_:\mBbbF{}\}
{}\mrightarrow{}  u:\{H,  phi  \mvdash{}  \_:(A)sigma\}
{}\mrightarrow{}  \{H  \mvdash{}  \_:(A)sigma[phi  |{}\mrightarrow{}  u]\}
4.  uniform-extension-fun\{[i  |  j]:l\}(Gamma;  A;  ext)
5.  (q)p  \mmember{}  \{Gamma.A.\mBbbI{}  \mvdash{}  \_:((A)p)p\}
6.  <>(ext  Gamma.A.\mBbbI{}  p  o  p  (q=1)  (q)p)
      \mmember{}  \{Gamma.A  \mvdash{}  \_:(Path\_(A)p  (ext  Gamma.A.\mBbbI{}  p  o  p  (q=1)  (q)p)[0(\mBbbI{})]  (ext  Gamma.A.\mBbbI{}  p  o  p  (q=1) 
                                                                                                                                          (q)p)[1(\mBbbI{})])\}
\mvdash{}  (ext  Gamma.A.\mBbbI{}  p  o  p  (q=1)  (q)p)[0(\mBbbI{})]  =  (ext  Gamma  1(Gamma)  0(\mBbbF{})  discr(\mcdot{}))p


By

---

Latex:
(UnfoldTopAb  4  THEN  (InstHyp  [\mkleeneopen{}Gamma.A.\mBbbI{}\mkleeneclose{};\mkleeneopen{}Gamma.A\mkleeneclose{};\mkleeneopen{}[0(\mBbbI{})]\mkleeneclose{};\mkleeneopen{}p  o  p\mkleeneclose{};\mkleeneopen{}(q=1)\mkleeneclose{};\mkleeneopen{}(q)p\mkleeneclose{}]  4\mcdot{}  THENA  Auto))

---

Home Index