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.
import
1 parent d8ec317 commit 2326602Copy full SHA for 2326602
src/Function/Bundles.agda
@@ -20,6 +20,7 @@
20
module Function.Bundles where
21
22
open import Function.Base using (_∘_)
23
+open import Function.Consequences.Propositional
24
open import Function.Definitions
25
import Function.Structures as FunctionStructures
26
open import Level using (Level; _⊔_; suc)
@@ -28,7 +29,6 @@ open import Relation.Binary.Bundles using (Setoid)
28
29
open import Relation.Binary.PropositionalEquality.Core as ≡
30
using (_≡_)
31
import Relation.Binary.PropositionalEquality.Properties as ≡
-open import Function.Consequences.Propositional
32
open Setoid using (isEquivalence)
33
34
private
0 commit comments