proposition: Theorem paradox : forall F:U1, F.
proof: Proof. intros F. Generic.paradox h. + exact U1. + exact (fun X => X). + cbn. exact (fun u F => forall x:u, F x). + cbn. exact (fun _ _ x => x). + cbn. exact (fun _ _ x => x). + cbn. exact (fun F => u22u1 (forall x, F x)). + cbn. exact (fun _ x => u22u1_unit _ x). + cbn. exact (fun _ x => u22u1_counit _ x). + exact U0. + cbn. exact (fun X => u02u1 X). + cbn. exact (fun u F => u12u0 (forall x:(u02u1 u), u02u1 (F x))). + cbn. exact (fun u F => u12u0 (forall x:u, u02u1 (F x))). + cbn. exact (u12u0 F). + cbn in h. exact (u12u0_counit _ h). + cbn. easy. + cbn. intros **. now rewrite u22u1_coherent. + cbn. intros * x. exact (u12u0_unit _ x). + cbn. intros * x. exact (u12u0_counit _ x). + cbn. intros * x. exact (u12u0_unit _ x). + cbn. intros * x. exact (u12u0_counit _ x). Qed.