{-# OPTIONS --cubical --safe #-}
module Test2 where

open import Agda.Primitive
open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Cubical.Sub
open import Agda.Builtin.Cubical.HCompU
open import Agda.Builtin.Sigma

≡refl : ∀ {α} {A : Set α} {a : A} → a ≡ a
≡refl {a = a} = λ _ → a

≡sym : ∀ {α} {A : Set α} {a b : A} → a ≡ b → b ≡ a
≡sym p = λ i → p (primINeg i)

≡subst : ∀ {α β} {A : Set α} (B : A → Set β) {a b : A} → a ≡ b → B a → B b
≡subst B p h = primTransp (λ i → B (p i)) i0 h

record _≃_ {α β} (A : Set α) (B : Set β) : Set (α ⊔ β) where
  field
    ≃comp : A → B
    ≃inv : B → A
    ≃comp-inv : (b : B) → ≃comp (≃inv b) ≡ b
open _≃_
{-# BUILTIN EQUIV _≃_ #-}
{-# BUILTIN EQUIVFUN ≃comp #-}

equiv-proof : ∀ {α β} (A : Set α) (B : Set β) (f : A ≃ B) (b : B) (i : I) → Partial i (Σ A (λ a → ≃comp f a ≡ b)) → Σ A (λ a → ≃comp f a ≡ b)
equiv-proof A B f b i p = ≃inv f b , ≃comp-inv f b
{-# BUILTIN EQUIVPROOF equiv-proof #-}

primitive
  primGlue : _
  prim^glue : _
  prim^unglue : _

≃refl : ∀ {α} {A : Set α} → A ≃ A
≃comp ≃refl = λ a → a
≃inv ≃refl = λ a → a
≃comp-inv ≃refl = λ a → ≡refl

ua : ∀ {α} {A B : Set α} → A ≃ B → A ≡ B
ua {_} {A} {B} f = λ i → primGlue B (λ { (i = i0) → A ; (i = i1) → B }) λ { (i = i0) → f ; (i = i1) → ≃refl }

data ⊥ : Set where

record ⊤ : Set where
  constructor tt

data Bool : Set where
  true false : Bool

-- The function for this equivalence is surjective but not injective
-- In particular, the inverse function is a right inverse but no left inverse is definable
Bool≃⊤ : Bool ≃ ⊤
≃comp Bool≃⊤ = λ _ → tt
≃inv Bool≃⊤ = λ _ → true
≃comp-inv Bool≃⊤ = λ _ → ≡refl

Bool≡⊤ : Bool ≡ ⊤
Bool≡⊤ = ua Bool≃⊤

⊤-compact : (a b : ⊤) → a ≡ b
⊤-compact _ _ = ≡refl

Bool-reify : Bool → Set
Bool-reify true = ⊤
Bool-reify false = ⊥

true≢false : true ≡ false → ⊥
true≢false p = ≡subst Bool-reify p tt

true≡false : true ≡ false
true≡false = ≡subst (λ A → (a b : A) → a ≡ b) (≡sym Bool≡⊤) ⊤-compact true false

-- Normal form is `tt`: Subject reduction is broken
oops : ⊥
oops = true≢false true≡false