---

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


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}
⊢ a.2 = b.2 ∈ {X ⊢ _:((Path_(T)p (z)p app((f)p; q)))[a.1]}
BY
{ ((InstLemmaIJ `csm-path-type` [⌜X.A⌝;⌜X⌝;⌜[a.1]⌝;⌜(T)p⌝;⌜(z)p⌝;⌜app((f)p; q)⌝]⋅ THENA Auto)
   THEN (Assert ⌜a.2 = b.2 ∈ {X ⊢ _:(Path_((T)p)[a.1] ((z)p)[a.1] (app((f)p; q))[a.1])}⌝⋅
        THENM (InferEqualTypeGen THEN EqCD THEN Auto)
        )
   ) }

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

---

Latex:

---

Latex:

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
\mvdash{}  a.2  =  b.2


By

---

Latex:
((InstLemmaIJ  `csm-path-type`  [\mkleeneopen{}X.A\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}[a.1]\mkleeneclose{};\mkleeneopen{}(T)p\mkleeneclose{};\mkleeneopen{}(z)p\mkleeneclose{};\mkleeneopen{}app((f)p;  q)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}a.2  =  b.2\mkleeneclose{}\mcdot{}  THENM  (InferEqualTypeGen  THEN  EqCD  THEN  Auto))
  )

---

Home Index