--#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
 #-}