---

Step * of Lemma presheaf-sigma-fun_wf

No Annotations
∀[C:SmallCategory]. ∀[G:ps_context{j:l}(C)]. ∀[A:{G ⊢ _}]. ∀[B,B':{G.A ⊢ _}]. ∀[f:{G.A ⊢ _:(B ⟶ B')}].
  (presheaf-sigma-fun(G;A;B;f) ∈ {G ⊢ _:(Σ A B ⟶ Σ A B')})
BY
{ ((Intros THEN Unhide)
   THEN (InstLemma `presheaf-sigma-p` [⌜C⌝;⌜G⌝;⌜Σ A B⌝;⌜A⌝;⌜B'⌝]⋅ THENA Auto)
   THEN (InstLemma `presheaf-sigma-p` [⌜C⌝;⌜G⌝;⌜Σ A B⌝;⌜A⌝;⌜B⌝]⋅ THENA Auto)
   THEN (Assert q ∈ {G.Σ A B ⊢ _:(Σ A B)p} BY
               Auto)
   THEN (Assert q ∈ {G.Σ A B ⊢ _:Σ (A)p (B)(p o p;q)} BY
               (InferEqualTypeUp THEN Auto))
   THEN (Assert q.1 ∈ {G.Σ A B ⊢ _:(A)p} BY
               (InstLemma `presheaf-fst_wf` [⌜parm{i}⌝;⌜parm{i|j}⌝;⌜C⌝;⌜G.Σ A B⌝;⌜(A)p⌝;⌜(B)(p o p;q)⌝;⌜q⌝]⋅
                THEN Try (Complete (Auto))
                THEN (InstLemma `pscm-ap-type_wf` [⌜parm{i}⌝;⌜parm{i|j}⌝;⌜C⌝;⌜G.A⌝;⌜G.Σ A B.(A)p⌝]⋅ THENA Auto)
                THEN BHyp -1
                THEN Auto))
   THEN Unfold `presheaf-sigma-fun` 0
   THEN (MemCD THEN Try (Trivial))
   THEN Try ((MemCD THEN Auto))
   THEN (SubsumeC ⌜{G.Σ A B ⊢ _:Σ (A)p (B')(p o p;q)}⌝⋅ THENL [Id; Auto])) }

1
1. C : SmallCategory
2. G : ps_context{j:l}(C)
3. A : {G ⊢ _}
4. B : {G.A ⊢ _}
5. B' : {G.A ⊢ _}
6. f : {G.A ⊢ _:(B ⟶ B')}
7. (Σ A B')p = Σ (A)p (B')(p o p;q) ∈ {G.Σ A B ⊢ _}
8. (Σ A B)p = Σ (A)p (B)(p o p;q) ∈ {G.Σ A B ⊢ _}
9. q ∈ {G.Σ A B ⊢ _:(Σ A B)p}
10. q ∈ {G.Σ A B ⊢ _:Σ (A)p (B)(p o p;q)}
11. q.1 ∈ {G.Σ A B ⊢ _:(A)p}
⊢ presheaf-pair(q.1;app(app(((λf))p; q.1); q.2)) ∈ {G.Σ A B ⊢ _:Σ (A)p (B')(p o p;q)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[G:ps\_context\{j:l\}(C)].  \mforall{}[A:\{G  \mvdash{}  \_\}].  \mforall{}[B,B':\{G.A  \mvdash{}  \_\}].
\mforall{}[f:\{G.A  \mvdash{}  \_:(B  {}\mrightarrow{}  B')\}].
    (presheaf-sigma-fun(G;A;B;f)  \mmember{}  \{G  \mvdash{}  \_:(\mSigma{}  A  B  {}\mrightarrow{}  \mSigma{}  A  B')\})


By

---

Latex:
((Intros  THEN  Unhide)
  THEN  (InstLemma  `presheaf-sigma-p`  [\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}\mSigma{}  A  B\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B'\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `presheaf-sigma-p`  [\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}\mSigma{}  A  B\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  q  \mmember{}  \{G.\mSigma{}  A  B  \mvdash{}  \_:(\mSigma{}  A  B)p\}  BY
                          Auto)
  THEN  (Assert  q  \mmember{}  \{G.\mSigma{}  A  B  \mvdash{}  \_:\mSigma{}  (A)p  (B)(p  o  p;q)\}  BY
                          (InferEqualTypeUp  THEN  Auto))
  THEN  (Assert  q.1  \mmember{}  \{G.\mSigma{}  A  B  \mvdash{}  \_:(A)p\}  BY
                          (InstLemma  `presheaf-fst\_wf`  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}parm\{i|j\}\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}G.\mSigma{}  A  B\mkleeneclose{};\mkleeneopen{}(A)p\mkleeneclose{};\mkleeneopen{}(B)(p  o  p;q)\mkleeneclose{}
                            ;\mkleeneopen{}q\mkleeneclose{}]\mcdot{}
                            THEN  Try  (Complete  (Auto))
                            THEN  (InstLemma  `pscm-ap-type\_wf`  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}parm\{i|j\}\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}G.A\mkleeneclose{};\mkleeneopen{}G.\mSigma{}  A  B.(A)p\mkleeneclose{}]\mcdot{}
                                        THENA  Auto
                                        )
                            THEN  BHyp  -1
                            THEN  Auto))
  THEN  Unfold  `presheaf-sigma-fun`  0
  THEN  (MemCD  THEN  Try  (Trivial))
  THEN  Try  ((MemCD  THEN  Auto))
  THEN  (SubsumeC  \mkleeneopen{}\{G.\mSigma{}  A  B  \mvdash{}  \_:\mSigma{}  (A)p  (B')(p  o  p;q)\}\mkleeneclose{}\mcdot{}  THENL  [Id;  Auto]))

---

Home Index