Adding workaround and refactor monotone

[GenericMonkey]

• Adding the workaround from RecordEquiv reflection doesn't seem to handle implicit field arguments agda/cubical#995 (comment)
• Refactoring definition of MonFun and eliminating the (now redundant) proofs/defns with explicit arguments

[maxsnew]

A more thorough example would be better. Does the example work if Foo has parameters and if foo has parameters?

[GenericMonkey]

module _ where private
  Bar : ℕ → Type
  Bar 0 = Unit
  Bar _ = ℕ

  record Foo {n : ℕ} (b : Bar n) : Type where
    field
      foo : {a : ℕ} → Bar a
      baz : Bar n
      goo : b ≡ baz

  Sigma : {n : ℕ} (b : Bar n) → Type
  Sigma {n} b = Σ ({a : ℕ} → Bar a) (λ z → Σ (Bar n) (PathP (λ i → Bar n) b))

  foo-iso : ∀ {x : ℕ} {b : Bar x} → Iso (Foo b) (Sigma b)
  unquoteDef foo-iso = defineRecordIsoΣ foo-iso (quote Foo)

Something like this?

[maxsnew]

Yes