---

Step * of Lemma fst-transprt-const-sigma

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[cA:X +⊢ Compositon(A)]. ∀[cB:X.A +⊢ Compositon(B)]. ∀[pr:{X ⊢ _:Σ A B}].
  (transprt-const(X;sigma_comp(cA;cB);pr).1 = transprt-const(X;cA;pr.1) ∈ {X ⊢ _:A})
BY
{ (Intros
   THEN Unfold `transprt-const` 0
   THEN (Assert ⌜pr ∈ {X ⊢ _:(Σ (A)p (B)p+)[0(𝕀)]}⌝⋅
   THENM ((InstLemmaIJ `fst-transprt-sigma`  [⌜X⌝;⌜(A)p⌝;⌜(B)p+⌝;⌜(cA)p⌝;⌜(cB)p+⌝;⌜pr⌝]⋅ THENA Auto)
          THEN (RWW  "csm-sigma_comp" 0 THENA Auto)
          )
   )
   THEN InferEqualType
   THEN Try (Trivial)
   THEN EqCDA
   THEN Auto) }

1
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. cA : X +⊢ Compositon(A)
5. cB : X.A +⊢ Compositon(B)
6. pr : {X ⊢ _:Σ A B}
⊢ Σ A B = (Σ (A)p (B)p+)[0(𝕀)] ∈ {X ⊢ _}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[B:\{X.A  \mvdash{}  \_\}].  \mforall{}[cA:X  +\mvdash{}  Compositon(A)].  \mforall{}[cB:X.A  +\mvdash{}  Compositon(B)].
\mforall{}[pr:\{X  \mvdash{}  \_:\mSigma{}  A  B\}].
    (transprt-const(X;sigma\_comp(cA;cB);pr).1  =  transprt-const(X;cA;pr.1))


By

---

Latex:
(Intros
  THEN  Unfold  `transprt-const`  0
  THEN  (Assert  \mkleeneopen{}pr  \mmember{}  \{X  \mvdash{}  \_:(\mSigma{}  (A)p  (B)p+)[0(\mBbbI{})]\}\mkleeneclose{}\mcdot{}
  THENM  ((InstLemmaIJ  `fst-transprt-sigma`    [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}(A)p\mkleeneclose{};\mkleeneopen{}(B)p+\mkleeneclose{};\mkleeneopen{}(cA)p\mkleeneclose{};\mkleeneopen{}(cB)p+\mkleeneclose{};\mkleeneopen{}pr\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (RWW    "csm-sigma\_comp"  0  THENA  Auto)
                )
  )
  THEN  InferEqualType
  THEN  Try  (Trivial)
  THEN  EqCDA
  THEN  Auto)

---

Home Index