{-

Theory about path split equivalences.
They are convenient to construct localization HITs as in
(the "modalities paper")
https://arxiv.org/abs/1706.07526

- there are construction from and to equivalences ([pathSplitToEquiv] , [equivToPathSplit])
- the structure of a path split equivalence is actually a proposition ([isPropIsPathSplitEquiv])

The module starts with a couple of general facts about equivalences:

- if f is an equivalence then (cong f) is an equivalence ([equivCong])
- if f is an equivalence then pre- and postcomposition with f are equivalences ([preCompEquiv], [postCompEquiv])

(those are not in 'Equiv.agda' because they need Univalence.agda (which imports Equiv.agda))
-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.PathSplitEquiv where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Isomorphism

open import Cubical.Foundations.Equiv.Properties

record isPathSplitEquiv { ℓ'} {A : Type  } {B : Type ℓ'} (f : A  B) : Type (ℓ-max  ℓ') where
  field
    sec : hasSection f
    secCong : (x y : A)  hasSection  (p : x  y)  cong f p)

PathSplitEquiv :  { ℓ'} (A : Type  ) (B : Type ℓ')  Type (ℓ-max  ℓ')
PathSplitEquiv A B = Σ[ f  (A  B) ] isPathSplitEquiv f

open isPathSplitEquiv

idIsPathSplitEquiv :  {} {A : Type }  isPathSplitEquiv  (x : A)  x)
sec idIsPathSplitEquiv =  x  x) ,  x  refl)
secCong idIsPathSplitEquiv = λ x y   p  p) , λ p _  p

module _ { ℓ'} {A : Type } {B : Type ℓ'} where
  toIsEquiv : (f : A  B)  isPathSplitEquiv f  isEquiv f
  toIsEquiv f record { sec = sec ; secCong = secCong } =
    (isoToEquiv (iso f (fst sec) (snd sec)  x  (secCong (fst sec (f x)) x).fst (snd sec (f x))))) .snd

  sectionOfEquiv' : (f : A  B)  isEquiv f  B  A
  sectionOfEquiv' f record { equiv-proof = all-fibers-contractible } x =
    all-fibers-contractible x .fst .fst

  isSec : (f : A  B)  (pf : isEquiv f)  section f (sectionOfEquiv' f pf)
  isSec f record { equiv-proof = all-fibers-contractible } x =
    all-fibers-contractible x .fst .snd

  sectionOfEquiv : (f : A  B)  isEquiv f  hasSection f
  sectionOfEquiv f e = sectionOfEquiv' f e , isSec f e

module _ {} {A B : Type } where
  abstract
    fromIsEquiv : (f : A  B)  isEquiv f  isPathSplitEquiv f
    sec (fromIsEquiv f pf) = sectionOfEquiv' f pf , isSec f pf
    secCong (fromIsEquiv f pf) x y = sectionOfEquiv cong-f eq-cong
            where
            cong-f : x  y  f x  f y
            cong-f = λ (p : x  y)  cong f p
            eq-cong : isEquiv cong-f
            eq-cong = isEquivCong (f , pf)

  pathSplitToEquiv : PathSplitEquiv A B  A  B
  fst (pathSplitToEquiv (f , _)) = f
  snd (pathSplitToEquiv (_ , e)) = toIsEquiv _ e

  equivToPathSplit : A  B  PathSplitEquiv A B
  fst (equivToPathSplit (f , _)) = f
  snd (equivToPathSplit (_ , e)) = fromIsEquiv _ e

  equivHasUniqueSection : (f : A  B)
     isEquiv f  isContr (Σ (B  A) (section f))
  equivHasUniqueSection f eq = helper'
    where
      idB = λ (x : B)  x
      abstract
        helper : isContr (fiber  (φ : B  A)  f  φ) idB)
        helper = (equiv-proof (snd (postCompEquiv (f , eq)))) idB
      helper' : isContr (Σ[ φ  (B  A) ] ((x : B)  f (φ x)  x))
      fst helper' = (φ , λ x i  η i x)
        where φ = fst (fst helper)
              η : f  φ  idB
              η = snd (fst helper)
      (snd helper') y i = (fst (η i) , λ b j  snd (η i) j b)
        where η = (snd helper) (fst y , λ i b  snd y b i)

{-
  PathSplitEquiv is a proposition and the type
  of path split equivs is equivalent to the type of equivalences
-}
isPropIsPathSplitEquiv :  {} {A B : Type } (f : A  B)
      isProp (isPathSplitEquiv f)
isPropIsPathSplitEquiv {_} {A} {B} f
  record { sec = sec-φ ; secCong = secCong-φ }
  record { sec = sec-ψ ; secCong = secCong-ψ } i
  =
  record {
    sec = sectionsAreEqual i ;
    secCong = λ x y  congSectionsAreEqual x y (secCong-φ x y) (secCong-ψ x y) i
  }
  where
    φ' = record { sec = sec-φ ; secCong = secCong-φ }
    ψ' = record { sec = sec-ψ ; secCong = secCong-ψ }
    sectionsAreEqual : sec-φ  sec-ψ
    sectionsAreEqual = (sym (contraction sec-φ))  (contraction  sec-ψ)
      where contraction = snd (equivHasUniqueSection f (toIsEquiv f φ'))
    congSectionsAreEqual : (x y : A) (l u : hasSection  (p : x  y)  cong f p))  l  u
    congSectionsAreEqual x y l u = (sym (contraction l))  (contraction u)
      where contraction = snd (equivHasUniqueSection
                                  (p : x  y)  cong f p)
                                 (isEquivCong (pathSplitToEquiv (f , φ'))))

module _ {} {A B : Type } where
  isEquivIsPathSplitToIsEquiv : (f : A  B)  isEquiv (fromIsEquiv f)
  isEquivIsPathSplitToIsEquiv f =
    isoToIsEquiv
      (iso (fromIsEquiv f) (toIsEquiv f)  b  isPropIsPathSplitEquiv f _ _)  a  isPropIsEquiv f _ _ ))

  isEquivPathSplitToEquiv : isEquiv (pathSplitToEquiv {A = A} {B = B})
  isEquivPathSplitToEquiv =
    isoToIsEquiv
      (iso pathSplitToEquiv equivToPathSplit
         {(f , e) i  (f , isPropIsEquiv f (toIsEquiv f (fromIsEquiv f e)) e i)})
         {(f , e) i  (f , isPropIsPathSplitEquiv f (fromIsEquiv f (toIsEquiv f e)) e i)}))

  equivPathSplitToEquiv : (PathSplitEquiv A B)  (A  B)
  equivPathSplitToEquiv = (pathSplitToEquiv , isEquivPathSplitToEquiv)


secCongDep :  { ℓ' ℓ''} {A : Type } {B : A  Type ℓ'} {C : A  Type ℓ''}
              (f :  a  B a  C a) {a a' : A} (q : a  a')
              (∀ a (x y : B a)  hasSection  (p : x  y)  cong (f a) p))
              (∀ (x : B a) (y : B a')  hasSection  (p : PathP  i  B (q i)) x y)  cong₂ f q p))
secCongDep {B = B} f {a} p secCong
  = J  a' q  (x : B a) (y : B a')  hasSection  (p : PathP  i  B (q i)) x y)  cong₂ f q p))
      (secCong a) p