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))
                                   (λ η → ι→ι (P.map id (λ {a} → η a))))
                         (λ f → δ→δ f (λ h → ι→ι (P.map 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