Chuangjie Xu, 9 Sep 2014

\begin{code}

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

module CwF.Space.Preliminaries where

open import Preliminaries.SetsAndFunctions hiding (_+_)
open import Preliminaries.NaturalNumber
open import Preliminaries.Boolean
open import Preliminaries.Sequence

\end{code}

Preliminaries

\begin{code}

apd : {X : Set} {Y : X → Set} {x₀ x₁ : X}
    → (f : (x : X) → Y x) → (p : x₀ ≡ x₁) → transport Y p (f x₀) ≡ f x₁
apd f refl = refl

transport-∘ : {Γ : Set} {Δ : Set} {δ₀ δ₁ : Δ} →
              (A : Γ → Set) (σ : Δ → Γ) (p : δ₀ ≡ δ₁) {a : A(σ δ₀)}
            → transport (A ∘ σ) p a ≡ transport A (ap σ p) a
transport-∘ A σ refl = refl

▢ : {X : Set} → (₂ → ₂ℕ → X) → ₂ℕ → X
▢ ρ α = ρ (α 0) (α ∘ succ)

▣ : {X : Set} {ρ : ₂ → ₂ℕ → X} → (A : X → Set)
  → ((i : ₂) → (α : ₂ℕ) → A(ρ i α)) → (α : ₂ℕ) → A(▢ ρ α)
▣ A ζ α = ζ (α 0) (α ∘ succ)

\end{code}