the fixed point of a lax double endofunctor on Span ought to be a category. I can't figure it out though as I get trapped in setoid hell and stuff.

fixed.v

Set Primitive Projections.

Require Import Coq.Unicode.Utf8.

Reserved Infix "∈" (at level 90, right associativity).

Variant fiber {A B} (f: A → B): B → Type :=
  | fiber_intro x: fiber f (f x).
Arguments fiber_intro {A B f}.

Notation "x ∈ X" := (fiber X x).

Definition witness {A B} {X: A → B} {x} (p: x ∈ X): A :=
  match p with
  | fiber_intro w => w
  end.

Definition p2 {A B} {X: A → B} {x} (p: x ∈ X): X (witness p) = x :=
  match p with
  | fiber_intro _ => eq_refl
  end.

Module Span.
  Record t (A B: Type) := {
      s: Type ;
      π1: s → A ;
      π2: s → B ;
    }.
  Arguments s {A B}.
  Arguments π1 {A B}.
  Arguments π2 {A B}.

  Variant ext {A B} (P: t A B): A → B → Type :=
    | ext_intro x: ext P (π1 P x) (π2 P x).

  Definition id A: t A A :=
    {|
      s := A ;
      π1 x := x ;
      π2 x := x ;
    |}.

  Definition compose {A B C} (P: t B C) (Q: t A B): t A C :=
    {|
      s := { x & π1 P x ∈ π2 Q } ;
      π2 xy := π2 P (projT1 xy) ;
      π1 xy := π1 Q (witness (projT2 xy)) ;
    |}.
End Span.

Module Data.
  Module Poly.
    Record t := {
        s: Type ;
        π: s → Type ;
      }.
  End Poly.

  Module μ.
    Inductive t (P: Poly.t) :=
    | sup (g: Poly.s P) (f: Poly.π P g → t P).

    Definition tag {P} (x: t P): Poly.s P :=
      match x with
      | sup _ t _ => t
      end.

    Definition field {P} (x: t P): Poly.π P (tag x) → t P :=
      match x with
      | sup _ _ f => f
      end.
  End μ.
End Data.

Module Category.
  Class t (Obj: Type) := {
      Mor: Obj → Obj → Type ;

      id A: Mor A A ;
      compose {A B C} (f: Mor B C) (g: Mor A B): Mor A C ;

      compose_id_l {A B} (f: Mor A B): compose (id _) f = f ;
      compose_id_r {A B} (f: Mor A B): compose f (id _) = f ;
      compose_assoc {A B C D} (f: Mor C D) (g: Mor B C) (h: Mor A B): compose f (compose g h) = compose (compose f g) h ;
    }.

  Module Import CategoryNotations.
    Infix "∘" := compose (at level 30).
  End CategoryNotations.

  Module Poly.
    Record t := {
        data: Data.Poly.t ;
        Category :> Category.t (Data.Poly.s data) ;
        map {A B: Data.Poly.s data}: Mor A B → Span.t (Data.Poly.π data A) (Data.Poly.π data B) ;

        map_id {A} x: Span.π1 (map (id A)) x = Span.π2 (map (id A)) x ;
        map_compose {A B C} (f: Mor B C) (g: Mor A B): Span.s (Span.compose (map f) (map g)) ;
        map_compose_π1 {A B C} (f: Mor B C) (g: Mor A B) x:
             Span.π1 (map (f ∘ g)) x = Span.π1 _ (map_compose f g) ;
        map_compose_π2 {A B C} (f: Mor B C) (g: Mor A B) x:
             Span.π2 (map (f ∘ g)) x = Span.π2 _ (map_compose f g) ;
      }.
    Arguments map {_ A B}.
    Arguments map_id {_ _}.
    Arguments map_compose {_ _ _ _}.
    Arguments map_compose_π1 {_ _ _ _}.
    Arguments map_compose_π2 {_ _ _ _}.
  End Poly.

  Module μ.
    Inductive t {P: Poly.t} (A B: Data.μ.t (Poly.data P)) :=
    | sup
        (g: @Mor _ (Poly.Category P) (Data.μ.tag A) (Data.μ.tag B))
        (f: ∀ x, t (Data.μ.field A (Span.π1 (Poly.map g) x))
                   (Data.μ.field B (Span.π2 (Poly.map g) x))).
    Arguments sup {P A B}.

    Definition tag {P} {A B: Data.μ.t (Poly.data P)} (x: t A B): Mor _ _ :=
      match x with
      | sup g _ => g
      end.

    Definition field {P} {A B: Data.μ.t (Poly.data P)}
      (x: t A B): ∀ y,
        t
          (Data.μ.field A (Span.π1 (Poly.map (tag x)) y))
          (Data.μ.field B (Span.π2 (Poly.map (tag x)) y)) :=
      match x with
      | sup _ f => f
      end.
    Arguments field {P A B}.

    Notation "s ▹ x , P" := (sup s (fun x => P)) (at level 100).

    Fixpoint id {P} (A: Data.μ.t (Poly.data P)) {struct A}: t A A :=
      Category.id _ ▹ x,
        match Poly.map_id x with
        | eq_refl => id _
        end.

    Definition compose_π1 {P} {A B C: Data.μ.t (Poly.data P)} (f: t B C) (g: t A B)
      (x : Span.s (Poly.map (tag f ∘ tag g))):
      t (Data.μ.field B (Span.π1 (Poly.map (tag f)) (projT1 (Poly.map_compose (tag f) (tag g)))))
        (Data.μ.field C (Span.π2 (Poly.map (tag f ∘ tag g)) x)).
    Proof.
      rewrite (Poly.map_compose_π2 (tag f) (tag g) x).
      exact (field f (projT1 (Poly.map_compose (tag f) (tag g)))).
    Defined.

    Definition compose_π2 {P} {A B C: Data.μ.t (Poly.data P)} (f: t B C) (g: t A B)
      (x : Span.s (Poly.map (tag f ∘ tag g))):
      t (Data.μ.field A (Span.π1 (Poly.map (tag f ∘ tag g)) x))
        (Data.μ.field B (Span.π2 (Poly.map (tag g)) (witness (projT2 (Poly.map_compose (tag f) (tag g)))))).
    Proof.
      rewrite (Poly.map_compose_π1 (tag f) (tag g) x).
      exact (field g (witness (projT2 (Poly.map_compose (tag f) (tag g))))).
    Defined.

    Definition compose_π2' {P} {A B C: Data.μ.t (Poly.data P)} (f: t B C) (g: t A B)
      (x : Span.s (Poly.map (tag f ∘ tag g))):
      t (Data.μ.field A (Span.π1 (Poly.map (tag f ∘ tag g)) x))
        (Data.μ.field B (Span.π1 (Poly.map (tag f)) (projT1 (Poly.map_compose (tag f) (tag g))))).
    Proof.
      assert (g' := compose_π2 f g x).
      cbn in *.
      destruct (Poly.map_compose (tag f) (tag g)).
      cbn in *.
      destruct f0.
      exact g'.
    Defined.

    Fixpoint compose {P} {A B C: Data.μ.t (Poly.data P)} (f: t B C) (g: t A B) {struct B}: t A C :=
      tag f ∘ tag g ▹ x,
        compose (compose_π1 f g x) (compose_π2' f g x).

    Fixpoint compose_id_l {P A B} {f: @μ.t P A B} {struct B}: μ.compose (μ.id _) f = f.
    Proof.
      destruct B, f.
      cbn in *.
    Admitted.

    Lemma compose_id_r {P A B} {f: @μ.t P A B}: μ.compose f (μ.id _) = f.
    Admitted.

    Lemma compose_assoc {P A B C D} {f: @μ.t P C D} (g: @μ.t P B C) (h: @μ.t P A B): μ.compose f (μ.compose g h) = μ.compose (μ.compose f g) h.
    Admitted.
  End μ.

  #[export]
    Instance μ (P: Poly.t): Category.t (Data.μ.t (Poly.data P)) := {
      Mor := @μ.t P ;
      id := @μ.id P ;
      compose := @μ.compose P ;
      compose_assoc := @μ.compose_assoc P ;
      compose_id_l := @μ.compose_id_l P ;
      compose_id_r := @μ.compose_id_r P ;
      }.
End Category.