Check nat.
Check Set.
Check True.
Check Prop.
Check Type.


(* Kodowanie impredykatywne *)
Definition NATP := forall C:Prop, C -> (C -> C) -> C.
Check NATP.

Definition ZEROP : NATP := 
  fun C z s => z.
Definition JEDENP : NATP :=
  fun C z s => s z.
Definition SUCCP : NATP -> NATP := 
  fun n => fun C z s => s (n C z s).

Definition PLUSP := 
  fun n m : NATP => n NATP m SUCCP.

Eval compute in (PLUSP (SUCCP (SUCCP ZEROP)) (SUCCP ZEROP)). 


Definition NATT := forall C:Type, C -> (C -> C) -> C.
Check NATT.

Definition ZEROT : NATT := 
  fun C z s => z.
Definition JEDENT : NATT :=
  fun C z s => s z.
Definition SUCCT : NATT -> NATT := 
  fun n => fun C z s => s (n C z s).

Definition PLUST := 
  fun n m : NATT => n NATT m SUCCT.

Eval compute in (PLUST (SUCCT (SUCCT ZEROT)) (SUCCT ZEROT)). 


Definition NATS := forall C:Set, C -> (C -> C) -> C.

Definition ZEROS : NATS := 
  fun C z s => z.
Definition JEDENS : NATS :=
  fun C z s => s z.
Definition SUCCS : NATS -> NATS := 
  fun n C z s => s (n C z s).

Definition PLUSS := 
  fun n m : NATS => n NATS m SUCCS.

Eval compute in (PLUSS (SUCCS (SUCCS ZEROS)) (SUCCS ZEROS)). 


(* Definition PLUST' := fun n m : NATT => fun C z s => n C (m C z s) s. *)



(* Kumulatywnosc *)

Definition P2S (X:Set) := X.

Check True.
Check P2S.
Check (P2S True).

Definition P2T(X:Type) := X.
Check P2T.
Check (P2T True).
Check nat.
Check (P2T nat).