Later on families

Definition. Later on families

Conjugation with the adjunction between presheaves and families $𝑈 ⊣ Cofree$ lets us induce a later construction on families from the one on presheaves,

⊳_{Fam} = 𝑈 \circ ⊳ \circ Cofree : Fam (𝒞︀) \to Fam (𝒞︀) .

Concretely, later on families evaluates to

⊳_{Fam} 𝐴 (𝑥) ≅ \prod_{𝑦 ≺ 𝑥} \prod_{𝑓 : 𝑦 \to 𝑥} 𝐴 (𝑦)