--#include "realisability_full_abs.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)(elb::B)
  :: 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)))))
  = let G (x::A) :: Set
          = Cr (exists@_ B (\(y::B) -> Q x y))
    in  let f (x::A)(w::G x) :: Sigma B (\(y::B) -> Cr (Q x y))
              = case w of {
                  (inl x') ->
                    struct {
                      _1 = elb;
                      _2 = element (Q x elb);};
                  (inr y) ->
                    struct {
                      _1 = y._1;
                      _2 = y._2;};}
        in  let k (r::Cr
                        (forall@_ A (\(x::A) -> exists@_ B (\(y::B) -> Q x y))))
                  :: Sigma
                       (A -> B)
                       (\(h'::(h'::A) -> B) ->
                        Cr (forall@_ A (\(x::A) -> Q x (h' x))))
                  = struct {
                      _1 = \(x::A) -> (f x (r x))._1;
                      _2 = \(x::A) -> (f x (r x))._2;}
            in  struct {
                  real =
                    \(r::Cr
                           (forall@_
                              A
                              (\(x::A) -> exists@_ B (\(y::B) -> Q x y)))) ->
                    inr@_ (k r);
                  pf =
                    let lemma (t::A)(r'::Cr (exists@_ B (\(y::B) -> Q t y)))
                          :: MR (exists@_ B (\(y::B) -> Q t y)) r' ->
                             MR (Q t (f t r')._1) (f t r')._2
                          = case r' of {
                              (inl x) ->
                                \(h::MR
                                       (exists@_ B (\(y::B) -> Q t y))
                                       (inl@_ x)) ->
                                elempty
                                  (MR
                                     (Q t (f t (inl@_ x))._1)
                                     (f t (inl@_ x))._2)
                                  h;
                              (inr y) ->
                                \(h::MR
                                       (exists@_ B (\(y'::B) -> Q t y'))
                                       (inr@_ y)) ->
                                h;}
                    in  let thething (r::Cr
                                           (forall@_
                                              A
                                              (\(x::A) ->
                                               exists@_ B (\(y::B) -> Q x y))))
                                     (p::MR
                                           (forall@_
                                              A
                                              (\(x::A) ->
                                               exists@_ B (\(y::B) -> Q x y)))
                                           r)
                              :: MR
                                   (exists@_
                                      ((h::A) -> B)
                                      (\(h::A -> B) ->
                                       forall@_ A (\(x::A) -> Q x (h x))))
                                   (real r)
                              = \(t::A) ->
                                let mutual r'
                                             :: Cr
                                                  (exists@_ B (\(y::B) -> Q t y))
                                             = r t
                                           p'
                                             :: MR
                                                  (exists@_ B (\(y::B) -> Q t y))
                                                  r'
                                             = p t
                                in  lemma t r' p'
                        in  struct {
                              _1 = thething;
                              _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 off
 #-}