---

Step * of Lemma cubical-fun-ext_wf

No Annotations
∀X:j⊢. ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀f,g:{X ⊢ _:ΠA B}. ∀e:{X ⊢ _:ΠA (Path_B app((f)p; q) app((g)p; q))}.
  (cubical-fun-ext(X;e) ∈ {X ⊢ _:(Path_ΠA B f g)})
BY
{ (RepeatFor 5 (Intro)
   THEN (InstLemma `cubical-pi-p` [⌜X⌝;⌜A⌝;⌜A⌝;⌜B⌝]⋅ THENA Auto)
   THEN (Assert (f)p ∈ {X.A ⊢ _:Π(A)p (B)(p o p;q)} BY
               ((Assert (f)p ∈ {X.A ⊢ _:(ΠA B)p} BY Auto) THEN InferEqualType THEN Try (Trivial) THEN EqCDA THEN Auto))
   THEN (Assert (g)p ∈ {X.A ⊢ _:Π(A)p (B)(p o p;q)} BY
               ((Assert (g)p ∈ {X.A ⊢ _:(ΠA B)p} BY Auto) THEN InferEqualType THEN Try (Trivial) THEN EqCDA THEN Auto))
   THEN (Assert app((f)p; q) ∈ {X.A ⊢ _:(B)(p;q)} BY
               (InferEqualType
                THENL [(EqCDA THEN (Subst' ((B)(p o p;q))[q] ~ (B)(p;q) 0 THENA (CsmUnfolding THEN Auto)) THEN Auto)
                      ; Auto]
               ))
   THEN (Assert app((g)p; q) ∈ {X.A ⊢ _:(B)(p;q)} BY
               (InferEqualType
                THENL [(EqCDA THEN (Subst' ((B)(p o p;q))[q] ~ (B)(p;q) 0 THENA (CsmUnfolding THEN Auto)) THEN Auto)
                      ; Auto]
               ))
   THEN Intro
   THEN (InstLemmaIJ `csm-cubical-pi` [⌜X⌝;⌜X.𝕀.(A)p⌝;⌜A⌝;⌜B⌝;⌜p o p⌝]⋅ THENA Auto)
   THEN (Assert (f)p o p ∈ {X.𝕀.(A)p ⊢ _:Π(A)p o p (B)(p o p o p;q)} BY
               ((InstLemmaIJ `csm-ap-term_wf` [⌜X.𝕀.(A)p⌝;⌜X⌝;⌜ΠA B⌝;⌜p o p⌝;⌜f⌝]⋅ THENA Auto)
                THEN InferEqualType
                THEN Try (Trivial)
                THEN EqCDA
                THEN Auto))
   THEN (Assert (g)p o p ∈ {X.𝕀.(A)p ⊢ _:Π(A)p o p (B)(p o p o p;q)} BY
               ((InstLemmaIJ `csm-ap-term_wf` [⌜X.𝕀.(A)p⌝;⌜X⌝;⌜ΠA B⌝;⌜p o p⌝;⌜g⌝]⋅ THENA Auto)
                THEN InferEqualType
                THEN Try (Trivial)
                THEN EqCDA
                THEN Auto))) }

1
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. f : {X ⊢ _:ΠA B}
5. g : {X ⊢ _:ΠA B}
6. (ΠA B)p = X.A ⊢ Π(A)p (B)(p o p;q) ∈ {X.A ⊢ _}
7. (f)p ∈ {X.A ⊢ _:Π(A)p (B)(p o p;q)}
8. (g)p ∈ {X.A ⊢ _:Π(A)p (B)(p o p;q)}
9. app((f)p; q) ∈ {X.A ⊢ _:(B)(p;q)}
10. app((g)p; q) ∈ {X.A ⊢ _:(B)(p;q)}
11. e : {X ⊢ _:ΠA (Path_B app((f)p; q) app((g)p; q))}
12. (ΠA B)p o p = X.𝕀.(A)p ⊢ Π(A)p o p (B)(p o p o p;q) ∈ {X.𝕀.(A)p ⊢ _}
13. (f)p o p ∈ {X.𝕀.(A)p ⊢ _:Π(A)p o p (B)(p o p o p;q)}
14. (g)p o p ∈ {X.𝕀.(A)p ⊢ _:Π(A)p o p (B)(p o p o p;q)}
⊢ cubical-fun-ext(X;e) ∈ {X ⊢ _:(Path_ΠA B f g)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:j\mvdash{}.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}B:\{X.A  \mvdash{}  \_\}.  \mforall{}f,g:\{X  \mvdash{}  \_:\mPi{}A  B\}.
\mforall{}e:\{X  \mvdash{}  \_:\mPi{}A  (Path\_B  app((f)p;  q)  app((g)p;  q))\}.
    (cubical-fun-ext(X;e)  \mmember{}  \{X  \mvdash{}  \_:(Path\_\mPi{}A  B  f  g)\})


By

---

Latex:
(RepeatFor  5  (Intro)
  THEN  (InstLemma  `cubical-pi-p`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  (f)p  \mmember{}  \{X.A  \mvdash{}  \_:\mPi{}(A)p  (B)(p  o  p;q)\}  BY
                          ((Assert  (f)p  \mmember{}  \{X.A  \mvdash{}  \_:(\mPi{}A  B)p\}  BY
                                          Auto)
                            THEN  InferEqualType
                            THEN  Try  (Trivial)
                            THEN  EqCDA
                            THEN  Auto))
  THEN  (Assert  (g)p  \mmember{}  \{X.A  \mvdash{}  \_:\mPi{}(A)p  (B)(p  o  p;q)\}  BY
                          ((Assert  (g)p  \mmember{}  \{X.A  \mvdash{}  \_:(\mPi{}A  B)p\}  BY
                                          Auto)
                            THEN  InferEqualType
                            THEN  Try  (Trivial)
                            THEN  EqCDA
                            THEN  Auto))
  THEN  (Assert  app((f)p;  q)  \mmember{}  \{X.A  \mvdash{}  \_:(B)(p;q)\}  BY
                          (InferEqualType
                            THENL  [(EqCDA
                                            THEN  (Subst'  ((B)(p  o  p;q))[q]  \msim{}  (B)(p;q)  0  THENA  (CsmUnfolding  THEN  Auto))
                                            THEN  Auto)
                                        ;  Auto]
                          ))
  THEN  (Assert  app((g)p;  q)  \mmember{}  \{X.A  \mvdash{}  \_:(B)(p;q)\}  BY
                          (InferEqualType
                            THENL  [(EqCDA
                                            THEN  (Subst'  ((B)(p  o  p;q))[q]  \msim{}  (B)(p;q)  0  THENA  (CsmUnfolding  THEN  Auto))
                                            THEN  Auto)
                                        ;  Auto]
                          ))
  THEN  Intro
  THEN  (InstLemmaIJ  `csm-cubical-pi`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}X.\mBbbI{}.(A)p\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}p  o  p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  (f)p  o  p  \mmember{}  \{X.\mBbbI{}.(A)p  \mvdash{}  \_:\mPi{}(A)p  o  p  (B)(p  o  p  o  p;q)\}  BY
                          ((InstLemmaIJ  `csm-ap-term\_wf`  [\mkleeneopen{}X.\mBbbI{}.(A)p\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}\mPi{}A  B\mkleeneclose{};\mkleeneopen{}p  o  p\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  InferEqualType
                            THEN  Try  (Trivial)
                            THEN  EqCDA
                            THEN  Auto))
  THEN  (Assert  (g)p  o  p  \mmember{}  \{X.\mBbbI{}.(A)p  \mvdash{}  \_:\mPi{}(A)p  o  p  (B)(p  o  p  o  p;q)\}  BY
                          ((InstLemmaIJ  `csm-ap-term\_wf`  [\mkleeneopen{}X.\mBbbI{}.(A)p\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}\mPi{}A  B\mkleeneclose{};\mkleeneopen{}p  o  p\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  InferEqualType
                            THEN  Try  (Trivial)
                            THEN  EqCDA
                            THEN  Auto)))

---

Home Index