{- Basic theory about transport:

- transport is invertible
- transport is an equivalence ([transportEquiv])

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.Transport where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Function using (_∘_)

-- Direct definition of transport filler, note that we have to
-- explicitly tell Agda that the type is constant (like in CHM)
transpFill :  {} {A : Type }
             (φ : I)
             (A : (i : I)  Type  [ φ   _  A) ])
             (u0 : outS (A i0))
            --------------------------------------
             PathP  i  outS (A i)) u0 (transp  i  outS (A i)) φ u0)
transpFill φ A u0 i = transp  j  outS (A (i  j))) (~ i  φ) u0

transport⁻ :  {} {A B : Type }  A  B  B  A
transport⁻ p = transport  i  p (~ i))

subst⁻ :  { ℓ'} {A : Type } {x y : A} (B : A  Type ℓ') (p : x  y)  B y  B x
subst⁻ B p pa = transport⁻  i  B (p i)) pa

transport-fillerExt :  {} {A B : Type } (p : A  B)
                     PathP  i  A  p i)  x  x) (transport p)
transport-fillerExt p i x = transport-filler p x i

transport⁻-fillerExt :  {} {A B : Type } (p : A  B)
                      PathP  i  p i  A)  x  x) (transport⁻ p)
transport⁻-fillerExt p i x = transp  j  p (i  ~ j)) (~ i) x

transport-fillerExt⁻ :  {} {A B : Type } (p : A  B)
                     PathP  i  p i  B) (transport p)  x  x)
transport-fillerExt⁻ p = symP (transport⁻-fillerExt (sym p))

transport⁻-fillerExt⁻ :  {} {A B : Type } (p : A  B)
                      PathP  i  B  p i) (transport⁻ p)  x  x)
transport⁻-fillerExt⁻ p = symP (transport-fillerExt (sym p))


transport⁻-filler :  {} {A B : Type } (p : A  B) (x : B)
                    PathP  i  p (~ i)) x (transport⁻ p x)
transport⁻-filler p x = transport-filler  i  p (~ i)) x

transport⁻Transport :  {} {A B : Type }  (p : A  B)  (a : A) 
                          transport⁻ p (transport p a)  a
transport⁻Transport p a j = transport⁻-fillerExt p (~ j) (transport-fillerExt p (~ j) a)

transportTransport⁻ :  {} {A B : Type }  (p : A  B)  (b : B) 
                        transport p (transport⁻ p b)  b
transportTransport⁻ p b j = transport-fillerExt⁻ p j (transport⁻-fillerExt⁻ p j b)

-- Transport is an equivalence
isEquivTransport :  {} {A B : Type } (p : A  B)  isEquiv (transport p)
isEquivTransport {A = A} {B = B} p =
  transport  i  isEquiv (transport-fillerExt p i)) (idIsEquiv A)

transportEquiv :  {} {A B : Type }  A  B  A  B
transportEquiv p = (transport p , isEquivTransport p)

substEquiv :  { ℓ'} {A : Type } {a a' : A} (P : A  Type ℓ') (p : a  a')  P a  P a'
substEquiv P p = (subst P p , isEquivTransport  i  P (p i)))

liftEquiv :  { ℓ'} {A B : Type } (P : Type   Type ℓ') (e : A  B)  P A  P B
liftEquiv P e = substEquiv P (ua e)

transpEquiv :  {} {A B : Type } (p : A  B)   i  p i  B
transpEquiv P i .fst = transp  j  P (i  j)) i
transpEquiv P i .snd
  = transp  k  isEquiv (transp  j  P (i  (j  k))) (i  ~ k)))
      i (idIsEquiv (P i))

uaTransportη :  {} {A B : Type } (P : A  B)  ua (transportEquiv P)  P
uaTransportη P i j
  = Glue (P i1) λ where
      (j = i0)  P i0 , transportEquiv P
      (i = i1)  P j , transpEquiv P j
      (j = i1)  P i1 , idEquiv (P i1)

pathToIso :  {} {A B : Type }  A  B  Iso A B
Iso.fun (pathToIso x) = transport x
Iso.inv (pathToIso x) = transport⁻ x
Iso.rightInv (pathToIso x) = transportTransport⁻ x
Iso.leftInv (pathToIso x) = transport⁻Transport x

isInjectiveTransport :  { : Level} {A B : Type } {p q : A  B}
   transport p  transport q  p  q
isInjectiveTransport {p = p} {q} α i =
  hcomp
     j  λ
      { (i = i0)  secEq univalence p j
      ; (i = i1)  secEq univalence q j
      })
    (invEq univalence ((λ a  α i a) , t i))
  where
  t : PathP  i  isEquiv  a  α i a)) (pathToEquiv p .snd) (pathToEquiv q .snd)
  t = isProp→PathP  i  isPropIsEquiv  a  α i a)) _ _

transportUaInv :  {} {A B : Type } (e : A  B)  transport (ua (invEquiv e))  transport (sym (ua e))
transportUaInv e = cong transport (uaInvEquiv e)
-- notice that transport (ua e) would reduce, thus an alternative definition using EquivJ can give
-- refl for the case of idEquiv:
-- transportUaInv e = EquivJ (λ _ e → transport (ua (invEquiv e)) ≡ transport (sym (ua e))) refl e

isSet-subst :  { ℓ′} {A : Type } {B : A  Type ℓ′}
                 (isSet-A : isSet A)
                  {a : A}
                 (p : a  a)  (x : B a)  subst B p x  x
isSet-subst {B = B} isSet-A p x = subst  p′  subst B p′ x  x) (isSet-A _ _ refl p) (substRefl {B = B} x)

-- substituting along a composite path is equivalent to substituting twice
substComposite :  { ℓ′} {A : Type }  (B : A  Type ℓ′)
                  {x y z : A} (p : x  y) (q : y  z) (u : B x)
                  subst B (p  q) u  subst B q (subst B p u)
substComposite B p q Bx i =
  transport (cong B (compPath-filler' p q (~ i))) (transport-fillerExt (cong B p) i Bx)

-- substitution commutes with morphisms in slices
substCommSlice :  { ℓ′} {A : Type }
                    (B C : A  Type ℓ′)
                    (F :  i  B i  C i)
                    {x y : A} (p : x  y) (u : B x)
                    subst C p (F x u)  F y (subst B p u)
substCommSlice B C F p Bx i =
  transport-fillerExt⁻ (cong C p) i (F _ (transport-fillerExt (cong B p) i Bx))

-- transporting over (λ i → B (p i) → C (p i)) divides the transport into
-- transports over (λ i → C (p i)) and (λ i → B (p (~ i)))
funTypeTransp :  { ℓ'} {A : Type } (B C : A  Type ℓ') {x y : A} (p : x  y) (f : B x  C x)
          PathP  i  B (p i)  C (p i)) f (subst C p  f  subst B (sym p))
funTypeTransp B C {x = x} p f i b =
  transp  j  C (p (j  i))) (~ i) (f (transp  j  B (p (i  ~ j))) (~ i) b))

-- transports between loop spaces preserve path composition
overPathFunct :  {} {A : Type } {x y : A} (p q : x  x) (P : x  y)
            transport  i  P i  P i) (p  q)
             transport  i  P i  P i) p  transport  i  P i  P i) q
overPathFunct p q =
  J  y P  transport  i  P i  P i) (p  q)  transport  i  P i  P i) p  transport  i  P i  P i) q)
    (transportRefl (p  q)  cong₂ _∙_ (sym (transportRefl p)) (sym (transportRefl q)))