------------------------------------------------------------------------
-- Equivalences with erased "proofs", defined in terms of partly
-- erased contractible fibres
------------------------------------------------------------------------

-- This module contains some basic definitions with few dependencies.
-- See Equivalence.Erased.Contractible-preimages for more definitions.
-- The definitions below are reexported from
-- Equivalence.Erased.Contractible-preimages.

{-# OPTIONS --cubical-compatible --safe #-}

open import Equality

module Equivalence.Erased.Contractible-preimages.Basics
  {reflexive} (eq :  {a p}  Equality-with-J a p reflexive) where

open Derived-definitions-and-properties eq
open import Erased.Basics
open import Prelude

open import Bijection eq using (_↔_)
import Equivalence.Contractible-preimages eq as CP
open import Extensionality eq
open import H-level eq as H-level
open import H-level.Closure eq
open import Preimage eq as Preimage using (_⁻¹_)
open import Surjection eq using (_↠_; Split-surjective)

private
  variable
    a b  ℓ₁ ℓ₂      : Level
    A B              : Type a
    c ext k k′ p x y : A
    P                : A  Type p
    f                : (x : A)  P x

------------------------------------------------------------------------
-- Some basic types

-- "Preimages" with erased proofs.

infix 5 _⁻¹ᴱ_

_⁻¹ᴱ_ : {A : Type a} {@0 B : Type b}  @0 (A  B)  @0 B  Type (a  b)
f ⁻¹ᴱ y =  λ x  Erased (f x  y)

-- Contractibility with an erased proof.

Contractibleᴱ : Type   Type 
Contractibleᴱ A =  λ (x : A)  Erased (∀ y  x  y)

-- The property of being an equivalence (with erased proofs).

Is-equivalenceᴱ : {A : Type a} {B : Type b}  @0 (A  B)  Type (a  b)
Is-equivalenceᴱ f =  y  Contractibleᴱ (f ⁻¹ᴱ y)

-- Equivalences with erased proofs.

_≃ᴱ_ : Type a  Type b  Type (a  b)
A ≃ᴱ B =  λ (f : A  B)  Is-equivalenceᴱ f

------------------------------------------------------------------------
-- Some conversion lemmas

-- Conversions between _⁻¹_ and _⁻¹ᴱ_.

⁻¹→⁻¹ᴱ :
  {@0 A : Type a} {@0 B : Type b} {@0 f : A  B} {@0 y : B} 
  f ⁻¹ y  f ⁻¹ᴱ y
⁻¹→⁻¹ᴱ = Σ-map id [_]→

@0 ⁻¹ᴱ→⁻¹ : f ⁻¹ᴱ x  f ⁻¹ x
⁻¹ᴱ→⁻¹ = Σ-map id erased

-- Conversions between Contractible and Contractibleᴱ.

Contractible→Contractibleᴱ :
  {@0 A : Type a} 
  Contractible A  Contractibleᴱ A
Contractible→Contractibleᴱ = Σ-map id [_]→

@0 Contractibleᴱ→Contractible : Contractibleᴱ A  Contractible A
Contractibleᴱ→Contractible = Σ-map id erased

-- Conversions between CP.Is-equivalence and Is-equivalenceᴱ.

Is-equivalence→Is-equivalenceᴱ :
  {@0 A : Type a} {@0 B : Type b} {@0 f : A  B} 
  CP.Is-equivalence f  Is-equivalenceᴱ f
Is-equivalence→Is-equivalenceᴱ eq y =
    ⁻¹→⁻¹ᴱ (proj₁₀ (eq y))
  , [ cong ⁻¹→⁻¹ᴱ  proj₂ (eq y)  ⁻¹ᴱ→⁻¹ ]

@0 Is-equivalenceᴱ→Is-equivalence :
  Is-equivalenceᴱ f  CP.Is-equivalence f
Is-equivalenceᴱ→Is-equivalence eq y =
    ⁻¹ᴱ→⁻¹ (proj₁ (eq y))
  , cong ⁻¹ᴱ→⁻¹  erased (proj₂ (eq y))  ⁻¹→⁻¹ᴱ

-- Conversions between CP._≃_ and _≃ᴱ_.

≃→≃ᴱ :
  {@0 A : Type a} {@0 B : Type b} 
  A CP.≃ B  A ≃ᴱ B
≃→≃ᴱ = Σ-map id Is-equivalence→Is-equivalenceᴱ

@0 ≃ᴱ→≃ : A ≃ᴱ B  A CP.≃ B
≃ᴱ→≃ = Σ-map id Is-equivalenceᴱ→Is-equivalence

------------------------------------------------------------------------
-- Some results related to Contractibleᴱ

-- Contractibleᴱ respects split surjections with erased proofs.

Contractibleᴱ-respects-surjection :
  {@0 A : Type a} {@0 B : Type b}
  (f : A  B)  @0 Split-surjective f 
  Contractibleᴱ A  Contractibleᴱ B
Contractibleᴱ-respects-surjection {A = A} {B = B} f s h@(x , _) =
    f x
  , [ proj₂ (H-level.respects-surjection surj 0
               (Contractibleᴱ→Contractible h))
    ]
  where
  @0 surj : A  B
  surj = record
    { logical-equivalence = record
      { to   = f
      ; from = proj₁  s
      }
    ; right-inverse-of = proj₂  s
    }

-- "Preimages" (with erased proofs) of an erased function with a
-- quasi-inverse with erased proofs are contractible.

Contractibleᴱ-⁻¹ᴱ :
  {@0 A : Type a} {@0 B : Type b}
  (@0 f : A  B)
  (g : B  A)
  (@0 f∘g :  x  f (g x)  x)
  (@0 g∘f :  x  g (f x)  x) 
   y  Contractibleᴱ (f ⁻¹ᴱ y)
Contractibleᴱ-⁻¹ᴱ {A = A} {B = B} f g f∘g g∘f y =
    (g y , [ proj₂ (proj₁ c′) ])
  , [ cong ⁻¹→⁻¹ᴱ  proj₂ c′  ⁻¹ᴱ→⁻¹ ]
  where
  @0 A↔B : A  B
  A↔B = record
    { surjection = record
      { logical-equivalence = record
        { to   = f
        ; from = g
        }
      ; right-inverse-of = f∘g
      }
    ; left-inverse-of = g∘f
    }

  @0 c′ : Contractible (f ⁻¹ y)
  c′ = Preimage.bijection⁻¹-contractible A↔B y

-- If an inhabited type comes with an erased proof of
-- propositionality, then it is contractible (with erased proofs).

inhabited→Is-proposition→Contractibleᴱ :
  {@0 A : Type a} 
  A  @0 Is-proposition A  Contractibleᴱ A
inhabited→Is-proposition→Contractibleᴱ x prop = (x , [ prop x ])

-- Some closure properties.

Contractibleᴱ-Σ :
  {@0 A : Type a} {@0 P : A  Type p} 
  Contractibleᴱ A  (∀ x  Contractibleᴱ (P x))  Contractibleᴱ (Σ A P)
Contractibleᴱ-Σ cA@(a , _) cP =
    (a , proj₁₀ (cP a))
  , [ proj₂ $ Σ-closure 0 (Contractibleᴱ→Contractible cA)
                          (Contractibleᴱ→Contractible  cP)
    ]

Contractibleᴱ-× :
  {@0 A : Type a} {@0 B : Type b} 
  Contractibleᴱ A  Contractibleᴱ B  Contractibleᴱ (A × B)
Contractibleᴱ-× cA cB = Contractibleᴱ-Σ cA  _  cB)

Contractibleᴱ-Π :
  {@0 A : Type a} {@0 P : A  Type p} 
  @0 Extensionality a p 
  (∀ x  Contractibleᴱ (P x))  Contractibleᴱ ((x : A)  P x)
Contractibleᴱ-Π ext c =
    proj₁₀  c
  , [ proj₂ $ Π-closure ext 0 (Contractibleᴱ→Contractible  c)
    ]

Contractibleᴱ-↑ :
  {@0 A : Type a} 
  Contractibleᴱ A  Contractibleᴱ (  A)
Contractibleᴱ-↑ c@(a , _) =
    lift a
  , [ proj₂ $ ↑-closure 0 (Contractibleᴱ→Contractible c)
    ]