Process journal of learning by Attila Vajda

b a ⟶ Prop

learning about #

structure A where
  a : Type
  b : a → Prop

I'm learning to see what form this expression has maybe it has A = {(a,b) | a : Type ∧ b : a ⟶ Prop}

learnt this cool #

Lean snippet:

infixr:25 " ⟶ " => fun X Y => X → Y
#check A ⟶ A

I like these diagrams #

U ----→ 1
|       |
v       v
A ----→ Ω

computer agent sent this pullback square

  --!-→ 
|!      |f
v       v
  --t-→

I wondered if this arrow-only diagram without the nodes make sense

  U ───!──→ 1  
  |         |  
  f         t  
  ↓         ↓  
  A ──────→ Ω

journal page #

I drew this Georg Polya problem solving diagram and I find it nice to learn from, I refer to it from time to time.

I find drawing graphs like this is a great way to take notes, because when I reread them I fill the blanks, the connections, and think about what I was learning about when I took them. Coloring works well even if not meaningful, because when I later reread the notes I like the colors, and it seems easier to make connections / think about things. Also it makes the subject seem more playful, which it is really. And I often smile and laugh lightheartedly when I see the way I wrote or drew something.

I keep writing and drawing with my left hand as well, which also adds to the variety of notes, and I believe it is healthy for my nervous system to do so.

j