---

Step * 1 of Lemma cubical-fun-ext_wf


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)}
BY
{ ((Assert app((f)p o p; q) ∈ {X.𝕀.(A)p ⊢ _:(B)(p o p;q)} BY
          (InferEqualType
           THEN Try (((Subst' ((B)(p o p o p;q))[q] ~ (B)(p o p;q) 0 THENA (CsmUnfolding THEN Auto))
                      THEN Fold `member` 0
                      THEN Auto))
           THEN Auto))
   THEN (Assert app((g)p o p; q) ∈ {X.𝕀.(A)p ⊢ _:(B)(p o p;q)} BY
               (InferEqualType
                THEN Try (((Subst' ((B)(p o p o p;q))[q] ~ (B)(p o p;q) 0 THENA (CsmUnfolding THEN Auto))
                           THEN Fold `member` 0
                           THEN Auto))
                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)}
15. app((f)p o p; q) ∈ {X.𝕀.(A)p ⊢ _:(B)(p o p;q)}
16. app((g)p o p; q) ∈ {X.𝕀.(A)p ⊢ _:(B)(p o p;q)}
⊢ cubical-fun-ext(X;e) ∈ {X ⊢ _:(Path_ΠA B f g)}

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  A  :  \{X  \mvdash{}  \_\}
3.  B  :  \{X.A  \mvdash{}  \_\}
4.  f  :  \{X  \mvdash{}  \_:\mPi{}A  B\}
5.  g  :  \{X  \mvdash{}  \_:\mPi{}A  B\}
6.  (\mPi{}A  B)p  =  X.A  \mvdash{}  \mPi{}(A)p  (B)(p  o  p;q)
7.  (f)p  \mmember{}  \{X.A  \mvdash{}  \_:\mPi{}(A)p  (B)(p  o  p;q)\}
8.  (g)p  \mmember{}  \{X.A  \mvdash{}  \_:\mPi{}(A)p  (B)(p  o  p;q)\}
9.  app((f)p;  q)  \mmember{}  \{X.A  \mvdash{}  \_:(B)(p;q)\}
10.  app((g)p;  q)  \mmember{}  \{X.A  \mvdash{}  \_:(B)(p;q)\}
11.  e  :  \{X  \mvdash{}  \_:\mPi{}A  (Path\_B  app((f)p;  q)  app((g)p;  q))\}
12.  (\mPi{}A  B)p  o  p  =  X.\mBbbI{}.(A)p  \mvdash{}  \mPi{}(A)p  o  p  (B)(p  o  p  o  p;q)
13.  (f)p  o  p  \mmember{}  \{X.\mBbbI{}.(A)p  \mvdash{}  \_:\mPi{}(A)p  o  p  (B)(p  o  p  o  p;q)\}
14.  (g)p  o  p  \mmember{}  \{X.\mBbbI{}.(A)p  \mvdash{}  \_:\mPi{}(A)p  o  p  (B)(p  o  p  o  p;q)\}
\mvdash{}  cubical-fun-ext(X;e)  \mmember{}  \{X  \mvdash{}  \_:(Path\_\mPi{}A  B  f  g)\}


By

---

Latex:
((Assert  app((f)p  o  p;  q)  \mmember{}  \{X.\mBbbI{}.(A)p  \mvdash{}  \_:(B)(p  o  p;q)\}  BY
                (InferEqualType
                  THEN  Try  (((Subst'  ((B)(p  o  p  o  p;q))[q]  \msim{}  (B)(p  o  p;q)  0  THENA  (CsmUnfolding  THEN  Auto))
                                        THEN  Fold  `member`  0
                                        THEN  Auto))
                  THEN  Auto))
  THEN  (Assert  app((g)p  o  p;  q)  \mmember{}  \{X.\mBbbI{}.(A)p  \mvdash{}  \_:(B)(p  o  p;q)\}  BY
                          (InferEqualType
                            THEN  Try  (((Subst'  ((B)(p  o  p  o  p;q))[q]  \msim{}  (B)(p  o  p;q)  0
                                                    THENA  (CsmUnfolding  THEN  Auto)
                                                    )
                                                  THEN  Fold  `member`  0
                                                  THEN  Auto))
                            THEN  Auto))
  )

---

Home Index