Ornaments

An Ornament is an alternative encoding of a cartesian lift in the fibration $\mathrm{Poly}\to\mathrm{Sets}$ (See Cartesian Morphism of Polynomial Functors for more details).

Via Display

Idea: Ornaments are displayed Polynomial Functors with a Contractible space of fibres. EG:

record Poly (ℓ ℓ' : Level) : Type (lsuc (ℓ ⊔ ℓ')) where
  no-eta-equality
  field
    Base : Type ℓ
    Fib : Base → Type ℓ'


record Ornament (P : Poly ℓp ℓp') (ℓo : Level) : Type (ℓp ⊔ lsuc ℓo) where
  field
    Orn : P .Base → Type ℓo

∫ᵒ : (P : Poly ℓp ℓp') → Ornament P ℓ → Poly (ℓp ⊔ ℓ) ℓp'
∫ᵒ P O .Base = Σ[ p ∈ P .Base ] O .Orn p
∫ᵒ P O .Fib (p , o) = P .Fib p

πᵒ : ∀ {P : Poly ℓp ℓp'} {O : Ornament P ℓ} → ∫ᵒ P O →ᵖ P
πᵒ .fwd = fst
πᵒ .bwd _ p = p