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` THEN Assert ⌜{X ⊢ _:(A ⟶ B)} {X ⊢ _:Π(B)p} ∈ 𝕌{[i j']}⌝⋅}

1
.....assertion..... 
1. SmallCategory
2. ps_context{j:l}(C)
3. {X ⊢ _}
4. {X ⊢ _}
5. {X ⊢ _:(A ⟶ B)}
⊢ {X ⊢ _:(A ⟶ B)} {X ⊢ _:Π(B)p} ∈ 𝕌{[i j']}

2
1. SmallCategory
2. ps_context{j:l}(C)
3. {X ⊢ _}
4. {X ⊢ _}
5. {X ⊢ _:(A ⟶ B)}
6. {X ⊢ _:(A ⟶ B)} {X ⊢ _:Π(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