Cubical Agda Inclusion Order

I'm almost finished defining an Inclusion Order in Cubical Agda, But I'm stuck proving the second projections are equal for dependent pairs. I would appreciate it if someone can fill in the hole for the antisymmetric relation.

{-# OPTIONS --cubical #-}
{-# OPTIONS --without-K #-}
{-# OPTIONS --safe #-}

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism

open import Agda.Primitive

private
  variable
    l l' al bl : Level
    A : Type al
    B : Type bl

-- https://en.wikipedia.org/wiki/Partially_ordered_set
record Poset (A : Type l)(l' : Level) : Type (lsuc (l ⊔ l'))
  where field
  _≤_ : A → A → Type l'
  leProp : (x y : A) → isProp (x ≤ y)
  leTrans : (x y z : A) → x ≤ y → y ≤ z → x ≤ z
  leRefl : (x : A) → x ≤ x
  antiSym : (x y : A) → x ≤ y → y ≤ x → x ≡ y
open Poset {{...}}

isPropEq : (A → B) → (B → A) → isProp A → isProp B → A ≡ B
isPropEq f g p q = isoToPath (iso f g (λ b → q (f (g b)) b) (λ a → p (g (f a)) a))

PropSet : (l' : Level) → (A : Type l) → Type (l ⊔ (lsuc l'))
PropSet l' A = Σ (A → Type l') λ f → (x : A) → isProp (f x)

instance
  -- https://en.wikipedia.org/wiki/Inclusion_order
  InclusionOrder : {A : Type l} → Poset (PropSet l' A) (l ⊔ l')
  InclusionOrder {A = A} = record
                   { _≤_ = λ{(f , _) (g , _) -> (a : A) → f a → g a}
                   ; leProp = λ{(f , f') (g , g') a b → funExt (λ z → let H = f' z in funExt (λ w → g' z (a z w) (b z w)))}
                   ; leTrans = λ X Y Z p q a b → q a (p a b)
                   ; leRefl = λ x a z → z
                   ; antiSym = λ{ (w , w') (x , x') f g → let H : w ≡ x
                                                              H = funExt (λ y →
                                                                  isPropEq (f y) (g y) (w' y) (x' y)) in
                                                           λ i → (H i) , {!!}
                                                              } }

I partially understand partial types. I'm sure I have to use 'hcomp' when dealing with the constraints but I'm still unable to wrap my head around 'hcomp'. You may change code outside of the hole if it makes it easier for you.

You can do this in "HoTT style" without introducing any interval variables:

ΣPathPProp (λ _ → isPropΠ λ _ → isPropIsProp) H

The second component of PropSet is a proposition (because isProp is a proposition and Π types preserve propositionality), and paths in such Σ types are entirely determined by paths between the first components.

Doing this in "cubical style" would be more annoying because of issues like https://github.com/agda/agda/issues/6009.