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

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

open import Equality

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

open Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection eq using (_↔_)
open import Equivalence eq as Eq using (_≃_; Is-equivalence)
import Equivalence.Contractible-preimages eq as CP
open import Erased.Level-1 eq as Erased
  hiding (module []-cong; module []-cong₁;
          module []-cong₂; module []-cong₂-⊔)
open import Extensionality eq
open import Function-universe eq hiding (id; _∘_)
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

open import Equivalence.Erased.Contractible-preimages.Basics eq public

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

-- Another conversion between _⁻¹_ and _⁻¹ᴱ_.

@0 ⁻¹≃⁻¹ᴱ : f ⁻¹ y  f ⁻¹ᴱ y
⁻¹≃⁻¹ᴱ {f = f} {y = y} =
  ( λ x  f x  y)           ↝⟨ (∃-cong λ _  Eq.inverse $ Eq.↔⇒≃ $ erased Erased↔) ⟩□
  ( λ x  Erased (f x  y))  

_ : _≃_.to ⁻¹≃⁻¹ᴱ p  ⁻¹→⁻¹ᴱ p
_ = refl _

@0 _ : _≃_.from ⁻¹≃⁻¹ᴱ p  ⁻¹ᴱ→⁻¹ p
_ = refl _

-- Another conversion between Contractible and Contractibleᴱ.

@0 Contractible≃Contractibleᴱ :
  Contractible A  Contractibleᴱ A
Contractible≃Contractibleᴱ =
  ( λ x   y  x  y)           ↝⟨ (∃-cong λ _  Eq.inverse $ Eq.↔⇒≃ $ erased Erased↔) ⟩□
  ( λ x  Erased (∀ y  x  y))  

_ :
  _≃_.to Contractible≃Contractibleᴱ c  Contractible→Contractibleᴱ c
_ = refl _

@0 _ :
  _≃_.from Contractible≃Contractibleᴱ c  Contractibleᴱ→Contractible c
_ = refl _

private

  -- In an erased context CP.Is-equivalence and Is-equivalenceᴱ are
  -- pointwise equivalent (assuming extensionality).
  --
  -- This lemma is not exported. See Is-equivalence≃Is-equivalenceᴱ
  -- below, which computes in a different way.

  @0 Is-equivalence≃Is-equivalenceᴱ′ :
    {A : Type a} {B : Type b} {f : A  B} 
    CP.Is-equivalence f ↝[ a  b  a  b ] Is-equivalenceᴱ f
  Is-equivalence≃Is-equivalenceᴱ′ {a = a} {f = f} {k = k} ext =
    (∀ y  Contractible (f ⁻¹ y))    ↝⟨ (∀-cong ext′ λ _  H-level-cong ext 0 ⁻¹≃⁻¹ᴱ) 
    (∀ y  Contractible (f ⁻¹ᴱ y))   ↝⟨ (∀-cong ext′ λ _  from-isomorphism Contractible≃Contractibleᴱ) ⟩□
    (∀ y  Contractibleᴱ (f ⁻¹ᴱ y))  
    where
    ext′ = lower-extensionality? k a lzero ext

------------------------------------------------------------------------
-- Some type formers are propositional in erased contexts

-- In an erased context Contractibleᴱ is propositional (assuming
-- extensionality).

@0 Contractibleᴱ-propositional :
  {A : Type a} 
  Extensionality a a 
  Is-proposition (Contractibleᴱ A)
Contractibleᴱ-propositional ext =
  H-level.respects-surjection
    (_≃_.surjection Contractible≃Contractibleᴱ)
    1
    (Contractible-propositional ext)

-- In an erased context Is-equivalenceᴱ f is a proposition (assuming
-- extensionality).
--
-- See also Is-equivalenceᴱ-propositional-for-Erased below.

@0 Is-equivalenceᴱ-propositional :
  {A : Type a} {B : Type b} 
  Extensionality (a  b) (a  b) 
  (f : A  B)  Is-proposition (Is-equivalenceᴱ f)
Is-equivalenceᴱ-propositional ext f =
  H-level.respects-surjection
    (_≃_.surjection $ Is-equivalence≃Is-equivalenceᴱ′ ext)
    1
    (Is-equivalence-CP-propositional ext)

------------------------------------------------------------------------
-- More conversion lemmas

-- In an erased context CP.Is-equivalence and Is-equivalenceᴱ are
-- pointwise equivalent (assuming extensionality).

@0 Is-equivalence≃Is-equivalenceᴱ :
  {A : Type a} {B : Type b} {f : A  B} 
  CP.Is-equivalence f ↝[ a  b  a  b ] Is-equivalenceᴱ f
Is-equivalence≃Is-equivalenceᴱ {k = equivalence} ext =
  Eq.with-other-function
    (Eq.with-other-inverse
       (Is-equivalence≃Is-equivalenceᴱ′ ext)
       Is-equivalenceᴱ→Is-equivalence
        _  Is-equivalence-CP-propositional ext _ _))
    Is-equivalence→Is-equivalenceᴱ
     _  Is-equivalenceᴱ-propositional ext _ _ _)
Is-equivalence≃Is-equivalenceᴱ = Is-equivalence≃Is-equivalenceᴱ′

_ :
  _≃_.to (Is-equivalence≃Is-equivalenceᴱ ext) p 
  Is-equivalence→Is-equivalenceᴱ p
_ = refl _

@0 _ :
  _≃_.from (Is-equivalence≃Is-equivalenceᴱ ext) p 
  Is-equivalenceᴱ→Is-equivalence p
_ = refl _

-- In an erased context CP._≃_ and _≃ᴱ_ are pointwise equivalent
-- (assuming extensionality).

@0 ≃≃≃ᴱ :
  {A : Type a} {B : Type b} 
  (A CP.≃ B) ↝[ a  b  a  b ] (A ≃ᴱ B)
≃≃≃ᴱ {A = A} {B = B} ext =
  A CP.≃ B                       ↔⟨⟩
  ( λ f  CP.Is-equivalence f)  ↝⟨ (∃-cong λ _  Is-equivalence≃Is-equivalenceᴱ ext) 
  ( λ f  Is-equivalenceᴱ f)    ↔⟨⟩
  A ≃ᴱ B                         

_ : _≃_.to (≃≃≃ᴱ ext) p  ≃→≃ᴱ p
_ = refl _

@0 _ : _≃_.from (≃≃≃ᴱ ext) p  ≃ᴱ→≃ p
_ = refl _

-- An isomorphism relating _⁻¹ᴱ_ to _⁻¹_.

Erased-⁻¹ᴱ↔Erased-⁻¹ :
  {@0 A : Type a} {@0 B : Type b} {@0 f : A  B} {@0 y : B} 
  Erased (f ⁻¹ᴱ y)  Erased (f ⁻¹ y)
Erased-⁻¹ᴱ↔Erased-⁻¹ {f = f} {y = y} =
  Erased ( λ x  Erased (f x  y))             ↝⟨ Erased-Σ↔Σ 
  ( λ x  Erased (Erased (f (erased x)  y)))  ↝⟨ (∃-cong λ _  Erased-Erased↔Erased) 
  ( λ x  Erased (f (erased x)  y))           ↝⟨ inverse Erased-Σ↔Σ ⟩□
  Erased ( λ x  f x  y)                      

-- An isomorphism relating Contractibleᴱ to Contractible.

Erased-Contractibleᴱ↔Erased-Contractible :
  {@0 A : Type a} 
  Erased (Contractibleᴱ A)  Erased (Contractible A)
Erased-Contractibleᴱ↔Erased-Contractible =
  Erased ( λ x  Erased (∀ y  x  y))           ↝⟨ Erased-Σ↔Σ 
  ( λ x  Erased (Erased (∀ y  erased x  y)))  ↝⟨ (∃-cong λ _  Erased-Erased↔Erased) 
  ( λ x  Erased (∀ y  erased x  y))           ↝⟨ inverse Erased-Σ↔Σ ⟩□
  Erased ( λ x   y  x  y)                    

------------------------------------------------------------------------
-- Results that follow if the []-cong axioms hold for one universe
-- level

module []-cong₁ (ax : []-cong-axiomatisation ) where

  open Erased-cong ax ax
  open Erased.[]-cong₁ ax

  ----------------------------------------------------------------------
  -- Some results related to _⁻¹ᴱ_

  -- The function _⁻¹ᴱ y respects erased extensional equality.

  ⁻¹ᴱ-respects-extensional-equality :
    {@0 B : Type } {@0 f g : A  B} {@0 y : B} 
    @0 (∀ x  f x  g x)  f ⁻¹ᴱ y  g ⁻¹ᴱ y
  ⁻¹ᴱ-respects-extensional-equality {f = f} {g = g} {y = y} f≡g =
    ( λ x  Erased (f x  y))  ↝⟨ (∃-cong λ _  Erased-cong-≃ (≡⇒↝ _ (cong (_≡ _) $ f≡g _))) ⟩□
    ( λ x  Erased (g x  y))  

  -- An isomorphism relating _⁻¹ᴱ_ to _⁻¹_.

  ⁻¹ᴱ[]↔⁻¹[] :
    {@0 B : Type } {f : A  Erased B} {@0 y : B} 
    f ⁻¹ᴱ [ y ]  f ⁻¹ [ y ]
  ⁻¹ᴱ[]↔⁻¹[] {f = f} {y = y} =
    ( λ x  Erased (f x  [ y ]))       ↔⟨ (∃-cong λ _  Erased-cong-≃ (Eq.≃-≡ $ Eq.↔⇒≃ $ inverse $ erased Erased↔)) 
    ( λ x  Erased (erased (f x)  y))  ↝⟨ (∃-cong λ _  Erased-≡↔[]≡[]) ⟩□
    ( λ x  f x  [ y ])                

  -- Erased "commutes" with _⁻¹ᴱ_.

  Erased-⁻¹ᴱ :
    {@0 A : Type a} {@0 B : Type } {@0 f : A  B} {@0 y : B} 
    Erased (f ⁻¹ᴱ y)  map f ⁻¹ᴱ [ y ]
  Erased-⁻¹ᴱ {f = f} {y = y} =
    Erased (f ⁻¹ᴱ y)  ↝⟨ Erased-⁻¹ᴱ↔Erased-⁻¹ 
    Erased (f ⁻¹ y)   ↝⟨ Erased-⁻¹ 
    map f ⁻¹ [ y ]    ↝⟨ inverse ⁻¹ᴱ[]↔⁻¹[] ⟩□
    map f ⁻¹ᴱ [ y ]   

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

  -- Erased commutes with Contractibleᴱ.

  Erased-Contractibleᴱ↔Contractibleᴱ-Erased :
    {@0 A : Type } 
    Erased (Contractibleᴱ A) ↝[    ]ᴱ Contractibleᴱ (Erased A)
  Erased-Contractibleᴱ↔Contractibleᴱ-Erased {A = A} ext =
    Erased ( λ x  Erased ((y : A)  x  y))           ↔⟨ Erased-cong-↔ (∃-cong λ _  erased Erased↔) 
    Erased ( λ x  (y : A)  x  y)                    ↔⟨ Erased-Σ↔Σ 
    ( λ x  Erased ((y : A)  erased x  y))           ↝⟨ (∃-cong λ _ 
                                                            Erased-cong?
                                                               ext  ∀-cong ext λ _ 
                                                                         from-isomorphism (inverse $ erased Erased↔))
                                                              ext) 
    ( λ x  Erased ((y : A)  Erased (erased x  y)))  ↝⟨ (∃-cong λ _ 
                                                            Erased-cong?
                                                               ext  Π-cong ext (inverse $ erased Erased↔) λ _ 
                                                                         from-isomorphism Erased-≡↔[]≡[])
                                                              ext) ⟩□
    ( λ x  Erased ((y : Erased A)  x  y))           

  -- An isomorphism relating Contractibleᴱ to Contractible.

  Contractibleᴱ-Erased↔Contractible-Erased :
    {@0 A : Type } 
    Contractibleᴱ (Erased A) ↝[    ] Contractible (Erased A)
  Contractibleᴱ-Erased↔Contractible-Erased {A = A} ext =
    Contractibleᴱ (Erased A)  ↝⟨ inverse-erased-ext? Erased-Contractibleᴱ↔Contractibleᴱ-Erased ext 
    Erased (Contractibleᴱ A)  ↔⟨ Erased-Contractibleᴱ↔Erased-Contractible 
    Erased (Contractible A)   ↝⟨ Erased-H-level↔H-level 0 ext ⟩□
    Contractible (Erased A)   

------------------------------------------------------------------------
-- Results that follow if the []-cong axioms hold for two universe
-- levels

module []-cong₂
  (ax₁ : []-cong-axiomatisation ℓ₁)
  (ax₂ : []-cong-axiomatisation ℓ₂)
  where

  open Erased-cong ax₁ ax₂

  ----------------------------------------------------------------------
  -- A result related to Contractibleᴱ

  -- Contractibleᴱ preserves isomorphisms (assuming extensionality).

  Contractibleᴱ-cong :
    {A : Type ℓ₁} {B : Type ℓ₂} 
    @0 Extensionality? k′ (ℓ₁  ℓ₂) (ℓ₁  ℓ₂) 
    A ↔[ k ] B  Contractibleᴱ A ↝[ k′ ] Contractibleᴱ B
  Contractibleᴱ-cong {A = A} {B = B} ext A↔B =
    ( λ (x : A)  Erased ((y : A)  x  y))  ↝⟨ (Σ-cong A≃B′ λ _ 
                                                  Erased-cong?
                                                     ext  Π-cong ext A≃B′ λ _ 
                                                             from-isomorphism $ inverse $ Eq.≃-≡ A≃B′)
                                                    ext) ⟩□
    ( λ (x : B)  Erased ((y : B)  x  y))  
    where
    A≃B′ = from-isomorphism A↔B

------------------------------------------------------------------------
-- Results that follow if the []-cong axioms hold for two universe
-- levels and their maximum

module []-cong₂-⊔
  (ax₁ : []-cong-axiomatisation ℓ₁)
  (ax₂ : []-cong-axiomatisation ℓ₂)
  (ax  : []-cong-axiomatisation (ℓ₁  ℓ₂))
  where

  ----------------------------------------------------------------------
  -- A preservation lemma

  -- Is-equivalenceᴱ f is equivalent to Is-equivalenceᴱ g if f and g
  -- are pointwise equal (assuming extensionality).

  Is-equivalenceᴱ-cong :
    {A : Type ℓ₁} {B : Type ℓ₂} {@0 f g : A  B} 
    Extensionality? k (ℓ₁  ℓ₂) (ℓ₁  ℓ₂) 
    @0 (∀ x  f x  g x) 
    Is-equivalenceᴱ f ↝[ k ] Is-equivalenceᴱ g
  Is-equivalenceᴱ-cong {k = k} ext f≡g =
    ∀-cong (lower-extensionality? k ℓ₁ lzero ext) λ _ 
    []-cong₂.Contractibleᴱ-cong ax ax ext $ ∃-cong λ _ 
    Erased-cong.Erased-cong-≃ ax₂ ax₂ (≡⇒↝ _ $ cong (_≡ _) $ f≡g _)

  ----------------------------------------------------------------------
  -- Some equivalences

  -- A variant of ∘⁻¹≃.

  ∘⁻¹ᴱ≃ :
     {B : Type ℓ₁} {C : Type ℓ₂} {z} 
    (f : B  C) (g : A  B) 
    f  g ⁻¹ᴱ z   λ (([ y , _ ]) : Erased (f ⁻¹ z))  g ⁻¹ᴱ y
  ∘⁻¹ᴱ≃ {z = z} f g =
    f  g ⁻¹ᴱ z                                                       ↔⟨⟩
    ( λ a  Erased (f (g a)  z))                                    ↔⟨ (∃-cong λ _  Erased-cong.Erased-cong-≃ ax₂ ax (other-∃-intro _ _)) 
    ( λ a  Erased ( λ y  f y  z × g a  y))                      ↔⟨ (∃-cong λ _  Erased-cong.Erased-cong-↔ ax ax Σ-assoc) 
    ( λ a  Erased ( λ ((y , _) : f ⁻¹ z)  g a  y))               ↔⟨ (∃-cong λ _  Erased-Σ↔Σ) 
    ( λ a   λ (([ y , _ ]) : Erased (f ⁻¹ z))  Erased (g a  y))  ↔⟨ ∃-comm ⟩□
    ( λ (([ y , _ ]) : Erased (f ⁻¹ z))  g ⁻¹ᴱ y)                   

  -- A variant of to-∘-⁻¹-≃-⁻¹-from.

  to-∘-⁻¹ᴱ-≃-⁻¹ᴱ-from :
    {B : Type ℓ₁} {C : Type ℓ₂} {f : A  B} {z : C} 
    (B≃C : B  C) 
    _≃_.to B≃C  f ⁻¹ᴱ z  f ⁻¹ᴱ _≃_.from B≃C z
  to-∘-⁻¹ᴱ-≃-⁻¹ᴱ-from {f = f} {z = z} B≃C =
    _≃_.to B≃C  f ⁻¹ᴱ z                                      ↝⟨ ∘⁻¹ᴱ≃ _ _ 
    ( λ (([ y , _ ]) : Erased (_≃_.to B≃C ⁻¹ z))  f ⁻¹ᴱ y)  ↔⟨ drop-⊤-left-Σ $
                                                                 _⇔_.to contractible⇔↔⊤ $
                                                                 Erased.[]-cong₁.H-level-Erased ax 0 (Preimage.bijection⁻¹-contractible (_≃_.bijection B≃C) _) ⟩□
    f ⁻¹ᴱ _≃_.from B≃C z                                      

------------------------------------------------------------------------
-- Results that follow if the []-cong axioms hold for all universe
-- levels

module []-cong (ax :  {}  []-cong-axiomatisation ) where

  private
    open module BC₁ {} =
      []-cong₁ (ax { = })
      public
    open module BC₂ {ℓ₁ ℓ₂} =
      []-cong₂ (ax { = ℓ₁}) (ax { = ℓ₂})
      public
    open module BC₂-⊔ {ℓ₁ ℓ₂} =
      []-cong₂-⊔ (ax { = ℓ₁}) (ax { = ℓ₂}) ax
      public