---

Step * 1 1 of Lemma csm-glue-comp-agrees


1. H : CubicalSet{j}
2. G : CubicalSet{j}
3. tau : H j⟶ G
4. A : {G ⊢ _}
5. cA : G +⊢ Compositon(A)
6. psi : {G ⊢ _:𝔽}
7. T : {G, psi ⊢ _}
8. cT : G, psi +⊢ Compositon(T)
9. f : {G, psi ⊢ _:Equiv(T;A)}
10. H ⊢ (1(𝔽) ⇒ (psi)tau)
11. (cT)tau ∈ H, (psi)tau +⊢ Compositon((T)tau)
12. (f)tau ∈ {H, (psi)tau ⊢ _:(Equiv(T;A))tau}
⊢ (f)tau ∈ {H, (psi)tau ⊢ _:Equiv((T)tau;(A)tau)}
BY
{ (InferEqualTypeGen THEN Try (Trivial) THEN EqCDA) }

1
1. H : CubicalSet{j}
2. G : CubicalSet{j}
3. tau : H j⟶ G
4. A : {G ⊢ _}
5. cA : G +⊢ Compositon(A)
6. psi : {G ⊢ _:𝔽}
7. T : {G, psi ⊢ _}
8. cT : G, psi +⊢ Compositon(T)
9. f : {G, psi ⊢ _:Equiv(T;A)}
10. H ⊢ (1(𝔽) ⇒ (psi)tau)
11. (cT)tau ∈ H, (psi)tau +⊢ Compositon((T)tau)
12. (f)tau ∈ {H, (psi)tau ⊢ _:(Equiv(T;A))tau}
⊢ (Equiv(T;A))tau = Equiv((T)tau;(A)tau) ∈ {H, (psi)tau ⊢ _}

---

Latex:

---

Latex:

1.  H  :  CubicalSet\{j\}
2.  G  :  CubicalSet\{j\}
3.  tau  :  H  j{}\mrightarrow{}  G
4.  A  :  \{G  \mvdash{}  \_\}
5.  cA  :  G  +\mvdash{}  Compositon(A)
6.  psi  :  \{G  \mvdash{}  \_:\mBbbF{}\}
7.  T  :  \{G,  psi  \mvdash{}  \_\}
8.  cT  :  G,  psi  +\mvdash{}  Compositon(T)
9.  f  :  \{G,  psi  \mvdash{}  \_:Equiv(T;A)\}
10.  H  \mvdash{}  (1(\mBbbF{})  {}\mRightarrow{}  (psi)tau)
11.  (cT)tau  \mmember{}  H,  (psi)tau  +\mvdash{}  Compositon((T)tau)
12.  (f)tau  \mmember{}  \{H,  (psi)tau  \mvdash{}  \_:(Equiv(T;A))tau\}
\mvdash{}  (f)tau  \mmember{}  \{H,  (psi)tau  \mvdash{}  \_:Equiv((T)tau;(A)tau)\}


By

---

Latex:
(InferEqualTypeGen  THEN  Try  (Trivial)  THEN  EqCDA)

---

Home Index