Linear Polynomial Functor

A linear polynomial functor is an Indexed Polynomial Functor $I\leftarrow X\xrightarrow{mathrm{id}{ifx..lse\par i}}X\to J$ where the middle leg is the identity map. Alternatively, a linear polynomial functor is just a Span.

As a container

Typically, we represent linear polynomial functors as half-indexed, half fibred.

record Linear (A B : Type) : Type where
  field
    Pos : B → Type
    ix : ∀ (b : B) → Pos b → A

The interpretation of a linear polynomial as a Functor does not involve any $\Pi$, as the type of directions is morally the unit type.

instance
  Linear-⟦⟧ : ⟦⟧-notation (Linear A B)
  Linear-⟦⟧ .⟦⟧-notation.lvl = lzero
  Linear-⟦⟧ {A = A} {B = B} .⟦⟧-notation.Sem = (A → Type) → (B → Type)
  ⟦⟧-notation.⟦ Linear-⟦⟧ ⟧ P X b = Σ[ p ∈ P .Pos b ] X (P .ix b p)

The least fixpoints of linear polynomials are not very useful, as you always have a direction to move in. From the datatype perspective, this means that you always have a single recursive occurance. However, the greatest fixpoints are still interesting:

record Cofix (P : Linear A A) (a : A) : Type where
  coinductive
  field
    pos : P .Pos a
    next : Cofix P (P .ix a pos)

These are a sort of dependent infinite stream, where the indexing scheme tells you what sort of element you need to produce next.