--#include "realisability.agda" atomic_imp (A::Set) (B::Set) (Q::A -> B -> SP) (P::A -> B -> Set) (tr::(x::A) -> (y::B) -> Tp (Q x y) -> P x y) :: Realized (forall@_ A (\(x::A) -> forall@_ B (\(y::B) -> simp@_ (Q x y) (atom@_ (P x y))))) = struct { real = \(x::A) -> \(x'::B) -> \(h::Cr (Q x x')) -> elt@_; pf = \(x::A) -> \(y::B) -> struct { _1 = \(x'::Cr (Q x y)) -> \(h::MR (Q x y) x') -> tr x y (Correct (Q x y) x' h); _2 = tr x y;};} negatives (A::Set) (B::Set) (Q::A -> B -> SP) (P::A -> B -> Set) (tr::(x::A) -> (y::B) -> Tp (Q x y) -> Absurd) :: Realized (forall@_ A (\(x::A) -> forall@_ B (\(y::B) -> simp@_ (Q x y) absurd@_))) = struct { real = \(x::A) -> \(x'::B) -> \(h::Cr (Q x x')) -> elt@_; pf = \(x::A) -> \(y::B) -> struct { _1 = \(x'::Cr (Q x y)) -> \(h::MR (Q x y) x') -> tr x y (Correct (Q x y) x' h); _2 = tr x y;};} presetAC (A::Set)(B::Set)(Q::A -> B -> SP) :: Realized (simp@_ (forall@_ A (\(x::A) -> exists@_ B (\(y::B) -> Q x y))) (exists@_ (A -> B) (\(h::(h::A) -> B) -> forall@_ A (\(x::A) -> Q x (h x))))) = struct { real = \(h::Cr (forall@_ A (\(x::A) -> exists@_ B (\(y::B) -> Q x y)))) -> struct { _1 = \(h'::A) -> (h h')._1; _2 = \(x::A) -> (h x)._2;}; pf = struct { _1 = \(x::Cr (forall@_ A (\(x::A) -> exists@_ B (\(y::B) -> Q x y)))) -> \(h::MR (forall@_ A (\(x'::A) -> exists@_ B (\(y::B) -> Q x' y))) x) -> h; _2 = \(h::Tp (forall@_ A (\(x::A) -> exists@_ B (\(y::B) -> Q x y)))) -> struct { _1 = \(x::A) -> (h x)._1; _2 = \(x::A) -> (h x)._2;};};} {-# Alfa unfoldgoals off brief on hidetypeannots off wide nd hiding on #-}