Step
*
of Lemma
presheaf-fun-eta
No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A,B:{X ⊢ _}]. ∀[w:{X ⊢ _:(A ⟶ B)}].
  (presheaf-lam(X;app((w)p; q)) = w ∈ {X ⊢ _:(A ⟶ B)})
BY
{ (Intros THEN Unfold `presheaf-lam` 0 THEN Assert ⌜{X ⊢ _:(A ⟶ B)} = {X ⊢ _:ΠA (B)p} ∈ 𝕌{[i | j']}⌝⋅) }
1
.....assertion..... 
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X ⊢ _}
5. w : {X ⊢ _:(A ⟶ B)}
⊢ {X ⊢ _:(A ⟶ B)} = {X ⊢ _:ΠA (B)p} ∈ 𝕌{[i | j']}
2
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X ⊢ _}
5. w : {X ⊢ _:(A ⟶ B)}
6. {X ⊢ _:(A ⟶ B)} = {X ⊢ _:ΠA (B)p} ∈ 𝕌{[i | j']}
⊢ (λapp((w)p; q)) = w ∈ {X ⊢ _:(A ⟶ B)}
Latex:
Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[A,B:\{X  \mvdash{}  \_\}].  \mforall{}[w:\{X  \mvdash{}  \_:(A  {}\mrightarrow{}  B)\}].
    (presheaf-lam(X;app((w)p;  q))  =  w)
By
Latex:
(Intros  THEN  Unfold  `presheaf-lam`  0  THEN  Assert  \mkleeneopen{}\{X  \mvdash{}  \_:(A  {}\mrightarrow{}  B)\}  =  \{X  \mvdash{}  \_:\mPi{}A  (B)p\}\mkleeneclose{}\mcdot{})
Home
Index