---

Step * 2 of Lemma extend-to-contraction_wf

.....subterm..... T:t
4: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)[1(𝕀)] = q ∈ {Gamma.A ⊢ _:(A)p}
BY
{ (GenConclTerm ⌜ext Gamma.A.𝕀 p o p (q=1) (q)p⌝⋅ 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. 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(𝕀)])}
7. v : {Gamma.A.𝕀 ⊢ _:(A)p o p[(q=1) |⟶ (q)p]}
8. (ext Gamma.A.𝕀 p o p (q=1) (q)p) = v ∈ {Gamma.A.𝕀 ⊢ _:(A)p o p[(q=1) |⟶ (q)p]}
⊢ (v)[1(𝕀)] = q ∈ {Gamma.A ⊢ _:(A)p}

---

Latex:

---

Latex:
.....subterm.....  T:t
4: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)[1(\mBbbI{})]  =  q


By

---

Latex:
(GenConclTerm  \mkleeneopen{}ext  Gamma.A.\mBbbI{}  p  o  p  (q=1)  (q)p\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index