module Examples.Universes where

open import Data.Empty
open import Data.Unit
open import Data.Product as P
open import Function
open import Data.Bool
open import Data.Nat

open import Relation.Binary.PropositionalEquality

import posIR
import Constructions.Coproduct as Plus
import Constructions

-- A universe closed under Σ, ℕ and ⊤ in Set^op
module sigma-nat-unit where

  -- C = Set^op
  open posIR Set  A B  B -> A)  c  id)  f g  g  f)
  open Plus Set  A B  B -> A)  c  id)  f g  g  f)
  open Constructions Set  A B  B -> A)  c  id)  f g  g  f)  

  γ : IR+
  γ = ι  +IR ι  +IR δ₁  TA  δ TA  T∘B  ι (Σ TA T∘B))
                                    η  ι→ι ( id  {a}  η a))))
                          f  δ→δ f  h  ι→ι ( f id)))

-- A universe closed under Π and ℕ in Set^iso
module pi-nat (ext :  {c}{d} -> Extensionality c d) where

  HomSet^iso : Set -> Set -> Set
  HomSet^iso  A B = Σ[ f  (A -> B) ] Σ[ f⁻¹  (B -> A) ]
                                      ((x : A) -> f⁻¹ (f x)  x)

  idSet^iso : (A : Set) -> HomSet^iso A A
  idSet^iso A = id , id ,  x  refl)

  ∘Set^iso : {A B C : Set} -> HomSet^iso B C -> HomSet^iso A B -> HomSet^iso A C
  ∘Set^iso (f , f' , p) (g , g' , q) = f  g ,
                                       g'  f' ,
                                        x  trans (cong g' (p (g x))) (q x))

  -- C = Set^iso (actually f⁻¹ ∘ f = id is enough)
  open posIR Set HomSet^iso idSet^iso ∘Set^iso
  open Plus Set HomSet^iso idSet^iso ∘Set^iso
  open Constructions Set HomSet^iso idSet^iso ∘Set^iso

  γ : IR+
  γ = ι  +IR
      δ₁  TA  δ TA  T∘B  ι ((x : TA) -> (T∘B x)))
                       η  ι→ι ((λ f x  proj₁ (η x) (f x)) ,
                                   g x  proj₁ (proj₂ (η x)) (g x)) ,
                                   f  ext  x  proj₂ (proj₂ (η x)) (f x))))))
             { (f , f' , p)  
                   δ→δ f'
                        h  ι→ι ((λ g x  g (f' x)) ,
                        g x  subst h (p x) (g (f x))) ,
                        g  (ext λ x  J  x y p  subst h p (g x)  g y)  x  refl) (f' (f x)) x (p x))))) })
    where J : {A : Set}(P : (x y : A) -> x  y -> Set) ->
              ((x : A) -> P x x refl) -> (x y : A) -> (p : x  y) -> P x y p
          J P d x .x refl = d x