------------------------------------------------------------------------
-- Some alternative definitions of the concept of being an equivalence
------------------------------------------------------------------------

-- Partly based on the blog post "Universal properties without
-- function extensionality" by Mike Shulman
-- (https://homotopytypetheory.org/2014/11/02/universal-properties-without-function-extensionality/),
-- and the corresponding code in the Coq HoTT library
-- (https://github.com/HoTT/HoTT).

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

open import Equality

module Equivalence.Path-split
  {e⁺} (eq :  {a p}  Equality-with-J a p e⁺) where

open Derived-definitions-and-properties eq

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

open import Bijection eq as B using (_↔_)
open import Embedding eq using (Embedding)
open import Equality.Decision-procedures eq
open import Equivalence eq as Eq using (_≃_; Is-equivalence)
open import Equivalence.Erased.Basics eq using (Is-equivalenceᴱ)
open import Extensionality eq
open import Function-universe eq as F hiding (id; _∘_)
open import H-level eq as H-level
open import H-level.Closure eq
open import Pullback eq using ()
open import Surjection eq using (Split-surjective; _↠_)

private
  variable
    a b c d  p q : Level
    A B C         : Type a
    P             : A  Type p
    x y           : A
    f             : A  B
    k             : Kind
    n             : 

------------------------------------------------------------------------
-- Path-split

-- An alternative definition of "Is-equivalence".

Path-split : {A : Type a} {B : Type b}    (A  B)  Type (a  b)
Path-split zero    f =  _ 
Path-split (suc n) f =
  Split-surjective f ×
  (∀ x y  Path-split n (cong {x = x} {y = y} f))

private

  -- A lemma.

  eq→emb : Is-equivalence f  Is-equivalence (cong {x = x} {y = y} f)
  eq→emb eq =
    Embedding.is-embedding (from-isomorphism Eq.⟨ _ , eq ) _ _

-- Equivalences are path-split.

Is-equivalence→Path-split : Is-equivalence f  Path-split n f
Is-equivalence→Path-split {n = zero}  eq = _
Is-equivalence→Path-split {n = suc n} eq =
    _≃_.split-surjective Eq.⟨ _ , eq 
  , λ x y  Is-equivalence→Path-split (eq→emb eq)

private

  -- Path-split n f holds, for n ≥ 2, iff f is an equivalence.

  Path-split⇔Is-equivalence :
    Path-split (2 + n) f  Is-equivalence f
  Path-split⇔Is-equivalence {f = f} = record
    { to   = λ (s , p) 
               let inv    = proj₁  s
                   is-inv = proj₂  s
               in _≃_.is-equivalence $ Eq.↔⇒≃ (record
                    { surjection = record
                      { right-inverse-of = is-inv
                      }
                    ; left-inverse-of = λ x   $⟨ is-inv (f x) 
                        f (inv (f x))  f x    ↝⟨ proj₁  proj₁ (p _ _) 
                        inv (f x)  x          
                    })
    ; from = Is-equivalence→Path-split
    }

-- If f is an equivalence, then Split-surjective f is contractible
-- (assuming extensionality).

Split-surjective-contractible-for-equivalences :
   {a b} {A : Type a} {B : Type b} {f : A  B} 
  Extensionality b (a  b) 
  Is-equivalence f 
  Contractible (Split-surjective f)
Split-surjective-contractible-for-equivalences
  {A = A} {B = B} {f = f} ext eq =

  propositional⇒inhabited⇒contractible
    (Π-closure ext 1 λ y 
     let surj : ( λ x  x  _≃_.from A≃B y)  ( λ x  f x  y)
         surj = ∃-cong λ x 
           x  _≃_.from A≃B y        ↔⟨ inverse $ Eq.≃-≡ A≃B 
           f x  f (_≃_.from A≃B y)  ↝⟨ ≡⇒↝ _ $ cong (_ ≡_) $ _≃_.right-inverse-of A≃B _ ⟩□
           f x  y                   
     in
     H-level.respects-surjection surj 1 $
     mono₁ 0 $
     singleton-contractible _)
    (_≃_.split-surjective A≃B)
  where
  A≃B : A  B
  A≃B = Eq.⟨ _ , eq 

-- If f is an equivalence, then Path-split n f is contractible
-- (assuming extensionality).

Path-split-contractible-for-equivalences :
  {A : Type a} {B : Type b} {f : A  B} 
  Extensionality (a  b) (a  b) 
  Is-equivalence f 
  Contractible (Path-split n f)
Path-split-contractible-for-equivalences {n = zero} _ _ =
  ↑-closure 0 $
  ⊤-contractible

Path-split-contractible-for-equivalences
  {a = a} {b = b} {n = suc n} {A = A} {B = B} {f = f} ext eq =

  ×-closure 0
    (Split-surjective-contractible-for-equivalences
       (lower-extensionality a lzero ext) eq)
    (Π-closure (lower-extensionality b lzero ext) 0 λ _ 
     Π-closure (lower-extensionality b lzero ext) 0 λ _ 
     Path-split-contractible-for-equivalences
        ext (eq→emb eq))

-- Path-split n is pointwise propositional for n ≥ 2 (assuming
-- extensionality).

Path-split-propositional :
  {A : Type a} {B : Type b} {f : A  B} 
  Extensionality (a  b) (a  b) 
  Is-proposition (Path-split (2 + n) f)
Path-split-propositional ext =
  [inhabited⇒contractible]⇒propositional λ p 
  Path-split-contractible-for-equivalences ext $
    _⇔_.to Path-split⇔Is-equivalence p

-- There is a bijection between Path-split n f, for n ≥ 2, and
-- Is-equivalence f (assuming extensionality).

Path-split↔Is-equivalence :
  {A : Type a} {B : Type b} {f : A  B} 
  Path-split (2 + n) f ↝[ a  b  a  b ] Is-equivalence f
Path-split↔Is-equivalence =
  generalise-ext?-prop
    Path-split⇔Is-equivalence
    Path-split-propositional
    Is-equivalence-propositional

-- Another alternative definition of "Is-equivalence".

Path-split-∞ : {A : Type a} {B : Type b}  (A  B)  Type (a  b)
Path-split-∞ f =  n  Path-split n f

-- Path-split-∞ is pointwise propositional (assuming extensionality).

Path-split-∞-propositional :
  {A : Type a} {B : Type b} {f : A  B} 
  Extensionality (a  b) (a  b) 
  Is-proposition (Path-split-∞ f)
Path-split-∞-propositional ext =
  [inhabited⇒contractible]⇒propositional λ p 
  Π-closure (lower-extensionality _ lzero ext) 0 λ _ 
  Path-split-contractible-for-equivalences ext $
    _⇔_.to Path-split⇔Is-equivalence (p 2)

-- There is a bijection between Path-split-∞ f and Is-equivalence f
-- (assuming extensionality).

Path-split-∞↔Is-equivalence :
  {A : Type a} {B : Type b} {f : A  B} 
  Path-split-∞ f ↝[ a  b  a  b ] Is-equivalence f
Path-split-∞↔Is-equivalence =
  generalise-ext?-prop
    (record
       { to   = λ p  _⇔_.to Path-split⇔Is-equivalence (p 2)
       ; from = λ eq _  Is-equivalence→Path-split eq
       })
    Path-split-∞-propositional
    Is-equivalence-propositional

-- A preservation lemma for Path-split.

Path-split-cong :
  {A : Type a} {B : Type b} {C : Type c} {D : Type d}
  {f : A  B} {g : C  D} 
  Extensionality? k (a  b  c  d) (a  b  c  d) 
  (A≃C : A  C) (B≃D : B  D) 
  (∀ x  g (_≃_.to A≃C x)  _≃_.to B≃D (f x)) 
   n  Path-split n f ↝[ k ] Path-split n g
Path-split-cong
  {a = a} {b = b} {c = c} {d = d} {k = k} {f = f} {g = g}
  ext A≃C B≃D hyp = λ where

  zero 
     _   ↔⟨ B.↑↔ 
          ↔⟨ inverse B.↑↔ ⟩□
     _   

  (suc n) 

    (Split-surjective f                   ↔⟨⟩

     (∀ y   λ x  f x  y)              ↝⟨ (Π-cong (lower-extensionality? k (a  c) lzero ext) B≃D λ y 
                                              Σ-cong A≃C λ x 

       (f x  y)                                ↔⟨ inverse $ Eq.≃-≡ B≃D 
       (_≃_.to B≃D (f x)  _≃_.to B≃D y)        ↝⟨ ≡⇒↝ _ $ cong (_≡ _) $ sym $ hyp x ⟩□
       (g (_≃_.to A≃C x)  _≃_.to B≃D y)        ) 

     (∀ y   λ x  g x  y)              ↔⟨⟩

     Split-surjective g                   )

      ×-cong

    (Π-cong (lower-extensionality? k (b  d) lzero ext) A≃C λ x 
     Π-cong (lower-extensionality? k (b  d) lzero ext) A≃C λ y 
     Path-split-cong ext

       (x  y                        ↝⟨ inverse $ Eq.≃-≡ A≃C ⟩□
        _≃_.to A≃C x  _≃_.to A≃C y  )

       (f x  f y                            ↝⟨ inverse $ Eq.≃-≡ B≃D 
        _≃_.to B≃D (f x)  _≃_.to B≃D (f y)  ↝⟨ ≡⇒↝ _ $ cong₂ _≡_ (sym $ hyp x) (sym $ hyp y) ⟩□
        g (_≃_.to A≃C x)  g (_≃_.to A≃C y)  )

        x≡y 
          cong g (cong (_≃_.to A≃C) x≡y)                            ≡⟨ cong-∘ _ _ _ 

          cong (g  _≃_.to A≃C) x≡y                                 ≡⟨ elim¹
                                                                          {y} x≡y 
                                                                            cong (g  _≃_.to A≃C) x≡y 
                                                                            trans (trans (hyp x) (cong (_≃_.to B≃D  f) x≡y))
                                                                              (sym $ hyp y))
                                                                         (
            cong (g  _≃_.to A≃C) (refl _)                                ≡⟨ cong-refl _ 

            refl _                                                        ≡⟨ sym $ trans-symʳ _ 

            trans (hyp x) (sym $ hyp x)                                   ≡⟨ cong (flip trans _) $
                                                                             trans (sym $ trans-reflʳ _) $
                                                                             cong (trans _) $ sym $ cong-refl _ ⟩∎
            trans (trans (hyp x) (cong (_≃_.to B≃D  f) (refl _)))
              (sym $ hyp x)                                               )
                                                                         _ 
          trans (trans (hyp x) (cong (_≃_.to B≃D  f) x≡y))
            (sym $ hyp y)                                           ≡⟨ trans (cong (flip trans _) $ sym $
                                                                              subst-trans _) $
                                                                       trans-subst 
          subst (_ ≡_) (sym $ hyp y)
            (subst (_≡ _) (sym $ hyp x)
               (cong (_≃_.to B≃D  f) x≡y))                         ≡⟨ trans (cong (subst _ _) $
                                                                              subst-in-terms-of-≡⇒↝ equivalence _ _ _) $
                                                                       subst-in-terms-of-≡⇒↝ equivalence _ _ _ 
          _≃_.to (≡⇒↝ _ (cong (_ ≡_) (sym $ hyp y)))
            (_≃_.to (≡⇒↝ _ (cong (_≡ _) (sym $ hyp x)))
               (cong (_≃_.to B≃D  f) x≡y))                         ≡⟨ cong (_$ cong (_≃_.to B≃D  f) x≡y) $ sym $
                                                                       ≡⇒↝-trans equivalence 
          _≃_.to
            (≡⇒↝ _ $
             trans (cong (_≡ _) (sym $ hyp x))
               (cong (_ ≡_) (sym $ hyp y)))
            (cong (_≃_.to B≃D  f) x≡y)                             ≡⟨⟩

          _≃_.to (≡⇒↝ _ $ cong₂ _≡_ (sym $ hyp x) (sym $ hyp y))
            (cong (_≃_.to B≃D  f) x≡y)                             ≡⟨ cong (_≃_.to (≡⇒↝ _ _)) $ sym $
                                                                       cong-∘ _ _ _ ⟩∎
          _≃_.to (≡⇒↝ _ $ cong₂ _≡_ (sym $ hyp x) (sym $ hyp y))
            (cong (_≃_.to B≃D) (cong f x≡y))                        )

       n)

-- Path-split 2 f can be expressed using Split-surjective and ∆
-- (assuming extensionality).
--
-- This definition is based on Lemma 2.12 in "Modalities in Homotopy
-- Type Theory" by Rijke, Shulman and Spitters.

Path-split-2≃Split-surjective×Split-surjective-∆ :
  {A : Type a} {B : Type b} {f : A  B} 
  Path-split 2 f
    ↝[ a  b  a  b ]
  (Split-surjective f × Split-surjective ( f))
Path-split-2≃Split-surjective×Split-surjective-∆
  {a = a} {b = b} {f = f} {k = k} ext =
  Path-split 2 f                                ↔⟨⟩

  Split-surjective f ×
  (∀ x y 
   Split-surjective (cong {x = x} {y = y} f) ×
   (∀ x y   _ ))                             ↝⟨ (∃-cong λ _  lemma₁) ⟩□

  Split-surjective f × Split-surjective ( f)   
  where
  ext′ = lower-extensionality? k b lzero ext
  ext″ = lower-extensionality? k a lzero ext

  lemma₂ = λ x y p 
    ( λ (q : x  y)  cong f q  p)                                      ↝⟨ (∃-cong λ q  ≡⇒↝ _ $ cong (_≡ _) (

      cong f q                                                                  ≡⟨ sym $
                                                                                   trans (cong (flip trans _) $
                                                                                          trans (cong sym $ cong-const _)
                                                                                          sym-refl) $
                                                                                   trans (trans-reflˡ _) $
                                                                                   trans-reflˡ _ 
      trans (sym (cong (const (f x)) q))
        (trans (refl (f x)) (cong f q))                                         ≡⟨ sym subst-in-terms-of-trans-and-cong ⟩∎

      subst  y  f x  f y) q (refl (f x))                                    )) 

    ( λ (q : x  y)  subst  y  f x  f y) q (refl (f x))  p)        ↝⟨ B.Σ-≡,≡↔≡ 

    (x , refl (f x))  (y , p)                                            ↝⟨ ≡⇒↝ _ $ cong (_≡ _) $ sym $ subst-refl _ _ 

    (subst  x   λ y  f x  f y) (refl x) (x , refl (f x)) 
     (y , p))                                                             ↝⟨ inverse $
                                                                             drop-⊤-left-Σ $
                                                                             _⇔_.to contractible⇔↔⊤ $ singleton-contractible _ 
    ( λ ((z , q) :  λ z  z  x) 
     subst  x   λ y  f x  f y) q (z , refl (f z))  (y , p))        ↝⟨ inverse Σ-assoc 

    ( λ z   λ (q : z  x) 
     subst  x   λ y  f x  f y) q (z , refl (f z))  (y , p))        ↝⟨ (∃-cong λ _ 
                                                                              B.Σ-≡,≡↔≡) ⟩□
    ( λ z  (z , z , refl (f z))  (x , y , p))                          

  lemma₁ =
    (∀ x y 
     Split-surjective (cong {x = x} {y = y} f) ×
     (∀ x y   _ ))                                                     ↝⟨ (∀-cong ext′ λ _  ∀-cong ext′ λ _ 
                                                                              drop-⊤-right λ _ 
                                                                              from-bijection →-right-zero F.∘
                                                                              ∀-cong ext′ λ _ 
                                                                              from-bijection →-right-zero F.∘
                                                                              ∀-cong ext′ λ _ 
                                                                              from-bijection B.↑↔) 
    (∀ x y  Split-surjective (cong {x = x} {y = y} f))                   ↔⟨⟩

    (∀ x y  (p : f x  f y)   λ (q : x  y)  cong f q  p)            ↝⟨ (∀-cong ext′ λ _  ∀-cong ext′ λ _  ∀-cong ext″ λ _ 
                                                                              from-bijection $ lemma₂ _ _ _) 
    (∀ x y  (p : f x  f y) 
      λ z  (z , z , refl (f z))  (x , y , p))                          ↝⟨ from-bijection (inverse currying) F.∘
                                                                             (∀-cong ext′ λ _  from-bijection (inverse currying)) 

    ((p :  λ x   λ y  f x  f y)   λ z  (z , z , refl (f z))  p)  ↔⟨⟩

    Split-surjective ( f)                                                

------------------------------------------------------------------------
-- Extendable along

-- Is-[ n ]-extendable-along-[ f ] P means that P is n-extendable
-- along f.

Is-[_]-extendable-along-[_] :
  {A : Type a} {B : Type b} 
    (A  B)  (B  Type c)  Type (a  b  c)
Is-[ zero  ]-extendable-along-[ f ] P =  _ 
Is-[ suc n ]-extendable-along-[ f ] P =
  ((g :  x  P (f x)) 
      λ (h :  x  P x)   x  h (f x)  g x) ×
  ((g h :  x  P x) 
     Is-[ n ]-extendable-along-[ f ]  x  g x  h x))

-- Is-∞-extendable-along-[ f ] P means that P is ∞-extendable along f.

Is-∞-extendable-along-[_] :
  {A : Type a} {B : Type b} 
  (A  B)  (B  Type c)  Type (a  b  c)
Is-∞-extendable-along-[ f ] P =
   n  Is-[ n ]-extendable-along-[ f ] P

-- Everything is ∞-extendable along the identity function.

∞-extendable-along-id : Is-∞-extendable-along-[ id ] P
∞-extendable-along-id zero    = _
∞-extendable-along-id (suc n) =
     f  f , refl  f)
  ,  _ _  ∞-extendable-along-id n)

-- In the presence of extensionality Is-[_]-extendable-along-[_] can
-- be expressed using Path-split.

Is-extendable-along≃Path-split :
  {A : Type a} {B : Type b} {P : B  Type p} {f : A  B} 
  Extensionality (a  b  p) (a  b  p) 
   n 
  Is-[ n ]-extendable-along-[ f ] P 
  Path-split n  (g :  x  P x)  g  f)
Is-extendable-along≃Path-split {a = a} {b = b} {p = p} {f = f} ext =
  λ where
    zero     Eq.id
    (suc n) 
      (∀-cong (lower-extensionality b lzero ext) λ g 
       ∃-cong λ h 
         (∀ x  h (f x)  g x)  ↝⟨ Eq.extensionality-isomorphism
                                     (lower-extensionality (b  p) (a  b) ext) ⟩□
         h  f  g              )
        ×-cong
      (∀-cong (lower-extensionality a lzero ext) λ g 
       ∀-cong (lower-extensionality a lzero ext) λ h 
         Is-[ n ]-extendable-along-[ f ]  x  g x  h x)  ↝⟨ Is-extendable-along≃Path-split ext n 
         Path-split n (_∘ f)                                ↝⟨ Path-split-cong ext
                                                                 (Eq.extensionality-isomorphism ext₁)
                                                                 (Eq.extensionality-isomorphism ext₂)
                                                                  eq 
          cong (_∘ f) (apply-ext ext₁ eq)                           ≡⟨ cong-pre-∘-ext ext₂ ext₁ ⟩∎
          apply-ext ext₂ (eq  f)                                   )
                                                                 n ⟩□
         Path-split n (cong (_∘ f))                         )
  where
  ext₁ = lower-extensionality (a  p) (a  b) ext
  ext₂ = lower-extensionality (b  p) (a  b) ext

-- In the presence of extensionality Is-∞-extendable-along-[_] can
-- be expressed using Path-split-∞.

Is-∞-extendable-along≃Path-split-∞ :
  {A : Type a} {B : Type b} {P : B  Type p} {f : A  B} 
  Extensionality (a  b  p) (a  b  p) 
  Is-∞-extendable-along-[ f ] P 
  Path-split-∞  (g :  x  P x)  g  f)
Is-∞-extendable-along≃Path-split-∞ ext =
  ∀-cong (lower-extensionality _ lzero ext) $
  Is-extendable-along≃Path-split ext

-- Is-[ 2 + n ]-extendable-along-[ f ] P is propositional (assuming
-- extensionality).

Is-extendable-along-propositional :
  {A : Type a} {B : Type b} {P : B  Type p} {f : A  B} 
  Extensionality (a  b  p) (a  b  p) 
  Is-proposition (Is-[ 2 + n ]-extendable-along-[ f ] P)
Is-extendable-along-propositional ext =
  H-level-cong _ 1 (inverse $ Is-extendable-along≃Path-split ext _) $
  Path-split-propositional ext

-- Is-∞-extendable-along-[ f ] P is propositional (assuming
-- extensionality).

Is-∞-extendable-along-propositional :
  {A : Type a} {B : Type b} {P : B  Type p} {f : A  B} 
  Extensionality (a  b  p) (a  b  p) 
  Is-proposition (Is-∞-extendable-along-[ f ] P)
Is-∞-extendable-along-propositional ext =
  H-level-cong _ 1 (inverse $ Is-∞-extendable-along≃Path-split-∞ ext) $
  Path-split-∞-propositional ext

-- In the presence of extensionality Is-∞-extendable-along-[_] can be
-- expressed using Is-equivalence.

Is-∞-extendable-along≃Is-equivalence :
  {A : Type a} {B : Type b} {P : B  Type p} {f : A  B} 
  Extensionality (a  b  p) (a  b  p) 
  Is-∞-extendable-along-[ f ] P 
  Is-equivalence  (g :  x  P x)  g  f)
Is-∞-extendable-along≃Is-equivalence {P = P} {f = f} ext =
  Is-∞-extendable-along-[ f ] P  ↝⟨ Is-∞-extendable-along≃Path-split-∞ ext 
  Path-split-∞ (_∘ f)            ↝⟨ Path-split-∞↔Is-equivalence ext ⟩□
  Is-equivalence (_∘ f)          

-- The definitions below are not taken directly from "Universal
-- properties without function extensionality".

-- Is-∞-extendable-along-[_] can sometimes be replaced by
-- Is-equivalence const.

Is-∞-extendable-along≃Is-equivalence-const :
  {A : Type a} {B : Type b} 
  Extensionality (a  b) (a  b) 
  Is-∞-extendable-along-[  (_ : A)  lift tt) ]  (_ :  a )  B) 
  Is-equivalence (const  (B  A  B))
Is-∞-extendable-along≃Is-equivalence-const {a = a} {A = A} {B = B} ext =
  Is-∞-extendable-along-[  _  lift tt) ]  (_ :  a )  B)  ↝⟨ Is-∞-extendable-along≃Is-equivalence ext 

  Is-equivalence (_∘  _  lift tt)  (( a   B)  (A  B)))  ↝⟨ inverse $
                                                                    Is-equivalence≃Is-equivalence-∘ʳ
                                                                      (_≃_.is-equivalence $ Eq.↔→≃ (_$ lift tt) const refl refl) ext ⟩□
  Is-equivalence (const  (B  A  B))                           

-- If f is an equivalence, then n-extendability along f is
-- contractible (assuming extensionality).

Is-extendable-along-contractible-for-equivalences :
  {A : Type a} {B : Type b} {f : A  B} {P : B  Type p} 
  Extensionality (a  b  p) (a  b  p) 
  Is-equivalence f 
   n  Contractible (Is-[ n ]-extendable-along-[ f ] P)
Is-extendable-along-contractible-for-equivalences _ _ zero =
  ↑-closure 0 ⊤-contractible

Is-extendable-along-contractible-for-equivalences
  {a = a} {b = b} {p = p} {f = f} {P = P} ext eq (suc n) =

  ×-closure 0
    (Π-closure (lower-extensionality b lzero ext) 0 λ g 
                                                             $⟨ singleton-contractible _ 
       Contractible ( λ h  h  subst P (inv _)  g  f⁻¹)  ↝⟨ H-level-cong _ 0 (lemma g)  (_  _) ⟩□
       Contractible ( λ h   x  h (f x)  g x)            )
    (Π-closure (lower-extensionality a lzero ext) 0 λ _ 
     Π-closure (lower-extensionality a lzero ext) 0 λ _ 
     Is-extendable-along-contractible-for-equivalences ext eq n)
  where
  f⁻¹ = _≃_.from Eq.⟨ _ , eq 
  inv = _≃_.left-inverse-of (inverse Eq.⟨ _ , eq )

  lemma :  _  _  _
  lemma g =
    ( λ h  h  subst P (inv _)  g  f⁻¹)  ↔⟨ (∃-cong λ h  inverse $
                                                 ∘from≡↔≡∘to′ (lower-extensionality p (a  b) ext) (inverse Eq.⟨ _ , eq )) 
    ( λ h  h  f  g)                      ↝⟨ (∃-cong λ _  inverse $
                                                 Eq.extensionality-isomorphism (lower-extensionality (b  p) (a  b) ext)) ⟩□
    ( λ h   x  h (f x)  g x)            

-- If f is an equivalence, then ∞-extendability along f is
-- contractible (assuming extensionality).

Is-∞-extendable-along-contractible-for-equivalences :
  {A : Type a} {B : Type b} {f : A  B} {P : B  Type p} 
  Extensionality (a  b  p) (a  b  p) 
  Is-equivalence f 
  Contractible (Is-∞-extendable-along-[ f ] P)
Is-∞-extendable-along-contractible-for-equivalences ext eq =
  Π-closure (lower-extensionality _ lzero ext) 0 λ n 
  Is-extendable-along-contractible-for-equivalences ext eq n

------------------------------------------------------------------------
-- Alternatives to Is-[_]-extendable-along-[_] and
-- Is-∞-extendable-along-[_]

-- A variant of Is-[_]-extendable-along-[_].

Is-[_]-extendable-along-const-tt-[_] :
    Type a  Type b  Type (a  b)
Is-[ zero  ]-extendable-along-const-tt-[ A ] B =  _ 
Is-[ suc n ]-extendable-along-const-tt-[ A ] B =
  ((g : A  B)   λ (x : B)   y  x  g y) ×
  ((x y : B)  Is-[ n ]-extendable-along-const-tt-[ A ] (x  y))

-- A variant of Is-∞-extendable-along-[_].

Is-∞-extendable-along-const-tt-[_] :
  Type a  Type b  Type (a  b)
Is-∞-extendable-along-const-tt-[ A ] B =
   n  Is-[ n ]-extendable-along-const-tt-[ A ] B

-- In some cases Is-[_]-extendable-along-[_] and
-- Is-∞-extendable-along-[_] can be replaced by the variants.

≃Is-extendable-along-const-tt :
  {A : Type a} {B : Type b} 
  Extensionality? k (a  b) (a  b) 
   n 
  Is-[ n ]-extendable-along-[  (_ : A)  lift tt) ]
     (_ :  a )  B) ↝[ k ]
  Is-[ n ]-extendable-along-const-tt-[ A ] B
≃Is-extendable-along-const-tt                 _   zero    = F.id
≃Is-extendable-along-const-tt {a = a} {k = k} ext (suc n) =
  (∀-cong ext λ _ 
   Σ-cong (Eq.↔→≃ (_$ lift tt) const refl refl) λ _ 
   F.id)
    ×-cong
  Π-cong ext′ (Eq.↔→≃ (_$ lift tt) const refl refl) λ _ 
  Π-cong ext′ (Eq.↔→≃ (_$ lift tt) const refl refl) λ _ 
  ≃Is-extendable-along-const-tt ext n
  where
  ext′ = lower-extensionality? k a lzero ext

≃Is-∞-extendable-along-const-tt :
  {A : Type a} {B : Type b} 
  Extensionality? k (a  b) (a  b) 
  Is-∞-extendable-along-[  (_ : A)  lift tt) ]  (_ :  a )  B)
    ↝[ k ]
  Is-∞-extendable-along-const-tt-[ A ] B
≃Is-∞-extendable-along-const-tt {k = k} ext =
  ∀-cong (lower-extensionality? k _ lzero ext) λ n 
  ≃Is-extendable-along-const-tt ext n

-- Preservation lemmas for Is-[_]-extendable-along-[_] and
-- Is-∞-extendable-along-[_].

Is-extendable-along-const-tt-cong :
  {A : Type a} {B : Type b} {C : Type c} 
  Extensionality? k (a  b  c) (a  b  c) 
  (A≃B : A  B)
  (A→≃B→ : {C : Type c}  (A  C)  (B  C)) 
  ({C : Type c} (f : A  C) (x : A) 
   _≃_.to A→≃B→ f (_≃_.to A≃B x)  f x) 
   n 
  Is-[ n ]-extendable-along-const-tt-[ A ] C ↝[ k ]
  Is-[ n ]-extendable-along-const-tt-[ B ] C
Is-extendable-along-const-tt-cong _ _ _ _ zero =
   _   ↔⟨ B.↑↔ 
        ↔⟨ inverse B.↑↔ ⟩□
   _   
Is-extendable-along-const-tt-cong
  {a = a} {b = b} {c = c} {k = k} ext A≃B A→≃B→ hyp (suc n) =

  (Π-cong ext A→≃B→ λ g 
   ∃-cong λ x 
   Π-cong (lower-extensionality? k c (a  b) ext) A≃B λ y 
     x  g y                            ↝⟨ ≡⇒↝ _ $ cong (_ ≡_) $ sym $ hyp g y ⟩□
     x  _≃_.to A→≃B→ g (_≃_.to A≃B y)  )
    ×-cong
  (∀-cong (lower-extensionality? k (a  b) lzero ext) λ x 
   ∀-cong (lower-extensionality? k (a  b) lzero ext) λ y 
   Is-extendable-along-const-tt-cong ext A≃B A→≃B→ hyp n)

Is-∞-extendable-along-const-tt-cong :
  {A : Type a} {B : Type b} {C : Type c} 
  Extensionality? k (a  b  c) (a  b  c) 
  (A≃B : A  B)
  (A→≃B→ : {C : Type c}  (A  C)  (B  C)) 
  ({C : Type c} (f : A  C) (x : A) 
   _≃_.to A→≃B→ f (_≃_.to A≃B x)  f x) 
  Is-∞-extendable-along-const-tt-[ A ] C ↝[ k ]
  Is-∞-extendable-along-const-tt-[ B ] C
Is-∞-extendable-along-const-tt-cong {k = k} ext A≃B A→≃B→ hyp =
  ∀-cong (lower-extensionality? k _ lzero ext) λ n 
  Is-extendable-along-const-tt-cong ext A≃B A→≃B→ hyp n

------------------------------------------------------------------------
-- P-null types

-- A type B is P-null for a predicate P of type A → Type p if the
-- function const of type B → P x → B is an equivalence for each x.
--
-- This definition is based on one from "Modalities in Homotopy Type
-- Theory" by Rijke, Shulman and Spitters.

_-Null_ : {A : Type a}  (A  Type p)  Type b  Type (a  b  p)
P -Null B =  x  Is-equivalence (const  (B  P x  B))

-- A variant of _-Null_ with erased proofs.

_-Nullᴱ_ : {A : Type a}  (A  Type p)  Type b  Type (a  b  p)
P -Nullᴱ B =  x  Is-equivalenceᴱ (const  (B  P x  B))

-- P -Null B is a proposition (assuming extensionality).
--
-- See also Equivalence.Erased.Nullᴱ-propositional.

Null-propositional :
  {A : Type a} {P : A  Type p} {B : Type b} 
  Extensionality (a  p  b) (p  b) 
  Is-proposition (P -Null B)
Null-propositional {a = a} {p = p} {b = b} ext =
  Π-closure (lower-extensionality (p  b) lzero ext) 1 λ _ 
  Is-equivalence-propositional (lower-extensionality a lzero ext)

-- The operator _-Null_ preserves equivalences (assuming
-- extensionality).
--
-- See also Equivalence.Erased.[]-cong₂-⊔.Nullᴱ-cong.

Null-cong :
  {A : Type a} {B : Type b} {C : Type c}
  {P : A  Type p} {Q : A  Type q} 
  Extensionality (a  b  c  p  q) (b  c  p  q) 
  (∀ x  P x  Q x)  B  C  P -Null B  Q -Null C
Null-cong
  {a = a} {b = b} {c = c} {p = p} {q = q}
  {B = B} {C = C} {P = P} {Q = Q} ext P≃Q B≃C =
  P -Null B                                                             ↔⟨⟩

  (∀ x  Is-equivalence (const  (B  P x  B)))                        ↝⟨ (∀-cong ext′ λ x 
                                                                            Is-equivalence≃Is-equivalence-∘ʳ
                                                                              (_≃_.is-equivalence $ inverse B≃C) ext″) 

  (∀ x  Is-equivalence ((const  (B  P x  B))  _≃_.from B≃C))       ↝⟨ (∀-cong ext′ λ x 
                                                                            Is-equivalence≃Is-equivalence-∘ˡ
                                                                              (_≃_.is-equivalence $
                                                                               ∀-cong (lower-extensionality (a  b  c  q) (p  q) ext) λ _ 
                                                                               B≃C)
                                                                              ext″) 
  (∀ x 
     Is-equivalence
       ((_≃_.to B≃C ∘_)  (const  (B  P x  B))  _≃_.from B≃C))      ↝⟨ (∀-cong (lower-extensionality (b  c  p  q) (b  q) ext) λ x 
                                                                            Is-equivalence-cong
                                                                              (lower-extensionality (a  b  q) (b  q) ext) λ y 
    const (_≃_.to B≃C (_≃_.from B≃C y))                                       ≡⟨ cong const $ _≃_.right-inverse-of B≃C _ ⟩∎
    const y                                                                   ) 

  (∀ x  Is-equivalence (const  (C  P x  C)))                        ↝⟨ (∀-cong (lower-extensionality (b  c  p  q) b ext) λ x 
                                                                           Is-equivalence≃Is-equivalence-∘ˡ
                                                                             (_≃_.is-equivalence
                                                                                (→-cong
                                                                                   (lower-extensionality (a  b  c) (b  p  q) ext)
                                                                                   (P≃Q x) F.id))
                                                                             (lower-extensionality (a  b) b ext)) 
  (∀ x 
     Is-equivalence ((_∘ _≃_.from (P≃Q x))  (const  (C  P x  C))))  ↔⟨⟩

  (∀ x  Is-equivalence (const  (C  Q x  C)))                        ↔⟨⟩

  Q -Null C                                                             
  where
  ext′ = lower-extensionality (b  c  p  q) q ext
  ext″ = lower-extensionality (a  q)         q ext

-- A corollary of Is-∞-extendable-along≃Is-equivalence-const.

Π-Is-∞-extendable-along≃Null :
  {A : Type a} {P : A  Type p} {B : Type b} 
  Extensionality (a  b  p) (b  p) 
  (∀ x  Is-∞-extendable-along-[  (_ : P x)  lift tt) ]
            (_ :  p )  B)) 
  P -Null B
Π-Is-∞-extendable-along≃Null {a = a} {p = p} {b = b} ext =
  ∀-cong (lower-extensionality (b  p) lzero ext) λ _ 
  Is-∞-extendable-along≃Is-equivalence-const
    (lower-extensionality a lzero ext)

-- If A is contractible, then const : B → A → B is an equivalence
-- (assuming extensionality).

Contractible→Is-equivalence-const :
  {A : Type a} {B : Type b} 
  Extensionality a b 
  Contractible A 
  Is-equivalence (const  (B  A  B))
Contractible→Is-equivalence-const ext c =
  _≃_.is-equivalence $
  Eq.↔→≃
    const
    (_$ proj₁ c)
     f  apply-ext ext λ x 
       f (proj₁ c)  ≡⟨ cong f $ proj₂ c x ⟩∎
       f x          )
    refl

-- If B is contractible, then every type is "λ (_ : A) → B"-null
-- (assuming extensionality).
--
-- Rijke, Shulman and Spitters mention something similar in
-- "Modalities in Homotopy Type Theory".

Contractible→Nullˡ :
  {B : Type b} {C : Type c} 
  Extensionality b c 
  Contractible B 
   (_ : A)  B) -Null C
Contractible→Nullˡ ext c _ =
  Contractible→Is-equivalence-const ext c

-- The unit type is P-null.
--
-- Rijke, Shulman and Spitters mention something similar in
-- "Modalities in Homotopy Type Theory".

Null-⊤ : P -Null 
Null-⊤ _ =
  _≃_.is-equivalence $
  Eq.↔→≃
    _
    _
    refl
    refl

-- P -Null ⊥ holds iff ¬ ¬ P x holds for each x.

Null-⊥≃¬¬ :
  {A : Type a} {P : A  Type p} 
  P -Null  { = } ↝[ a  p    p   ] (∀ x  ¬ ¬ P x)
Null-⊥≃¬¬ {a = a} {p = p} { = } {P = P} =
  generalise-ext?-prop
    (record
       { to = λ eq x 
           ¬ P x      →⟨ ¬↔→⊥ _ 
           (P x  )  ↔⟨ inverse Eq.⟨ _ , eq x  
                     ↔⟨ ⊥↔⊥ ⟩□
           ⊥₀         
       ; from = λ hyp x 
           _≃_.is-equivalence $
           Eq.↔→≃
             _
             (                 $⟨ hyp x 
              ¬ ¬ P x          →⟨ →-cong-→ (→-cong-→ id ⊥-elim) ⊥-elim ⟩□
              ((P x  )  )  )
              f  ⊥-elim $ hyp x (⊥-elim  f))
              ())
       })
    Null-propositional
     ext 
       Π-closure (lower-extensionality (p  )  ext) 1 λ _ 
       ¬-propositional (lower-extensionality (a  ) _ ext))

-- Every type is "λ (x : ⊥ {ℓ = ℓ}) → P x"-null.

Π⊥-Null :  (x :  { = })  P x) -Null A
Π⊥-Null ()

-- If A is inhabited, then (λ (_ : A) → ⊥ {ℓ = ℓ}) -Null B is
-- equivalent to Contractible B (assuming extensionality).
--
-- Rijke, Shulman and Spitters mention something similar in
-- "Modalities in Homotopy Type Theory".

⊥-Null≃Contractible :
  {A : Type a} {B : Type b} 
  Extensionality  b 
  A 
  ((λ (_ : A)   { = }) -Null B)
    ↝[ a  b    b   ]
  Contractible B
⊥-Null≃Contractible {a = a} { = } {B = B} ext inh =
  generalise-ext?-prop
    (record
       { to   =
            _  ) -Null B  →⟨  hyp  Eq.⟨ _ , hyp inh ) 
           B  (  B)        →⟨ Π⊥↔⊤ ext F.∘_ 
           B                →⟨ _⇔_.from contractible⇔↔⊤  _≃_.bijection ⟩□
           Contractible B     
       ; from = λ c x 
           _≃_.is-equivalence $
           Eq.↔→≃
             _
              _  proj₁ c)
              _  apply-ext ext λ ())
             (proj₂ c)
       })
    Null-propositional
     ext 
       H-level-propositional (lower-extensionality (a  )  ext) 0)

-- If A is inhabited and B is "λ (_ : A) → Bool"-null, then B is a
-- proposition.
--
-- This lemma is based on something mentioned by Rijke, Shulman and
-- Spitters in "Modalities in Homotopy Type Theory".

Bool-Null→Is-proposition :
  A   (_ : A)  Bool) -Null B  Is-proposition B
Bool-Null→Is-proposition {B = B} inh null x y =
  x                                       ≡⟨⟩
  xy true                                 ≡⟨ cong (_$ true) $ sym $ _≃_.right-inverse-of equiv _ 
  _≃_.to equiv (_≃_.from equiv xy) true   ≡⟨⟩
  _≃_.from equiv xy                       ≡⟨⟩
  _≃_.to equiv (_≃_.from equiv xy) false  ≡⟨ cong (_$ false) $ _≃_.right-inverse-of equiv _ 
  xy false                                ≡⟨⟩
  y                                       
  where
  equiv : B  (Bool  B)
  equiv = Eq.⟨ const , null inh 

  xy : Bool  B
  xy = if_then x else y

-- If B is a proposition, then it is "λ (_ : A) → Bool"-null (assuming
-- extensionality).
--
-- This lemma is based on something mentioned by Rijke, Shulman and
-- Spitters in "Modalities in Homotopy Type Theory".

Is-proposition→Bool-Null :
  {B : Type b} 
  Extensionality lzero b 
  Is-proposition B   (_ : A)  Bool) -Null B
Is-proposition→Bool-Null ext prop _ =
  _≃_.is-equivalence $
  Eq.↔→≃
    _
     f  f true)
     _  Π-closure ext 1  _  prop) _ _)
    refl

-- If A is inhabited, then (λ (_ : A) → Bool) -Null B is equivalent to
-- Is-proposition B (assuming extensionality).
--
-- Rijke, Shulman and Spitters mention something similar in
-- "Modalities in Homotopy Type Theory".

Bool-Null≃Is-proposition :
  {A : Type a} {B : Type b} 
  Extensionality lzero b 
  A 
  ((λ (_ : A)  Bool) -Null B) ↝[ a  b  b ] Is-proposition B
Bool-Null≃Is-proposition {a = a} ext inh =
  generalise-ext?-prop
    (record
       { to   = Bool-Null→Is-proposition inh
       ; from = Is-proposition→Bool-Null ext
       })
    Null-propositional
     ext 
       H-level-propositional (lower-extensionality a lzero ext) 1)

private

  -- If const is an equivalence from Bool to B → Bool, then B is not
  -- not inhabited (assuming extensionality).

  Is-equivalence-const→¬¬ :
    {B : Type b} 
    Extensionality b lzero 
    Is-equivalence (const  (Bool  B  Bool)) 
    ¬ ¬ B
  Is-equivalence-const→¬¬ {B = B} ext =
    curry
      (Is-equivalence (const  (Bool  B  Bool)) × ¬ B  →⟨ Σ-map Eq.⟨ _ ,_⟩ (Eq.↔⇒≃  inverse  B.⊥↔uninhabited) 
       Bool  (B  Bool) × B                           →⟨  (≃B→ , B≃)  →-cong ext B≃ F.id F.∘ ≃B→) 
       Bool  (  Bool)                                 →⟨ Π⊥↔⊤ ext F.∘_ 
       Bool                                            →⟨  eq  _≃_.to (Eq.≃-≡ eq) (refl _)) 
       true  false                                      →⟨ Bool.true≢false ⟩□
                                                        )

  -- If const is an equivalence from Bool to B → Bool, and equality is
  -- decidable for B, then B is a proposition.

  Is-equivalence-const→Decidable-equality→Is-proposition :
    Is-equivalence (const  (Bool  B  Bool)) 
    Decidable-equality B 
    Is-proposition B
  Is-equivalence-const→Decidable-equality→Is-proposition
    {B = B} eq _≟_ x y = x≡y
    where
    lemma :
      (f g : B  Bool)  f  g 
      (h : B  Bool)  f  h  g  h
    lemma =                                                        $⟨ helper 
      ((x y : Bool)  x  y  (z : Bool)  x  z  y  z)          →⟨ (Π-cong _ equiv λ x  Π-cong _ equiv λ y 
                                                                       →-cong-→ (→-cong-→ (_≃_.from (Eq.≃-≡ equiv)) id) $
                                                                       Π-cong _ equiv λ z 
                                                                       _≃_.from (Eq.≃-≡ equiv ⊎-cong Eq.≃-≡ equiv)) ⟩□
      ((f g : B  Bool)  f  g  (h : B  Bool)  f  h  g  h)  
      where
      equiv : Bool  (B  Bool)
      equiv = Eq.⟨ _ , eq 

      true≡⊎false≡ : (b : Bool)  true  b  false  b
      true≡⊎false≡ true  = inj₁ (refl _)
      true≡⊎false≡ false = inj₂ (refl _)

      helper : (x y : Bool)  x  y  (z : Bool)  x  z  y  z
      helper true  true  t≢t = ⊥-elim $ t≢t (refl _)
      helper true  false _   = true≡⊎false≡
      helper false true  _   = _↔_.to ⊎-comm  true≡⊎false≡
      helper false false f≢f = ⊥-elim $ f≢f (refl _)

    f₁ f₂ f₃ : B  Bool
    f₁ _ = true
    f₂ _ = false
    f₃ z = if x  z then true else false

    f₁≢f₂ : f₁  f₂
    f₁≢f₂ f₁≡f₂ = Bool.true≢false $ cong (_$ x) f₁≡f₂

    f₁≡f₃→x≡y : f₁  f₃  x  y
    f₁≡f₃→x≡y f₁≡f₃ = helper (x  y) (cong (_$ y) f₁≡f₃)
      where
      helper :
        (d : Dec (x  y)) 
        true  if d then true else false 
        x  y
      helper (yes x≡y) _          = x≡y
      helper (no  _)   true≡false =
        ⊥-elim $ Bool.true≢false true≡false

    f₂≢f₃ : f₂  f₃
    f₂≢f₃ =
      f₂  f₃                                →⟨ cong (_$ x) 
      false  if x  x then true else false  →⟨ flip trans (helper (x  x)) 
      false  true                           →⟨ Bool.true≢false  sym ⟩□
                                            
      where
      helper :
        (d : Dec (x  x)) 
        if d then true else false  true
      helper (yes _)  = refl _
      helper (no x≢x) = ⊥-elim $ x≢x $ refl _

    f₁≡⊎f₂≡ : (f : B  Bool)  f₁  f  f₂  f
    f₁≡⊎f₂≡ = lemma f₁ f₂ f₁≢f₂

    x≡y : x  y
    x≡y with f₁≡⊎f₂≡ f₃
     | inj₁ f₁≡f₃ = f₁≡f₃→x≡y f₁≡f₃
     | inj₂ f₂≡f₃ = ⊥-elim $ f₂≢f₃ f₂≡f₃