double-∐-lemma : {I : 𝓥 ̇ } (α : I → ⟨ ⟪ 𝓓 ⟹ᵈᶜᵖᵒ⊥ 𝓓 ⟫ ⟩)
                   (δ : is-Directed ⟪ 𝓓 ⟹ᵈᶜᵖᵒ⊥ 𝓓 ⟫ α)
                   (n : ℕ)
                 → ∐ ⟪ 𝓓 ⟫ (pointwise-family-is-directed ⟪ 𝓓 ⟫ ⟪ 𝓓 ⟫ α δ
                    (∐ ⟪ 𝓓 ⟫ (n-family-is-directed α δ n)))
                   ≡ ∐ ⟪ 𝓓 ⟫ (n-family-is-directed α δ (succ n))
  double-∐-lemma {I} α δ n = antisymmetry ⟪ 𝓓 ⟫ x y a b
   where
    ε : is-Directed ⟪ 𝓓 ⟫ (pointwise-family ⟪ 𝓓 ⟫ ⟪ 𝓓 ⟫ α
         (∐ ⟪ 𝓓 ⟫ (n-family-is-directed α δ n)))
    ε = (pointwise-family-is-directed ⟪ 𝓓 ⟫ ⟪ 𝓓 ⟫ α δ
         (∐ ⟪ 𝓓 ⟫ (n-family-is-directed α δ n)))
    φ : (n : ℕ) → is-Directed ⟪ 𝓓 ⟫ (n-family α n)
    φ n = n-family-is-directed α δ n

    x : ⟨ ⟪ 𝓓 ⟫ ⟩
    x = ∐ ⟪ 𝓓 ⟫ ε
    y : ⟨ ⟪ 𝓓 ⟫ ⟩
    y = ∐ ⟪ 𝓓 ⟫ (n-family-is-directed α δ (succ n))

    a : x ⊑⟨ ⟪ 𝓓 ⟫ ⟩ y
    a = ∐-is-lowerbound-of-upperbounds ⟪ 𝓓 ⟫ ε y g