---

Step * 1 of Lemma presheaf-sigma-fun_wf


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)}
BY
{ ((Assert (B')(p o p;q) ∈ G.Σ A B.(A)p ⊢  BY
          ((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 (Enough to prove app(app(((λf))p; q.1); q.2) ∈ {G.Σ A B ⊢ _:((B')(p o p;q))[q.1]}
          Because 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}
12. (B')(p o p;q) ∈ G.Σ A B.(A)p ⊢ 
⊢ app(app(((λf))p; q.1); q.2) ∈ {G.Σ A B ⊢ _:((B')(p o p;q))[q.1]}

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  G  :  ps\_context\{j:l\}(C)
3.  A  :  \{G  \mvdash{}  \_\}
4.  B  :  \{G.A  \mvdash{}  \_\}
5.  B'  :  \{G.A  \mvdash{}  \_\}
6.  f  :  \{G.A  \mvdash{}  \_:(B  {}\mrightarrow{}  B')\}
7.  (\mSigma{}  A  B')p  =  \mSigma{}  (A)p  (B')(p  o  p;q)
8.  (\mSigma{}  A  B)p  =  \mSigma{}  (A)p  (B)(p  o  p;q)
9.  q  \mmember{}  \{G.\mSigma{}  A  B  \mvdash{}  \_:(\mSigma{}  A  B)p\}
10.  q  \mmember{}  \{G.\mSigma{}  A  B  \mvdash{}  \_:\mSigma{}  (A)p  (B)(p  o  p;q)\}
11.  q.1  \mmember{}  \{G.\mSigma{}  A  B  \mvdash{}  \_:(A)p\}
\mvdash{}  presheaf-pair(q.1;app(app(((\mlambda{}f))p;  q.1);  q.2))  \mmember{}  \{G.\mSigma{}  A  B  \mvdash{}  \_:\mSigma{}  (A)p  (B')(p  o  p;q)\}


By

---

Latex:
((Assert  (B')(p  o  p;q)  \mmember{}  G.\mSigma{}  A  B.(A)p  \mvdash{}    BY
                ((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  (Enough  to  prove  app(app(((\mlambda{}f))p;  q.1);  q.2)  \mmember{}  \{G.\mSigma{}  A  B  \mvdash{}  \_:((B')(p  o  p;q))[q.1]\}
                Because  Auto)
  )

---

Home Index