{-

Basic properties about Σ-types

- Action of Σ on functions ([map-fst], [map-snd])
- Characterization of equality in Σ-types using dependent paths ([ΣPath{Iso,≃,≡}PathΣ], [Σ≡Prop])
- Proof that discrete types are closed under Σ ([discreteΣ])
- Commutativity and associativity ([Σ-swap-*, Σ-assoc-*])
- Distributivity of Π over Σ ([Σ-Π-*])
- Action of Σ on isomorphisms, equivalences, and paths ([Σ-cong-fst], [Σ-cong-snd], ...)
- Characterization of equality in Σ-types using transport ([ΣPathTransport{≃,≡}PathΣ])
- Σ with a contractible base is its fiber ([Σ-contractFst, ΣUnit])

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Sigma.Properties where

open import Cubical.Data.Sigma.Base

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Path
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Relation.Nullary
open import Cubical.Data.Unit.Base

open Iso

private
  variable
    ℓ ℓ' : Level
    A A' : Type ℓ
    B B' : (a : A) → Type ℓ
    C : (a : A) (b : B a) → Type ℓ

map-fst : {B : Type ℓ} → (f : A → A') → A × B → A' × B
map-fst f (a , b) = (f a , b)

map-snd : (∀ {a} → B a → B' a) → Σ A B → Σ A B'
map-snd f (a , b) = (a , f b)

map-× : {B : Type ℓ} {B' : Type ℓ'} → (A → A') → (B → B') → A × B → A' × B'
map-× f g (a , b) = (f a , g b)

≡-× : {A : Type ℓ} {B : Type ℓ'} {x y : A × B} → fst x ≡ fst y → snd x ≡ snd y → x ≡ y
≡-× p q i = (p i) , (q i)


-- Characterization of paths in Σ using dependent paths

module _ {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ'}
  {x : Σ (A i0) (B i0)} {y : Σ (A i1) (B i1)}
  where

  ΣPathP : Σ[ p ∈ PathP A (fst x) (fst y) ] PathP (λ i → B i (p i)) (snd x) (snd y)
    → PathP (λ i → Σ (A i) (B i)) x y
  ΣPathP eq i = fst eq i , snd eq i

  ΣPathIsoPathΣ : Iso (Σ[ p ∈ PathP A (fst x) (fst y) ] (PathP (λ i → B i (p i)) (snd x) (snd y)))
                      (PathP (λ i → Σ (A i) (B i)) x y)
  fun ΣPathIsoPathΣ        = ΣPathP
  inv ΣPathIsoPathΣ eq     = (λ i → fst (eq i)) , (λ i → snd (eq i))
  rightInv ΣPathIsoPathΣ _ = refl
  leftInv ΣPathIsoPathΣ _  = refl

  ΣPath≃PathΣ : (Σ[ p ∈ PathP A (fst x) (fst y) ] (PathP (λ i → B i (p i)) (snd x) (snd y)))
              ≃ (PathP (λ i → Σ (A i) (B i)) x y)
  ΣPath≃PathΣ = isoToEquiv ΣPathIsoPathΣ

  ΣPath≡PathΣ : (Σ[ p ∈ PathP A (fst x) (fst y) ] (PathP (λ i → B i (p i)) (snd x) (snd y)))
              ≡ (PathP (λ i → Σ (A i) (B i)) x y)
  ΣPath≡PathΣ = ua ΣPath≃PathΣ

Σ≡Prop : ((x : A) → isProp (B x)) → {u v : Σ A B}
       → (p : u .fst ≡ v .fst) → u ≡ v
Σ≡Prop pB {u} {v} p i = (p i) , isProp→PathP (λ i → pB (p i)) (u .snd) (v .snd) i

-- Characterization of dependent paths in Σ

module _ {A : I → Type ℓ} {B : (i : I) → (a : A i) → Type ℓ'}
  {x : Σ (A i0) (B i0)} {y : Σ (A i1) (B i1)}
  where

  ΣPathPIsoPathPΣ :
    Iso (Σ[ p ∈ PathP A (x .fst) (y .fst) ] PathP (λ i → B i (p i)) (x .snd) (y .snd))
        (PathP (λ i → Σ (A i) (B i)) x y)
  ΣPathPIsoPathPΣ .fun (p , q) i = p i , q i
  ΣPathPIsoPathPΣ .inv pq .fst i = pq i .fst
  ΣPathPIsoPathPΣ .inv pq .snd i = pq i .snd
  ΣPathPIsoPathPΣ .rightInv _ = refl
  ΣPathPIsoPathPΣ .leftInv _ = refl

  ΣPathP≃PathPΣ = isoToEquiv ΣPathPIsoPathPΣ

  ΣPathP≡PathPΣ = ua ΣPathP≃PathPΣ

-- Σ of discrete types

discreteΣ : Discrete A → ((a : A) → Discrete (B a)) → Discrete (Σ A B)
discreteΣ {B = B} Adis Bdis (a0 , b0) (a1 , b1) = discreteΣ' (Adis a0 a1)
  where
    discreteΣ' : Dec (a0 ≡ a1) → Dec ((a0 , b0) ≡ (a1 , b1))
    discreteΣ' (yes p) = J (λ a1 p → ∀ b1 → Dec ((a0 , b0) ≡ (a1 , b1))) (discreteΣ'') p b1
      where
        discreteΣ'' : (b1 : B a0) → Dec ((a0 , b0) ≡ (a0 , b1))
        discreteΣ'' b1 with Bdis a0 b0 b1
        ... | (yes q) = yes (transport ΣPath≡PathΣ (refl , q))
        ... | (no ¬q) = no (λ r → ¬q (subst (λ X → PathP (λ i → B (X i)) b0 b1) (Discrete→isSet Adis a0 a0 (cong fst r) refl) (cong snd r)))
    discreteΣ' (no ¬p) = no (λ r → ¬p (cong fst r))

Σ-swap-Iso : Iso (A × A') (A' × A)
fun Σ-swap-Iso (x , y) = (y , x)
inv Σ-swap-Iso (x , y) = (y , x)
rightInv Σ-swap-Iso _ = refl
leftInv Σ-swap-Iso _  = refl

Σ-swap-≃ : A × A' ≃ A' × A
Σ-swap-≃ = isoToEquiv Σ-swap-Iso

Σ-assoc-Iso : Iso (Σ[ (a , b) ∈ Σ A B ] C a b) (Σ[ a ∈ A ] Σ[ b ∈ B a ] C a b)
fun Σ-assoc-Iso ((x , y) , z) = (x , (y , z))
inv Σ-assoc-Iso (x , (y , z)) = ((x , y) , z)
rightInv Σ-assoc-Iso _ = refl
leftInv Σ-assoc-Iso _  = refl

Σ-assoc-≃ : (Σ[ (a , b) ∈ Σ A B ] C a b) ≃ (Σ[ a ∈ A ] Σ[ b ∈ B a ] C a b)
Σ-assoc-≃ = isoToEquiv Σ-assoc-Iso

Σ-Π-Iso : Iso ((a : A) → Σ[ b ∈ B a ] C a b) (Σ[ f ∈ ((a : A) → B a) ] ∀ a → C a (f a))
fun Σ-Π-Iso f         = (fst ∘ f , snd ∘ f)
inv Σ-Π-Iso (f , g) x = (f x , g x)
rightInv Σ-Π-Iso _    = refl
leftInv Σ-Π-Iso _     = refl

Σ-Π-≃ : ((a : A) → Σ[ b ∈ B a ] C a b) ≃ (Σ[ f ∈ ((a : A) → B a) ] ∀ a → C a (f a))
Σ-Π-≃ = isoToEquiv Σ-Π-Iso

Σ-cong-iso-fst : (isom : Iso A A') → Iso (Σ A (B ∘ fun isom)) (Σ A' B)
fun (Σ-cong-iso-fst isom) x = fun isom (x .fst) , x .snd
inv (Σ-cong-iso-fst {B = B} isom) x = inv isom (x .fst) , subst B (sym (ε (x .fst))) (x .snd)
  where
  ε = isHAEquiv.ret (snd (iso→HAEquiv isom))
rightInv (Σ-cong-iso-fst {B = B} isom) (x , y) = ΣPathP (ε x , toPathP goal)
  where
  ε = isHAEquiv.ret (snd (iso→HAEquiv isom))
  goal : subst B (ε x) (subst B (sym (ε x)) y) ≡ y
  goal = sym (substComposite B (sym (ε x)) (ε x) y)
      ∙∙ cong (λ x → subst B x y) (lCancel (ε x))
      ∙∙ substRefl {B = B} y
leftInv (Σ-cong-iso-fst {A = A} {B = B} isom@(iso f _ _ η)) (x , y) = ΣPathP (η x , toPathP goal)
  where
  ε = isHAEquiv.ret (snd (iso→HAEquiv isom))
  γ = isHAEquiv.com (snd (iso→HAEquiv isom))

  lem : (x : A) → sym (ε (f x)) ∙ cong f (η x) ≡ refl
  lem x = cong (λ a → sym (ε (f x)) ∙ a) (γ x) ∙ lCancel (ε (f x))

  goal : subst B (cong f (η x)) (subst B (sym (ε (f x))) y) ≡ y
  goal = sym (substComposite B (sym (ε (f x))) (cong f (η x)) y)
      ∙∙ cong (λ a → subst B a y) (lem x)
      ∙∙ substRefl {B = B} y

Σ-cong-equiv-fst : (e : A ≃ A') → Σ A (B ∘ equivFun e) ≃ Σ A' B
Σ-cong-equiv-fst e = isoToEquiv (Σ-cong-iso-fst (equivToIso e))

Σ-cong-fst : (p : A ≡ A') → Σ A (B ∘ transport p) ≡ Σ A' B
Σ-cong-fst {B = B} p i = Σ (p i) (B ∘ transp (λ j → p (i ∨ j)) i)

Σ-cong-iso-snd : ((x : A) → Iso (B x) (B' x)) → Iso (Σ A B) (Σ A B')
fun (Σ-cong-iso-snd isom) (x , y) = x , fun (isom x) y
inv (Σ-cong-iso-snd isom) (x , y') = x , inv (isom x) y'
rightInv (Σ-cong-iso-snd isom) (x , y) = ΣPathP (refl , rightInv (isom x) y)
leftInv (Σ-cong-iso-snd isom) (x , y') = ΣPathP (refl , leftInv (isom x) y')

Σ-cong-equiv-snd : (∀ a → B a ≃ B' a) → Σ A B ≃ Σ A B'
Σ-cong-equiv-snd h = isoToEquiv (Σ-cong-iso-snd (equivToIso ∘ h))

Σ-cong-snd : ((x : A) → B x ≡ B' x) → Σ A B ≡ Σ A B'
Σ-cong-snd {A = A} p i = Σ[ x ∈ A ] (p x i)

Σ-cong-iso : (isom : Iso A A')
           → ((x : A) → Iso (B x) (B' (fun isom x)))
           → Iso (Σ A B) (Σ A' B')
Σ-cong-iso isom isom' = compIso (Σ-cong-iso-snd isom') (Σ-cong-iso-fst isom)

Σ-cong-equiv : (e : A ≃ A')
             → ((x : A) → B x ≃ B' (equivFun e x))
             → Σ A B ≃ Σ A' B'
Σ-cong-equiv e e' = isoToEquiv (Σ-cong-iso (equivToIso e) (equivToIso ∘ e'))

Σ-cong' : (p : A ≡ A') → PathP (λ i → p i → Type ℓ') B B' → Σ A B ≡ Σ A' B'
Σ-cong' p p' = cong₂ (λ (A : Type _) (B : A → Type _) → Σ A B) p p'

-- Alternative version for path in Σ-types, as in the HoTT book

ΣPathTransport : (a b : Σ A B) → Type _
ΣPathTransport {B = B} a b = Σ[ p ∈ (fst a ≡ fst b) ] transport (λ i → B (p i)) (snd a) ≡ snd b

ΣPathTransport≃PathΣ : (a b : Σ A B) → ΣPathTransport a b ≃ (a ≡ b)
ΣPathTransport≃PathΣ {B = B} a b =
  compEquiv
    (isoToEquiv (Σ-cong-iso-snd λ p → invIso (equivToIso (PathP≃Path (λ i → B (p i)) _ _))))
    ΣPath≃PathΣ

ΣPathTransport→PathΣ : (a b : Σ A B) → ΣPathTransport a b → (a ≡ b)
ΣPathTransport→PathΣ a b = ΣPathTransport≃PathΣ a b .fst

PathΣ→ΣPathTransport : (a b : Σ A B) → (a ≡ b) → ΣPathTransport a b
PathΣ→ΣPathTransport a b = invEq (ΣPathTransport≃PathΣ a b)

ΣPathTransport≡PathΣ : (a b : Σ A B) → ΣPathTransport a b ≡ (a ≡ b)
ΣPathTransport≡PathΣ a b = ua (ΣPathTransport≃PathΣ a b)

Σ-contractFst : (c : isContr A) → Σ A B ≃ B (c .fst)
Σ-contractFst {B = B} c = isoToEquiv isom
  where
  isom : Iso _ _
  isom .fun (a , b) = subst B (sym (c .snd a)) b
  isom .inv b = (c .fst , b)
  isom .rightInv b =
    cong (λ p → subst B p b) (isProp→isSet (isContr→isProp c) _ _ _ _) ∙ transportRefl _
  isom .leftInv (a , b) =
    ΣPathTransport≃PathΣ _ _ .fst (c .snd a , transportTransport⁻ (cong B (c .snd a)) _)

-- a special case of the above
ΣUnit : ∀ {ℓ} (A : Unit → Type ℓ) → Σ Unit A ≃ A tt
ΣUnit A = isoToEquiv (iso snd (λ { x → (tt , x) }) (λ _ → refl) (λ _ → refl))

Σ-contractSnd : ((a : A) → isContr (B a)) → Σ A B ≃ A
Σ-contractSnd c = isoToEquiv isom
  where
  isom : Iso _ _
  isom .fun = fst
  isom .inv a = a , c a .fst
  isom .rightInv _ = refl
  isom .leftInv (a , b) = cong (a ,_) (c a .snd b)


≃-× : ∀ {ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} {D : Type ℓ'''} → A ≃ C → B ≃ D → A × B ≃ C × D
≃-× eq1 eq2 =
    map-× (fst eq1) (fst eq2)
  , record
     { equiv-proof
       = λ {(c , d) → ((eq1⁻ c .fst .fst
                        , eq2⁻ d .fst .fst)
                          , ≡-× (eq1⁻ c .fst .snd)
                                (eq2⁻ d .fst .snd))
                     , λ {((a , b) , p) → ΣPathP (≡-× (cong fst (eq1⁻ c .snd (a , cong fst p)))
                                                       (cong fst (eq2⁻ d .snd (b , cong snd p)))
                                                , λ i → ≡-× (snd ((eq1⁻ c .snd (a , cong fst p)) i))
                                                             (snd ((eq2⁻ d .snd (b , cong snd p)) i)))}}}
  where
  eq1⁻ = equiv-proof (eq1 .snd)
  eq2⁻ = equiv-proof (eq2 .snd)

{- Some simple ismorphisms -}

prodIso : ∀ {ℓ ℓ' ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} {D : Type ℓ'''}
       → Iso A C
       → Iso B D
       → Iso (A × B) (C × D)
Iso.fun (prodIso iAC iBD) (a , b) = (Iso.fun iAC a) , Iso.fun iBD b
Iso.inv (prodIso iAC iBD) (c , d) = (Iso.inv iAC c) , Iso.inv iBD d
Iso.rightInv (prodIso iAC iBD) (c , d) = ΣPathP ((Iso.rightInv iAC c) , (Iso.rightInv iBD d))
Iso.leftInv (prodIso iAC iBD) (a , b) = ΣPathP ((Iso.leftInv iAC a) , (Iso.leftInv iBD b))

toProdIso : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
         → Iso (A → B × C) ((A → B) × (A → C))
Iso.fun toProdIso = λ f → (λ a → fst (f a)) , (λ a → snd (f a))
Iso.inv toProdIso (f , g) = λ a → (f a) , (g a)
Iso.rightInv toProdIso (f , g) = refl
Iso.leftInv toProdIso b = funExt λ _ → refl

curryIso : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
         → Iso (A × B → C) (A → B → C)
Iso.fun curryIso f a b = f (a , b)
Iso.inv curryIso f a = f (fst a) (snd a)
Iso.rightInv curryIso a = refl
Iso.leftInv curryIso f = funExt λ _ → refl