The Category of Setoids can be used as the Ambient Category

Most of the required properties are already proven in the agda-categories library, we are only left to show distributivity.

module Category.Ambient.Setoids {c ℓ} where
  open M (Setoids c (c ⊔ ℓ))
  open _⟶_ using (cong) renaming (to to <_>)

  refl : ∀ (A : Setoid c (c ⊔ ℓ)) {a} → Setoid._≈_ A a a
  refl A = IsEquivalence.refl (Setoid.isEquivalence A)

  setoidDistributive : Distributive (Setoids c (c ⊔ ℓ))
  Distributive.cartesian setoidDistributive = Setoids-Cartesian
  Distributive.cocartesian setoidDistributive = Setoids-Cocartesian {c} {(c ⊔ ℓ)}
  < IsIso.inv (Distributive.isIsoˡ setoidDistributive {A} {B} {C}) > (x , (inj₁ y)) = inj₁ (x , y)
  < IsIso.inv (Distributive.isIsoˡ setoidDistributive {A} {B} {C}) > (x , (inj₂ y)) = inj₂ (x , y)
  cong (IsIso.inv (Distributive.isIsoˡ setoidDistributive {A} {B} {C})) {(x , inj₁ y)} {(a , inj₁ b)} (x≈a , inj₁ y≈b) = inj₁ (x≈a , y≈b)
  cong (IsIso.inv (Distributive.isIsoˡ setoidDistributive {A} {B} {C})) {(x , inj₂ y)} {(a , inj₂ b)} (x≈a , inj₂ y≈b) = inj₂ (x≈a , y≈b)
  Iso.isoˡ (IsIso.iso (Distributive.isIsoˡ setoidDistributive {A} {B} {C})) {inj₁ (a , b)} = inj₁ (refl A , refl B)
  Iso.isoˡ (IsIso.iso (Distributive.isIsoˡ setoidDistributive {A} {B} {C})) {inj₂ (a , c)} = inj₂ (refl A , refl C)
  Iso.isoʳ (IsIso.iso (Distributive.isIsoˡ setoidDistributive {A} {B} {C})) {a , inj₁ b} = refl A , inj₁ (refl B)
  Iso.isoʳ (IsIso.iso (Distributive.isIsoˡ setoidDistributive {A} {B} {C})) {a , inj₂ c} = (refl A) , (inj₂ (refl C))

  setoidAmbient : Ambient (ℓ-suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
  setoidAmbient = record 
    { C = Setoids c (c ⊔ ℓ)
    ; distributive = setoidDistributive
    }