module SOAS.Families.Core {T : Set} where
open import SOAS.Common
open import SOAS.Context {T}
open import SOAS.Sorting {T}
Family : Set₁
Family = Ctx → Set
_⇾_ : Family → Family → Set
X ⇾ Y = ∀{Γ : Ctx} → X Γ → Y Γ
infixr 10 _⇾_
𝔽amilies : Category 1ℓ 0ℓ 0ℓ
𝔽amilies = categoryHelper record
{ Obj = Family
; _⇒_ = _⇾_
; _≈_ = λ {X}{Y} f g → ∀{Γ : Ctx}{x : X Γ} → f x ≡ g x
; id = id
; _∘_ = λ g f → g ∘ f
; assoc = refl
; identityˡ = refl
; identityʳ = refl
; equiv = record { refl = refl ; sym = λ p → sym p ; trans = λ p q → trans p q }
; ∘-resp-≈ = λ where {f = f} p q → trans (cong f q) p
}
module 𝔽am = Category 𝔽amilies
𝔽amiliesₛ : Category 1ℓ 0ℓ 0ℓ
𝔽amiliesₛ = 𝕊orted 𝔽amilies
module 𝔽amₛ = Category 𝔽amiliesₛ
Familyₛ : Set₁
Familyₛ = 𝔽amₛ.Obj
_⇾̣_ : Familyₛ → Familyₛ → Set
_⇾̣_ = 𝔽amₛ._⇒_
infixr 10 _⇾̣_
∀[_] : Familyₛ → Family
∀[ 𝒳 ] Γ = {τ : T} → 𝒳 τ Γ
_⇾̣₂_ : (Familyₛ → Familyₛ) → (Familyₛ → Familyₛ) → Set₁
(𝓧 ⇾̣₂ 𝓨) = {𝒵 : Familyₛ} → 𝓧 𝒵 ⇾̣ 𝓨 𝒵