λ : j

module jagajaga where

ι : ∀ {J : Set} → J → J
ι x = x

me : Person
  name      ≔ Arseniy Seroka
  email     ≔ a@jagajaga
  born      ≔ 29.04.1993 · Saint Petersburg
  lives     ≔ Paris
  serokell  ≔ founded
  blooper   ≔ building
  studied   ≔ Mathematics ∧ CS  @  ITMO  ↦  docent ⊢ FP
  cinema    ≔ reel ∷ cinema
  directing ≔ lenfilm  ↦  imdb
  music     ∞ scrobbles
  hobbies   ≔ { tennis , extreme enduro , ski
              , photography , literature }
  pgp       ≔ 0xBB88A32CB051FD00
  elsewhere ≔ ⟨ github · linkedin · instagram ⟩

я  :  ι me ≡ me
я  =  β me  ∎