Containers based multisetoid

gistfile1.agda

record Container : Set where
  constructor _▹_
  field
    sh : Set
    po : sh → Set

⟦_⟧ : Container → Set → Set
⟦ sh ▹ po ⟧ A = Σ[ s ∶ sh ] (po s → A)

module _ {A : Set} {C : Container} (Q : A → Set) where
  Any : ⟦ C ⟧ A → Set
  Any ⟨ s , f ⟩ = Σ[ p ∶ Container.po C s ] Q (f p)

  All : ⟦ C ⟧ A → Set
  All ⟨ s , f ⟩ = (p : Container.po C s) → Q (f p)

record GeneralizedMultisetoid {T : Container} ⦃ TF : SetEndofunctor ⟦ T ⟧ ⦄ (TM : SetMonad TF) : Set where
  open SetMonad.SetMonad TM
  open SetEndofunctor.SetEndofunctor TF
  
  field
    ob : Set
    hom : ⟦ T ⟧ ob → ob → Set

    reflexivity : {X : ob}
      → hom (point X) X
    symmetry : {Tdom : ⟦ T ⟧ ob} {cod : ob}
      (φ : hom Tdom cod)
      → All (λ x → x) (map (hom (point cod)) Tdom)
    transitivity : {cod : ob}
      (Tp : ⟦ T  ⟧ (Σ[ Tdom ∶ ⟦ T ⟧ ob ] Σ ob (hom Tdom)))
      → hom (map (π₁ ∘ π₂) Tp) cod
      → hom (join (map π₁ Tp)) cod