We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 3ca0b06 commit 8bf7322Copy full SHA for 8bf7322
src/Function/Related/TypeIsomorphisms.agda
@@ -361,6 +361,6 @@ Related-cong {A = A} {B = B} {C = C} {D = D} A≈B C≈D = mk⇔
361
-- restriction that the quantified variable is equal to the given one
362
363
∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y)
364
-∃-≡ P {x} = mk↔ₛ′ (⟨ id ⟩⊢⁻ id) (⟨ id ⟩⊢⁺ id)
+∃-≡ P {x} = mk↔ₛ′ (⟨ id ⟩⊢⁻ id) (⟨ id ⟩⊢⁺ id)
365
(λ where (_ , refl , _) → refl) (λ where _ → refl)
366
0 commit comments