lectures.alex.balgavy.eu

Lecture notes from university.
git clone git://git.alex.balgavy.eu/lectures.alex.balgavy.eu.git
Log | Files | Refs | Submodules

Pair.md (290B)

      1 +++
      2 title = "Pair"
      3 +++
      4 
      5 # Pair
      6 we try to find a method to combine two terms in a pair, in such a way that a component can be extracted from the pair.
      7 
      8 **definition of pair:**
      9 π := λlrz.z l r
     10 
     11 then:
     12 π P Q =β λz.z P Q
     13 
     14 **projection:**
     15 - π₁ := λu.u (λlr.l)
     16 - π₂ := λu.u (λlr.r)