Chuangjie Xu 2014

\begin{code}

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

module CwF.Sheaf.Preliminaries where

open import Agda.Primitive using (Level ; lzero ; lsuc ; _⊔_)
open import Preliminaries.SetsAndFunctions hiding (_+_)

\end{code}

More preliminaries which are used when defining our sheaf model

\begin{code}

Σ! : {i j : Level}{X : Set i} → (X → Set j) → Set(i ⊔ j)
Σ! {i} {j} {X} P = Σ \(x₀ : X) → (P x₀ × (∀ x → P x → x₀ ≡ x))

IdP : {i j : Level} {A : Set i} {a₀ a₁ : A}
    → (B : A → Set j) → a₀ ≡ a₁ → B a₀ → B a₁ → Set j
IdP B p b₀ b₁ = transport B p b₀ ≡ b₁
syntax IdP B p x y = x ≈[ B , p ]≈ y

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

transport-· : {i j : Level} {A : Set i} (B : A → Set j) {x y z : A} →
              (p : x ≡ y) (q : y ≡ z) {b : B x}
            → transport B q (transport B p b) ≡ transport B (p · q) b
transport-· B refl refl = refl

transport-p⁻¹·p : {i j : Level} {A : Set i} (B : A → Set j) {x y : A} →
                  (p : x ≡ y) (b : B y)
                → transport B p (transport B (p ⁻¹) b) ≡ b
transport-p⁻¹·p B refl b = refl

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

transport-ap : {i j : Level} {Γ : Set i} {γ₀ γ₁ : Γ} →
               (A : Γ → Set j) {a : A γ₀} (p : γ₀ ≡ γ₁) →
               {f : Γ → Γ} (F : {γ : Γ} → A γ → A(f γ))
             → F (transport A p a) ≡ transport A (ap f p) (F a)
transport-ap A refl F = refl

\end{code}