{-# OPTIONS --without-K #-}

module agda.exp-path where

open import agda.prelude
open import agda.postulates

----------------------------------------------------------------------
-- The path functor given by exponentiating by 𝕀
----------------------------------------------------------------------
℘ :
  {l : Level}
  (Γ : Set l)
  → ---------
  Set l
℘ Γ = 𝕀 → Γ

℘` :
  {l m : Level}
  {Γ : Set l}
  {Δ : Set m}
  (γ : Δ → Γ)
  → -----------
  ℘ Δ → ℘ Γ
℘` γ p i = γ (p i)

℘`comp :
  {l m n : Level}
  {Γ : Set l}
  {Δ : Set m}
  {Θ : Set n}
  (γ : Δ → Γ)
  (σ : Θ → Δ)
  (p : ℘ Θ)
  → -----------
  ℘` γ (℘` σ p) ≡ ℘` (γ ∘ σ) p
℘`comp _ _ _ = refl