Module Singl.

Inductive cos (A:Type) : Type := nico : A -> cos A.

Print cos.

Check cos.

Check (cos True).

Check (cos nat).

Check (cos Prop).

Check (cos Set).

Check (cos Type).

End Singl.


Module Normalna.

Inductive cos (A:Type) : Type := 
| nic : A -> cos A 
| cosik : A -> cos A.

Print cos.

Check cos.

Check (cos True).

Check (cos nat).

Check (cos Prop).

Check (cos Set).

Check (cos Type).

End Normalna.


Module Duza.

Inductive cos (A:Type) : Type := 
| nic : forall B: Prop, B -> A -> cos A 
| cosik : A -> cos A.

Print cos.

Check cos.

Check (cos True).

Check (cos nat).

Check (cos Prop).

Check (cos Set).

Check (cos Type).

End Duza.


Module SingBig.

Inductive cos (A:Type) : Type := 
| nic : forall B: Prop, B -> A -> cos A.

Print cos.

Check cos.

Check (cos True).

End SingBig.

Module SingBigProp.

Inductive cos (A:Type) : Prop := 
| nic : forall B: Prop, B -> A -> cos A.

Print cos.

Check cos.

Check (cos True).

End SingBigProp.


(* Obnizanie nie dziala dla normalnych definicji *)

Definition cos2 (A:Type) := A.

Print cos2.

Check cos2.

Check (cos2 True).















Inductive llist (B:Type) : Type :=
| lnil : llist B
| lcons : forall A:Set, A -> llist B -> llist B.






Inductive flist (A :Type) (B:Type) : Type :=
| fnil : flist A B
| fcons : A -> B -> flist (A->A) B -> flist A B.

Print flist.

Check Type.

Check Set.

Check (flist nat nat).

Definition z:=flist nat.
Check z.
Check (z nat).

Definition t:=fun s => flist nat s.
Check t.
Check (t nat).


Definition t1:=Type.
Definition t2:t1:=Type.

Print t2.
Print t1.
Print Universes.


Definition id (x:t2) := x.

(*Check    id t1  . *)

Definition t3:=Type.
Definition t4:t3:=Type.

Definition w := t4 -> t2 : t1.

Print t3.
Print t4.

Print Universes.

Definition v := t2 -> t2 : t3.

Print Universes. 

(* t1= t3 *)

Check (eq (A:=Type) t2 t3).

Check t3=t2.


Check (let w:=flist nat in w).
Eval compute in let t:=flist nat in t nat.
Check (flist nat nat).

Inductive dflist (B:Set) (A :Set) : Set :=
| dfnil : dflist B A
| dfcons : A -> B -> dflist (A->A) B -> dflist B A.