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