Chuangjie Xu, November 2014

\begin{code}

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

module CwF.Sets.Base where

open import Preliminaries.SetsAndFunctions

\end{code}

Contexts and substitutions

\begin{code}

Cxt : Set₁
Cxt = Set

Sub : Cxt → Cxt → Set
Sub Δ Γ = Δ → Γ

Ι : {Γ : Cxt} → Sub Γ Γ
Ι γ = γ

ε : Cxt
ε = ⒈

\end{code}

Computational rules

\begin{code}

-- 1 ∘ σ = σ
EqCat₀ : ∀{Γ Δ : Cxt}{σ : Sub Δ Γ}
       → Ι ∘ σ ≡ σ
EqCat₀ = refl

-- σ ∘ 1 = σ
EqCat₁ : ∀{Γ Δ : Cxt}{σ : Sub Δ Γ}
       → σ ∘ Ι ≡ σ
EqCat₁ = refl

-- (σ ∘ τ) ∘ ν = σ ∘ (τ ∘ ν)
EqCat₂ : ∀{Γ Δ Θ Ξ : Cxt}{σ : Sub Δ Γ}{τ : Sub Θ Δ}{ν : Sub Ξ Θ}
       → (σ ∘ τ) ∘ ν ≡ σ ∘ (τ ∘ ν)
EqCat₂ = refl

\end{code}