(Category of) Families of Sets

Stream: Is there code for X?

[Chris Henson]

Does something like this already exist?

import Mathlib
namespace CategoryTheory

structure Fam where
  X₀ : Type
  X₁ : X₀ → Type

instance : Category Fam where
  Hom B C := by
    let {X₀ := B₀, X₁ := B₁} := B
    let {X₀ := C₀, X₁ := C₁} := C
    exact Σ(f₀ : B₀ → C₀), ∀ b : B₀, B₁ b → C₁ (f₀ b)
  id X := by exact ⟨id, fun _ => id⟩
  comp := by simp; aesop_cat

[nrs]

this looks like PFunctor

[Chris Henson]

You're right, thanks!