{- Basic theory about transport:

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

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

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv

-- 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))

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

transportTransport⁻ :  {} {A B : Type }  (p : A  B)  (b : B) 
                        transport p (transport⁻ p b)  b
transportTransport⁻ p b j =
  transp  i  p (i  j)) j (transp  i  p (~ i  j)) 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  x  transp  j  p (i  j)) (~ i) x)) (idIsEquiv A)

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