---

Step * 1 1 of Lemma equal-fiber-when-discrete

.....assertion..... 
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. A : {X ⊢ _}
4. f : {X ⊢ _:(A ⟶ T)}
5. z : {X ⊢ _:T}
6. a : {X ⊢ _:Fiber(f;z)}
7. b : {X ⊢ _:Fiber(f;z)}
8. ∀x:{X ⊢ _:Path(T)}. (x = refl(x @ 0(𝕀)) ∈ {X ⊢ _:Path(T)})
9. app((f)p; q) ∈ {X.A ⊢ _:(T)p}
10. a.1 = b.1 ∈ {X ⊢ _:A}
11. ((Path_(T)p (z)p app((f)p; q)))[a.1] = (X ⊢ Path_((T)p)[a.1] ((z)p)[a.1] (app((f)p; q))[a.1]) ∈ {X ⊢ _}
⊢ a.2 = b.2 ∈ {X ⊢ _:(Path_((T)p)[a.1] ((z)p)[a.1] (app((f)p; q))[a.1])}
BY
{ ((Assert a.2 ∈ {X ⊢ _:((Path_(T)p (z)p app((f)p; q)))[a.1]} BY
          (OnVar `a' (Unfold `cubical-fiber`) THEN Auto))
   THEN (Assert b.2 ∈ {X ⊢ _:((Path_(T)p (z)p app((f)p; q)))[b.1]} BY
               (OnVar `b' (Unfold `cubical-fiber`) THEN Auto))
   THEN (Assert b.2 ∈ {X ⊢ _:((Path_(T)p (z)p app((f)p; q)))[a.1]} BY
               (InferEqualTypeGen THEN Try (Trivial) THEN RepeatFor 3 (EqCDA) THEN Auto))
   THEN Thin (-2)
   THEN (Assert {X ⊢ _:((Path_(T)p (z)p app((f)p; q)))[a.1]}
               = {X ⊢ _:(Path_((T)p)[a.1] ((z)p)[a.1] (app((f)p; q))[a.1])}
               ∈ 𝕌{[i' | j']} BY
               (EqCD THEN Auto))) }

1
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. A : {X ⊢ _}
4. f : {X ⊢ _:(A ⟶ T)}
5. z : {X ⊢ _:T}
6. a : {X ⊢ _:Fiber(f;z)}
7. b : {X ⊢ _:Fiber(f;z)}
8. ∀x:{X ⊢ _:Path(T)}. (x = refl(x @ 0(𝕀)) ∈ {X ⊢ _:Path(T)})
9. app((f)p; q) ∈ {X.A ⊢ _:(T)p}
10. a.1 = b.1 ∈ {X ⊢ _:A}
11. ((Path_(T)p (z)p app((f)p; q)))[a.1] = (X ⊢ Path_((T)p)[a.1] ((z)p)[a.1] (app((f)p; q))[a.1]) ∈ {X ⊢ _}
12. a.2 ∈ {X ⊢ _:((Path_(T)p (z)p app((f)p; q)))[a.1]}
13. b.2 ∈ {X ⊢ _:((Path_(T)p (z)p app((f)p; q)))[a.1]}
14. {X ⊢ _:((Path_(T)p (z)p app((f)p; q)))[a.1]}
= {X ⊢ _:(Path_((T)p)[a.1] ((z)p)[a.1] (app((f)p; q))[a.1])}
∈ 𝕌{[i' | j']}
⊢ a.2 = b.2 ∈ {X ⊢ _:(Path_((T)p)[a.1] ((z)p)[a.1] (app((f)p; q))[a.1])}

---

Latex:

---

Latex:
.....assertion..... 
1.  X  :  CubicalSet\{j\}
2.  T  :  \{X  \mvdash{}  \_\}
3.  A  :  \{X  \mvdash{}  \_\}
4.  f  :  \{X  \mvdash{}  \_:(A  {}\mrightarrow{}  T)\}
5.  z  :  \{X  \mvdash{}  \_:T\}
6.  a  :  \{X  \mvdash{}  \_:Fiber(f;z)\}
7.  b  :  \{X  \mvdash{}  \_:Fiber(f;z)\}
8.  \mforall{}x:\{X  \mvdash{}  \_:Path(T)\}.  (x  =  refl(x  @  0(\mBbbI{})))
9.  app((f)p;  q)  \mmember{}  \{X.A  \mvdash{}  \_:(T)p\}
10.  a.1  =  b.1
11.  ((Path\_(T)p  (z)p  app((f)p;  q)))[a.1]  =  (X  \mvdash{}  Path\_((T)p)[a.1]  ((z)p)[a.1]  (app((f)p;  q))[a.1])
\mvdash{}  a.2  =  b.2


By

---

Latex:
((Assert  a.2  \mmember{}  \{X  \mvdash{}  \_:((Path\_(T)p  (z)p  app((f)p;  q)))[a.1]\}  BY
                (OnVar  `a'  (Unfold  `cubical-fiber`)  THEN  Auto))
  THEN  (Assert  b.2  \mmember{}  \{X  \mvdash{}  \_:((Path\_(T)p  (z)p  app((f)p;  q)))[b.1]\}  BY
                          (OnVar  `b'  (Unfold  `cubical-fiber`)  THEN  Auto))
  THEN  (Assert  b.2  \mmember{}  \{X  \mvdash{}  \_:((Path\_(T)p  (z)p  app((f)p;  q)))[a.1]\}  BY
                          (InferEqualTypeGen  THEN  Try  (Trivial)  THEN  RepeatFor  3  (EqCDA)  THEN  Auto))
  THEN  Thin  (-2)
  THEN  (Assert  \{X  \mvdash{}  \_:((Path\_(T)p  (z)p  app((f)p;  q)))[a.1]\}
                          =  \{X  \mvdash{}  \_:(Path\_((T)p)[a.1]  ((z)p)[a.1]  (app((f)p;  q))[a.1])\}  BY
                          (EqCD  THEN  Auto)))

---

Home Index