---

Step * of Lemma extend-to-contraction_wf

No Annotations
∀Gamma:j⊢. ∀A:{Gamma ⊢ _}. ∀ext:Gamma +⊢ Extension(A).
  (extend-to-contraction(Gamma;A;ext) ∈ {Gamma ⊢ _:Contractible(A)})
BY
{ (Auto
   THEN D -1
   THEN Unfold `extension-fun` -2
   THEN (Assert (q)p ∈ ⌜{Gamma.A.𝕀 ⊢ _:((A)p)p}⌝ BY
               Auto)
   THEN Unfold `extend-to-contraction` 0
   THEN MemCD
   THEN Auto
   THEN (InstLemmaIJ `term-to-path_wf` [⌜Gamma.A⌝;⌜(A)p⌝;⌜ext Gamma.A.𝕀 p o p (q=1) (q)p⌝]⋅ THENA Auto)
   THEN InferEqualType
   THEN Try (Trivial)
   THEN RepeatFor 2 (EqCDA)) }

1
.....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}

2
.....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}

---

Latex:

---

Latex:
No  Annotations
\mforall{}Gamma:j\mvdash{}.  \mforall{}A:\{Gamma  \mvdash{}  \_\}.  \mforall{}ext:Gamma  +\mvdash{}  Extension(A).
    (extend-to-contraction(Gamma;A;ext)  \mmember{}  \{Gamma  \mvdash{}  \_:Contractible(A)\})


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  Unfold  `extension-fun`  -2
  THEN  (Assert  (q)p  \mmember{}  \mkleeneopen{}\{Gamma.A.\mBbbI{}  \mvdash{}  \_:((A)p)p\}\mkleeneclose{}  BY
                          Auto)
  THEN  Unfold  `extend-to-contraction`  0
  THEN  MemCD
  THEN  Auto
  THEN  (InstLemmaIJ  `term-to-path\_wf`  [\mkleeneopen{}Gamma.A\mkleeneclose{};\mkleeneopen{}(A)p\mkleeneclose{};\mkleeneopen{}ext  Gamma.A.\mBbbI{}  p  o  p  (q=1)  (q)p\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  InferEqualType
  THEN  Try  (Trivial)
  THEN  RepeatFor  2  (EqCDA))

---

Home Index