---

Step * of Lemma cubical-contr_wf

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[cA:Gamma ⊢ CompOp(A)]. ∀[p:{Gamma ⊢ _:Contractible(A)}]. ∀[phi:{Gamma ⊢ _:𝔽}].
∀[u:{Gamma, phi ⊢ _:(A)iota}].
  (cubical-contr(Gamma; A; cA; p; phi; u) ∈ {Gamma ⊢ _:A[phi |⟶ u]})
BY
{ ((Intros THEN Unhide)
   THEN Unfold `cubical-contr` 0
   THEN (Assert ⌜Gamma.A ⊢ ((Path_((A)p)p (q)p q))([p.1] o p;q)⌝⋅ THENA Auto)
   THEN (InstLemma `csm-ap-type-iota` [⌜Gamma, phi⌝;⌜A⌝]⋅ THENA Auto)
   THEN (GenConcl ⌜u = uu ∈ {Gamma, phi ⊢ _:A}⌝⋅ THENA (InferEqualType THEN (Trivial ORELSE (EqCDA THEN Auto))))
   THEN ThinVar `u'
   THEN RenameTo `u' `uu'
   THEN (Assert {Gamma, phi ⊢ _:(Path_A p.1 u)} ∈ 𝕌{[i | j']} BY
               (Unfold `contractible-type` 4
                THEN (Assert p.1 ∈ {Gamma, phi ⊢ _:A} BY
                            (SubsumeC ⌜{Gamma ⊢ _:A}⌝⋅ THEN Auto))
                THEN Auto))
   THEN Assert ⌜app(p.2; u) ∈ {Gamma, phi ⊢ _:(Path_A p.1 u)}⌝⋅) }

1
.....assertion..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ CompOp(A)
4. p : {Gamma ⊢ _:Contractible(A)}
5. phi : {Gamma ⊢ _:𝔽}
6. Gamma.A ⊢ ((Path_((A)p)p (q)p q))([p.1] o p;q)
7. (A)iota = A ∈ {Gamma, phi ⊢ _}
8. u : {Gamma, phi ⊢ _:A}
9. {Gamma, phi ⊢ _:(Path_A p.1 u)} ∈ 𝕌{[i | j']}
⊢ app(p.2; u) ∈ {Gamma, phi ⊢ _:(Path_A p.1 u)}

2
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ CompOp(A)
4. p : {Gamma ⊢ _:Contractible(A)}
5. phi : {Gamma ⊢ _:𝔽}
6. Gamma.A ⊢ ((Path_((A)p)p (q)p q))([p.1] o p;q)
7. (A)iota = A ∈ {Gamma, phi ⊢ _}
8. u : {Gamma, phi ⊢ _:A}
9. {Gamma, phi ⊢ _:(Path_A p.1 u)} ∈ 𝕌{[i | j']}
10. app(p.2; u) ∈ {Gamma, phi ⊢ _:(Path_A p.1 u)}
⊢ comp (cA)p [phi ⊢→ (app(p.2; u))p @ q] p.1 ∈ {Gamma ⊢ _:A[phi |⟶ u]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[cA:Gamma  \mvdash{}  CompOp(A)].  \mforall{}[p:\{Gamma  \mvdash{}  \_:Contractible(A)\}].
\mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[u:\{Gamma,  phi  \mvdash{}  \_:(A)iota\}].
    (cubical-contr(Gamma;  A;  cA;  p;  phi;  u)  \mmember{}  \{Gamma  \mvdash{}  \_:A[phi  |{}\mrightarrow{}  u]\})


By

---

Latex:
((Intros  THEN  Unhide)
  THEN  Unfold  `cubical-contr`  0
  THEN  (Assert  \mkleeneopen{}Gamma.A  \mvdash{}  ((Path\_((A)p)p  (q)p  q))([p.1]  o  p;q)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `csm-ap-type-iota`  [\mkleeneopen{}Gamma,  phi\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}u  =  uu\mkleeneclose{}\mcdot{}  THENA  (InferEqualType  THEN  (Trivial  ORELSE  (EqCDA  THEN  Auto))))
  THEN  ThinVar  `u'
  THEN  RenameTo  `u'  `uu'
  THEN  (Assert  \{Gamma,  phi  \mvdash{}  \_:(Path\_A  p.1  u)\}  \mmember{}  \mBbbU{}\{[i  |  j']\}  BY
                          (Unfold  `contractible-type`  4
                            THEN  (Assert  p.1  \mmember{}  \{Gamma,  phi  \mvdash{}  \_:A\}  BY
                                                    (SubsumeC  \mkleeneopen{}\{Gamma  \mvdash{}  \_:A\}\mkleeneclose{}\mcdot{}  THEN  Auto))
                            THEN  Auto))
  THEN  Assert  \mkleeneopen{}app(p.2;  u)  \mmember{}  \{Gamma,  phi  \mvdash{}  \_:(Path\_A  p.1  u)\}\mkleeneclose{}\mcdot{})

---

Home Index