open import Calf.Core.Abstract
open import Calf.Value

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure

module Calf.Value.Open where

β—― : 𝒱 β†’ 𝒱
β—― X = (abs : ⟨ ABS ⟩) β†’ X

β—―' : (⟨ ABS ⟩ β†’ 𝒱) β†’ 𝒱
β—―' X = (abs : ⟨ ABS ⟩) β†’ X abs

Ξ·β—¦ : {X : 𝒱} β†’ X β†’ β—― X
Ξ·β—¦ x _ = x

map : {X Y : 𝒱} β†’ (X β†’ Y) β†’ β—― X β†’ β—― Y
map f xβ—¦ abs = f (xβ—¦ abs)

Ξ·β—¦-isNatural : {X Y : 𝒱} (f : X β†’ Y) β†’ Ξ·β—¦ ∘ f ≑ map f ∘ Ξ·β—¦
Ξ·β—¦-isNatural f = funExt Ξ» x β†’ refl

𝒱◦ : 𝒱₁
𝒱◦ = TypeWithStr _ Ξ» X β†’ isEquiv (Ξ·β—¦ {X})

join : {X : 𝒱} β†’ β—― (β—― X) β†’ β—― X
join x abs = x abs abs

bind : {X Y : 𝒱} β†’ β—― X β†’ (X β†’ β—― Y) β†’ β—― Y
bind xβ—¦ k = join (map k xβ—¦)

Ξ·-isEquiv : {X : 𝒱} β†’ isEquiv (Ξ·β—¦ {β—― X})
Ξ·-isEquiv = isoToIsEquiv (iso Ξ·β—¦ join sec ret)
  where
    sec : {X : 𝒱} β†’ (x : β—― (β—― X)) β†’ Ξ·β—¦ (join x) ≑ x
    sec x = funExt Ξ» abs β†’ funExt Ξ» q β†’ cong (Ξ» r β†’ x r q) (str ABS q abs)

    ret : {X : 𝒱} β†’ (x : β—― X) β†’ join (Ξ·β—¦ x) ≑ x
    ret x = refl

β—―-preserves-isSet : isSet X β†’ isSet (β—― X)
◯-preserves-isSet = isSet→