Przemek-K0/Nat.prmk

(set natArityFn (lambda (b Bool) ((Bool-ind Unit Empty) b)))
;; Typ Bólowski bo są dwa konstuktory - Zero i Następnik (aksjomatyke Peano).
;; Typ Jednostkowy i Pusty bo Zero nie przyjmuje argumentów a następnik przyjmuje jeden


(set Nat (W natArityFn)) ; typ liczb naturalnych
(set zero (WSup Nat false (lambda (e Empty) ((Empty-ind Nat) e)))) ; Typ pusty bo zero nie przyjmuje argumentów
(set succ (lambda (n Nat) (WSup Nat true (lambda (u Unit) n)))) ; Typ jednostkowy bo następnik ma jeden argument
(set double 
     (W-rec
      (lambda (n Nat) Nat)
      (lambda (a Bool)
        ((Bool-rec
          (lambda (bl Bool)
            (Pi
             (f (Pi (ba (natArityFn bl)) Nat))
             (Pi
              (g (Pi (ba (natArityFn bl)) Nat))
              Nat)))
          (lambda (unitToNat0 (Pi (u Unit) Nat))
            (lambda (unitToNat1 (Pi (u Unit) Nat))
              (succ (succ (unitToNat1 tt)))))
          (lambda (eToNat0 (Pi (e Empty) Nat))
            (lambda (eToNat2 (Pi (e Empty) Nat))
              zero)))
         a))))

(set zero-xD (double zero))
(set one (succ zero))
(set two (succ one))
(set four (double two))
(set four-xD (succ (succ two)))

(set four-eq-four (Id four four-xD) (refl four)) ; dowód że 4 = 4
(set four-eq-four-xD (Id four four-xD) (refl four-xD))

double