```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

```