posting in small fragments, frequently
reviewing a few things #
maybe, looking back, surely, I can find something cool to share as still days go by without posting, because I get immersed in learning, mathematics is really awesome! and I thought this could be something that others might not see but would be surprised, "Wow I did not see this is so!"
eg "I just learned this it surprised me!"
P Q : Prop #
P ⟵ Prop, in other words P is a term with type Prop,
is analogous to P ⟵ Hom(1,Ω),
maybe P, Q : Hom(1, Ω)?
f : P → Q
x : P
f x : Q -- just function application!P, P ⟶ Q ⊢ Q
≡
P ⊢ (P ⟶ Q) ⟶ Q
≡
⊢ P ⟶ (P ⟶ Q) ⟶ Q
ev : (P ⟶ Q) × P ⟶ Q (Evaluation morphism)
I'm learning about ⊢, ⊨, 𝕄,
This is a nice diagram: $\begin{CD}\Phi@>⊨>>𝔐@<⊨<<\Psi\end{CD}$
- Previous: f 1 ⟶ X game
- Next: tegnap