Issue234.agda

-- There was a problem with reordering telescopes.
module Issue234 where

postulate
  A : Set
  P : A → Set

data List : Set where
  _∷ : A → List

data _≅_ {x : A}(p : P x) : ∀ {y} → P y → Set where
  refl : p ≅ p

data _≡_ (x : A) : A → Set where
  refl : x ≡ x

data Any (x : A) : Set where
  here : P x → Any x

it : ∀ {x : A} → Any x → A
it {x} (here _) = x

prf : ∀ {x : A}(p : Any x) → P (it p)
prf (here px) = px

foo : (x : A) (p : Any x) →
      (f : ∀ {y} → it p ≡ y → P y) →
      f refl ≅ prf p →
      Set₁
foo x (here ._) f refl = Set