----------------------------------------------------------------------
-- This Agda code is designed to accompany the paper "Axioms for
-- Modelling Cubical Type Theory in a Topos". It is currently a work
-- in progress and still includes postulates/holes in certain places.
-- It also needs some tidying up and possibily reorganisation.
--
-- The idea for getting an impredicative universe of propositions Ω
-- comes from Martin Escardo, more details can be found at:
--
--          http://www.cs.bham.ac.uk/~mhe/impredicativity/          
----------------------------------------------------------------------

module impredicative.logic where

open import prelude
open import impredicative.prop public

infix  1 exists all exists!
infixr 3 _⊃_ _or_ _&_
infix  4 _≈_ 

----------------------------------------------------------------------
-- Function extensionality using primTrustMe
----------------------------------------------------------------------
open import Agda.Builtin.TrustMe

funext :
   {  ℓ' : Level}
   {A : Set }
   {B : A  Set ℓ'}
   {f g : (x : A)  B x}
    ----------------------------
   ((x : A)  f x  g x)  f  g
funext _ = primTrustMe

----------------------------------------------------------------------
-- Proposition extensionality using primTrustMe
----------------------------------------------------------------------
propext :
  {P Q : Ω}
   ---------------------------------------
  (prf P  prf Q)  (prf Q  prf P)  P  Q
propext _ _ = primTrustMe

----------------------------------------------------------------------
-- Comprehension
----------------------------------------------------------------------
set : (A : Set)(P : A  Ω)  Set
set A P = Σ x  A , prf (P x)

inc : {A : Set}(P : A  Ω)  set A P  A
inc _ = fst 

syntax set A  x  P) = ⟦ x ∈ A ∣ P ⟧

incMono :
   {A : Set}
   (P : A  Ω)
    -----------------------------------------
   (a b : set A P)  inc P a  inc P b  a  b
incMono P (x , u) (.x , v) refl = cong (_,_ x) (equ (P x) u v)

----------------------------------------------------------------------
-- Equality 
----------------------------------------------------------------------
_≈_ : {A : Set}  A  A  Ω 
prf (x  y) = x  y
equ (_  _) = uip 

----------------------------------------------------------------------
-- Universal quantifier
----------------------------------------------------------------------
all : (A : Set)  (A  Ω)  Ω
prf (all A P)     = (x : A)  prf (P x)
equ (all A P) f g = funext  x  equ (P x) (f x) (g x))

syntax all A  x  P) = All x ∈ A , P

----------------------------------------------------------------------
-- Implication
----------------------------------------------------------------------
_⊃_ : Ω  Ω  Ω
P  Q = All _  prf P , Q

----------------------------------------------------------------------
-- Truth
----------------------------------------------------------------------
 : Ω
prf  = Unit
equ  tt tt = refl

----------------------------------------------------------------------
-- Conjunction
----------------------------------------------------------------------
_&_ : Ω  Ω  Ω
prf (P & Q)                     = prf P × prf Q
equ (P & Q) (u₁ , u₂) (v₁ , v₂) =
  Σext (equ P u₁ v₁)
  (equ Q (subst  _  prf Q) (equ P u₁ v₁) u₂) v₂)

----------------------------------------------------------------------
-- Falsity
----------------------------------------------------------------------
 : Ω
prf   = 
equ  () _

----------------------------------------------------------------------
-- Negation
----------------------------------------------------------------------
¬ : Ω  Ω
¬ P = P  

----------------------------------------------------------------------
-- Propositional truncation
----------------------------------------------------------------------
∥_∥ : Set  Ω
prf  A      = (P : Ω)  (A  prf P)  prf P
equ  A  f g = funext  P  funext  h  equ P (f P h) (g P h)))

∣_∣ : {A : Set}  A  prf  A 
 x  _ f = f x

∥∥-rec :
  {A : Set}
  (P : Ω)
  (f : A  prf P)
   ---------------
  prf  A   prf P
∥∥-rec P f u = u P f

----------------------------------------------------------------------
-- Disjunction
----------------------------------------------------------------------
_or_ : Ω  Ω  Ω
P or Q =   prf P  prf Q 

----------------------------------------------------------------------
-- Existential quantifier
----------------------------------------------------------------------
exists : (A : Set)  (A  Ω)  Ω
exists A P =  Σ x  A , prf (P x) 

syntax exists A  x  P) = ∃ x ∈ A , P

----------------------------------------------------------------------
-- More general form of ∥∥-rec
----------------------------------------------------------------------
∥∥-elim :
  {A B : Set}
  (f : A  B)
  (e : (x x' : A)  f x  f x')
   ---------------------------
  prf  A   B

∥∥-elim {A} {B} f e u = fst (u Pf q) where
  Imf : Set
  Imf =  y  B   x  A , f x  y 

  q : A  Imf
  fst (q x)     = f x
  snd (q x) _ g = g (x , refl)

  lem1 :
    (y y' : B)
     ---------------------------------------------------
    (Σ x  A , f x  y)  (Σ x'  A , f x'  y')  y  y'
  lem1 y y' (x , u) (x' , u' ) =
    proof:
      y
        ≡[ symm u ]≡
      f x
        ≡[ e x x' ]≡
      f x'
        ≡[ u' ]≡
      y'
    qed
    
  lem2 :
    (y y' : B)
     -----------------------------------------------------------
    prf ( x  A , f x  y)  prf ( x'  A , f x'  y')  y  y'
  lem2 y y' =
    ∥∥-rec (exists A  x'  f x'  y')  y  y') λ z  
    ∥∥-rec (y  y') λ z'  lem1 y y' z z'
  
  Pf : Ω
  prf Pf                   = Imf
  equ Pf (y , v) (y' , v') = Σext (lem2 y y' v v')
                            (eq (exists A  x'  f x'  y')))

----------------------------------------------------------------------
-- or-elim
----------------------------------------------------------------------
or-elim-eq :
  {A B C : Set}
  (f : prf  A  B   C)
  (c : C)
  (p : {l : A}  f  inl l   c)
  (q : {r : B}  f  inr r   c)
   ---------------------------
  (u : prf  A  B )  f u  c

or-elim-eq {A} {B} {C} f c p q u = ∥∥-elim cases uip' u where
  cases : A  B  f u  c
  cases (inl l) = subst  u  f u  c) (equ  A  B   inl l  u) p
  cases (inr r) = subst  u  f u  c) (equ  A  B   inr r  u) q
  uip' : (x x' : A  B)  cases x  cases x'
  uip' x x' = uip (cases x) (cases x')

----------------------------------------------------------------------
-- Unique existence
----------------------------------------------------------------------
exists! : (A : Set)  (A  Ω)  Ω
exists! A P =  x  A , P x & (All x'  A , P x'  x  x')

syntax exists! A  x  P) = ∃! x ∈ A , P

----------------------------------------------------------------------
-- Axiom of description
----------------------------------------------------------------------
axd :
  {A : Set}
  (P : A  Ω)
   ----------------------------------------
  prf (∃! x  A , P x)  Σ x  A , prf (P x)

axd {A} P u = ∥∥-elim f e u where

  B : Set
  B = Σ x  A , prf (P x) × ((x' : A)  prf (P x')  x  x')
  
  f : B  (Σ x  A , prf (P x))
  f (x , u , _) = (x , u)

  e : (y y' : B)  f y  f y'
  e (_ , _ , g) (x' , u' , _) = Σext (g x' u') (eq (P x'))