--#include "BasicTypeTheory.agda"

-- The simple propositions are defined as a recursive data type

-- where there is an atomic formula atom(P) for  

-- each (constructive) proposition P

SP :: Type
  = data absurd |
         atom (P::Set) |
         sand (a::SP) (b::SP) |
         simp (a::SP) (b::SP) |
         sor (a::SP) (b::SP) |
         forall (A::Set) (P::A -> SP) |
         exists (A::Set) (P::A -> SP)

-- translation to  ordinary proposition

Tp (S::SP) :: Set
  = case S of {
      (absurd) -> Absurd;
      (atom P) -> P;
      (sand a b) -> Cart (Tp a) (Tp b);
      (simp a b) -> Tp a -> Tp b;
      (sor a b) -> Sum (Tp a) (Tp b);
      (forall A P) -> Pi A (\(h::A) -> Tp (P h));
      (exists A P) -> Sigma A (\(h::A) -> Tp (P h));}

-- make types for realising terms

Cr (S::SP) :: Set
  = case S of {
      (absurd) -> Unit;
      (atom P) -> Unit;
      (sand a b) -> Cart (Cr a) (Cr b);
      (simp a b) -> Cr a -> Cr b;
      (sor a b) -> Sum (Cr a) (Cr b);
      (forall A P) -> Pi A (\(h::A) -> Cr (P h));
      (exists A P) -> Sum Unit (Sigma A (\(h::A) -> Cr (P h)));}

element (S::SP) :: Cr S
  = case S of {
      (absurd) -> elt@_;
      (atom P) -> elt@_;
      (sand a b) ->
        struct {
          _1 = element a;
          _2 = element b;};
      (simp a b) -> \(h::Cr a) -> element b;
      (sor a b) -> inl@_ (element a);
      (forall A P) -> \(x::A) -> element (P x);
      (exists A P) -> inl@_ elt@_;}

-- Modified realisability with truth (see implication case)

MR (S::SP)(r::Cr S) :: Set
  = case S of {
      (absurd) -> Absurd;
      (atom P) -> P;
      (sand a b) -> and (MR a r._1) (MR b r._2);
      (simp a b) ->
        and ((x::Cr a) -> MR a x -> MR b (r x)) (Tp a -> Tp b);
      (sor a b) ->
        case r of {
          (inl x) -> MR a x;
          (inr y) -> MR b y;};
      (forall A P) -> (t::A) -> MR (P t) (r t);
      (exists A P) ->
        case r of {
          (inl x) -> Absurd;
          (inr y) -> MR (P y._1) y._2;};}

-- Correctness theorem 

Correct (S::SP)(r::Cr S)(p::MR S r) :: Tp S
  = case S of {
      (absurd) -> p;
      (atom P) -> p;
      (sand a b) ->
        struct {
          _1 = Correct a r._1 p._1;
          _2 = Correct b r._2 p._2;};
      (simp a b) -> p._2;
      (sor a b) ->
        case r of {
          (inl x) -> inl@_ (Correct a x p);
          (inr y) -> inr@_ (Correct b y p);};
      (forall A P) -> \(x::A) -> Correct (P x) (r x) (p x);
      (exists A P) ->
        case r of {
          (inl x) -> elempty (Tp (exists@_ A P)) p;
          (inr y) ->
            struct {
              _1 = y._1;
              _2 = Correct (P _1) y._2 p;};};}

-- predicate for realised formulas

Realized (A::SP) :: Set
  = sig{real :: Cr A;
        pf :: MR A real;}

Correct_2 (A::SP)(pf::Realized A) :: Tp A
  = Correct A pf.real pf.pf

-- extraction theorem for AE-formulas

Extract (A::Set)
        (B::Set)
        (P::A -> B -> SP)
        (pfe::Realized (forall@_ A (\(x::A) -> exists@_ B (\(y::B) -> P x y))))
  :: Pi A (\(x::A) -> Sigma B (\(y::B) -> Tp (P x y)))
  = \(x::A) ->
    Correct_2
      (exists@_ B (\(y::B) -> P x y))
      (struct {
         real = pfe.real x;
         pf = pfe.pf x;})

-- Validity of rules for first order logic 
-- system essentially the one often used in categorical logic

-- Note: weak elimination rule

true_impl_realised (A::Set)(B::Set)(p::A -> B)
  :: Realized (simp@_ (atom@_ A) (atom@_ B))
  = struct {
      real = \(h::Cr (atom@_ A)) -> h;
      pf =
        struct {
          _1 = \(x::Cr (atom@_ A)) -> p;
          _2 = p;};}

Entails (a::SP)(b::SP) :: SP
  = simp@_ a b

truthaxiom (a::SP)(P::Set)(p::P)
  :: Realized (Entails a (atom@_ P))
  = struct {
      real = \(h::Cr a) -> elt@_;
      pf =
        struct {
          _1 = \(x::Cr a) -> \(h::MR a x) -> p;
          _2 = \(h::Tp a) -> p;};}

absurdityaxiom (a::SP) :: Realized (Entails absurd@_ a)
  = struct {
      real = \(h::Cr absurd@_) -> element a;
      pf =
        struct {
          _1 =
            \(x::Cr absurd@_) ->
            \(h::MR absurd@_ x) ->
            elempty (MR a (real x)) h;
          _2 = \(h::Tp absurd@_) -> elempty (Tp a) h;};}

idaxiom (a::SP) :: Realized (Entails a a)
  = struct {
      real = \(h::Cr a) -> h;
      pf =
        struct {
          _1 = \(x::Cr a) -> \(h::MR a x) -> h;
          _2 = \(h::Tp a) -> h;};}

cut (a::SP)
    (b::SP)
    (c::SP)
    (p1::Realized (Entails a b))
    (p2::Realized (Entails b c))
  :: Realized (Entails a c)
  = struct {
      real = \(h::Cr a) -> p2.real (p1.real h);
      pf =
        struct {
          _1 =
            \(x::Cr a) ->
            \(h::MR a x) ->
            p2.pf._1 (p1.real x) (p1.pf._1 x h);
          _2 = \(h::Tp a) -> p2.pf._2 (p1.pf._2 h);};}

And_i (a::SP)
      (b::SP)
      (c::SP)
      (p1::Realized (Entails a b))
      (p2::Realized (Entails a c))
  :: Realized (Entails a (sand@_ b c))
  = struct {
      real =
        \(h::Cr a) ->
        struct {
          _1 = p1.real h;
          _2 = p2.real h;};
      pf =
        struct {
          _1 =
            \(x::Cr a) ->
            \(h::MR a x) ->
            struct {
              _1 = p1.pf._1 x h;
              _2 = p2.pf._1 x h;};
          _2 =
            \(h::Tp a) ->
            struct {
              _1 = p1.pf._2 h;
              _2 = p2.pf._2 h;};};}

And_e1 (a::SP)(b::SP) :: Realized (Entails (sand@_ a b) a)
  = struct {
      real = \(h::Cr (sand@_ a b)) -> h._1;
      pf =
        struct {
          _1 = \(x::Cr (sand@_ a b)) -> \(h::MR (sand@_ a b) x) -> h._1;
          _2 = \(h::Tp (sand@_ a b)) -> h._1;};}

And_e2 (a::SP)(b::SP) :: Realized (Entails (sand@_ a b) b)
  = struct {
      real = \(h::Cr (sand@_ a b)) -> h._2;
      pf =
        struct {
          _1 = \(x::Cr (sand@_ a b)) -> \(h::MR (sand@_ a b) x) -> h._2;
          _2 = \(h::Tp (sand@_ a b)) -> h._2;};}

Imp_i (a::SP)
      (b::SP)
      (c::SP)
      (p::Realized (Entails (sand@_ a b) c))
  :: Realized (Entails a (simp@_ b c))
  = struct {
      real =
        \(h::Cr a) ->
        \(h'::Cr b) ->
        p.real
          (struct {
             _1 = h;
             _2 = h';});
      pf =
        struct {
          _1 =
            \(x::Cr a) ->
            \(h::MR a x) ->
            struct {
              _1 =
                \(x'::Cr b) ->
                \(h'::MR b x') ->
                p.pf._1
                  (struct {
                     _1 = x;
                     _2 = x';})
                  (struct {
                     _1 = h;
                     _2 = h';});
              _2 =
                \(h'::Tp b) ->
                p.pf._2
                  (struct {
                     _1 = Correct a x h;
                     _2 = h';});};
          _2 =
            \(h::Tp a) ->
            \(h'::Tp b) ->
            p.pf._2
              (struct {
                 _1 = h;
                 _2 = h';});};}

Or_i1 (a::SP)(b::SP) :: Realized (Entails a (sor@_ a b))
  = struct {
      real = \(h::Cr a) -> inl@_ h;
      pf =
        struct {
          _1 = \(x::Cr a) -> \(h::MR a x) -> h;
          _2 = \(h::Tp a) -> inl@_ h;};}

Or_i2 (a::SP)(b::SP) :: Realized (Entails b (sor@_ a b))
  = struct {
      real = \(h::Cr b) -> inr@_ h;
      pf =
        struct {
          _1 = \(x::Cr b) -> \(h::MR b x) -> h;
          _2 = \(h::Tp b) -> inr@_ h;};}

Or_e (a::SP)
     (b::SP)
     (c::SP)
     (p1::Realized (Entails a c))
     (p2::Realized (Entails b c))
  :: Realized (Entails (sor@_ a b) c)
  = struct {
      real =
        \(h::Cr (sor@_ a b)) ->
        case h of {
          (inl x) -> p1.real x;
          (inr y) -> p2.real y;};
      pf =
        struct {
          _1 =
            \(x::Cr (sor@_ a b)) ->
            case x of {
              (inl x') -> \(h::MR (sor@_ a b) (inl@_ x')) -> p1.pf._1 x' h;
              (inr y) -> \(h::MR (sor@_ a b) (inr@_ y)) -> p2.pf._1 y h;};
          _2 =
            \(h::Tp (sor@_ a b)) ->
            case h of {
              (inl x) -> p1.pf._2 x;
              (inr y) -> p2.pf._2 y;};};}

Imp_e (a::SP)
      (b::SP)
      (c::SP)
      (p::Realized (Entails a (simp@_ b c)))
  :: Realized (Entails (sand@_ a b) c)
  = struct {
      real = \(h::Cr (sand@_ a b)) -> p.real h._1 h._2;
      pf =
        struct {
          _1 =
            \(x::Cr (sand@_ a b)) ->
            \(h::MR (sand@_ a b) x) ->
            let p1 :: MR (simp@_ b c) (p.real x._1)
                  = p.pf._1 x._1 h._1
            in  p1._1 x._2 h._2;
          _2 =
            \(h::Tp (sand@_ a b)) ->
            let p2 :: (h'::Tp a) -> Tp (simp@_ b c)
                  = p.pf._2
            in  p2 h._1 h._2;};}

All_i (A::Set)
      (a::SP)
      (P::A -> SP)
      (p::(x::A) -> Realized (Entails a (P x)))
  :: Realized (Entails a (forall@_ A P))
  = struct {
      real = \(h::Cr a) -> \(x::A) -> (p x).real h;
      pf =
        struct {
          _1 = \(x::Cr a) -> \(h::MR a x) -> \(t::A) -> (p t).pf._1 x h;
          _2 = \(h::Tp a) -> \(x::A) -> (p x).pf._2 h;};}

All_e (A::Set)
      (a::SP)
      (P::A -> SP)
      (p::Realized (Entails a (forall@_ A P)))
      (x::A)
  :: Realized (Entails a (P x))
  = struct {
      real = \(h::Cr a) -> p.real h x;
      pf =
        let p1 :: MR (Entails a (forall@_ A P)) p.real
              = p.pf
        in  struct {
              _1 = \(x'::Cr a) -> \(h::MR a x') -> p1._1 x' h x;
              _2 = \(h::Tp a) -> p1._2 h x;};}

Ex_i (A::Set)
     (a::SP)
     (P::A -> SP)
     (p::(x::A) -> Realized (Entails (P x) a))
  :: Realized (Entails (exists@_ A P) a)
  = struct {
      real =
        \(h::Cr (exists@_ A P)) ->
        case h of {
          (inl x) -> element a;
          (inr y) -> (p y._1).real y._2;};
      pf =
        struct {
          _1 =
            \(x::Cr (exists@_ A P)) ->
            \(h::MR (exists@_ A P) x) ->
            case x of {
              (inl x') -> elempty (MR a (real (inl@_ x'))) h;
              (inr y) -> (p y._1).pf._1 y._2 h;};
          _2 = \(h::Tp (exists@_ A P)) -> (p h._1).pf._2 h._2;};}

Ex_e (A::Set)
     (a::SP)
     (P::A -> SP)
     (p::Realized (Entails (exists@_ A P) a))
     (x::A)
  :: Realized (Entails (P x) a)
  = struct {
      real =
        \(h::Cr (P x)) ->
        p.real
          (inr@_
             (struct {
                _1 = x;
                _2 = h;}));
      pf =
        struct {
          _1 =
            \(x'::Cr (P x)) ->
            \(h::MR (P x) x') ->
            p.pf._1
              (inr@_
                 (struct {
                    _1 = x;
                    _2 = x';}))
              h;
          _2 =
            \(h::Tp (P x)) ->
            p.pf._2
              (struct {
                 _1 = x;
                 _2 = h;});};}
{-# Alfa unfoldgoals off
brief on
hidetypeannots off
wide

nd
hiding off
var "gg"
con "forall"
con "cimp" infix as "=>"
con "cand" infix as "&"
con "absurd" as "^" with symbolfont
var "BinProd" infix as "´" with symbolfont
var "Sigma" as "S" with symbolfont
var "iff" infix
var "Entails" infix as "|--"
con "sand" infix as "&"
con "simp" infix as "=>"
con "sor" infix as "Ú" with symbolfont
 #-}