{- Basic theory about transport:

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

{-# OPTIONS --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

subst⁻-filler :  { ℓ'} {A : Type } {x y : A} (B : A  Type ℓ') (p : x  y) (b : B y)
   PathP  i  B (p (~ i))) b (subst⁻ B p b)
subst⁻-filler B p = subst-filler B (sym p)

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)

subst⁻Subst :  { ℓ'} {A : Type } {x y : A} (B : A  Type ℓ') (p : x  y)
               (u : B x)  subst⁻ B p (subst B p u)  u
subst⁻Subst {x = x} {y = y} B p u = transport⁻Transport {A = B x} {B = B y} (cong B p) u

substSubst⁻ :  { ℓ'} {A : Type } {x y : A} (B : A  Type ℓ') (p : x  y)
               (v : B y)  subst B p (subst⁻ B p v)  v
substSubst⁻ {x = x} {y = y} B p v = transportTransport⁻ {A = B x} {B = B y} (cong B p) v

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 (pathToEquiv P)  P
uaTransportη P i j
  = Glue (P i1) λ where
      (j = i0)  P i0 , pathToEquiv 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 =
     j  λ
      { (i = i0)  retEq univalence p j
      ; (i = i1)  retEq univalence q j
    (invEq univalence ((λ a  α i a) , t i))
  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)

-- transporting along a composite path is equivalent to transporting twice
transportComposite :  {} {A B C : Type } (p : A  B) (q : B  C) (x : A)
                  transport (p  q) x  transport q (transport p x)
transportComposite = substComposite  D  D)

-- substitution commutes with morphisms in slices
substCommSlice :  { ℓ' ℓ''} {A : Type }
                    (B : A  Type ℓ') (C : A  Type ℓ'')
                    (F :  a  B a  C a)
                    {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 a =
  transport-fillerExt⁻ (cong C p) a (F _ (transport-fillerExt (cong B p) a Bx))

constSubstCommSlice :  { ℓ' ℓ''} {A : Type }
                    (B : A  Type ℓ')
                    (C : Type ℓ'')
                    (F :  a  B a  C)
                    {x y : A} (p : x  y) (u : B x)
                     (F x u)  F y (subst B p u)
constSubstCommSlice B C F p Bx = (sym (transportRefl (F _ Bx))  substCommSlice B  _  C) F p 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)))

-- substition over families of paths
-- theorem 2.11.3 in The Book
substInPaths :  {} {A B : Type } {a a' : A}
                  (f g : A  B)  (p : a  a') (q : f a  g a)
                  subst  x  f x  g x) p q  sym (cong f p)  q  cong g p
substInPaths {a = a} f g p q =
  J  x p'  (subst  y  f y  g y) p' q)  (sym (cong f p')  q  cong g p'))
    p=refl p
    p=refl : subst  y  f y  g y) refl q
            refl  q  refl
    p=refl = subst  y  f y  g y) refl q
           ≡⟨ substRefl {B =  y  f y  g y)} q  q
           ≡⟨ (rUnit q)  lUnit (q  refl)  refl  q  refl 

flipTransport :  {} {A : I  Type } {x : A i0} {y : A i1}
   x  transport⁻  i  A i) y
   transport  i  A i) x  y
flipTransport {A = A} {y = y} p =
  cong (transport  i  A i)) p  transportTransport⁻  i  A i) y

-- special cases of substInPaths from lemma 2.11.2 in The Book
module _ { : Level} {A : Type } {a x1 x2 : A} (p : x1  x2) where
  substInPathsL : (q : a  x1)  subst  x  a  x) p q  q  p
  substInPathsL q = subst  x  a  x) p q
    ≡⟨ substInPaths  _  a)  x  x) p q 
      sym (cong  _  a) p)  q  cong  x  x) p
    ≡⟨ assoc  _  a) q p 
      (refl  q)  p
    ≡⟨ cong (_∙ p) (sym (lUnit q))  q  p 

  substInPathsR : (q : x1  a)  subst  x  x  a) p q  sym p  q
  substInPathsR q = subst  x  x  a) p q
    ≡⟨ substInPaths  x  x)  _  a) p q 
      sym (cong  x  x) p)  q  cong  _  a) p
    ≡⟨ assoc (sym p) q refl 
      (sym p  q)  refl
    ≡⟨ sym (rUnit (sym p  q)) sym p  q