Mercurial > hg > Members > kono > Proof > category
diff src/SetsCompleteness.agda @ 1034:40c39d3e6a75
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 31 Mar 2021 15:58:02 +0900 |
| parents | c3b3faa791fa |
| children | 45de2b31bf02 |
line wrap: on
line diff
--- a/src/SetsCompleteness.agda Tue Mar 30 23:31:10 2021 +0900 +++ b/src/SetsCompleteness.agda Wed Mar 31 15:58:02 2021 +0900 @@ -9,8 +9,8 @@ open import Function import Relation.Binary.PropositionalEquality -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → ( λ x → f x ≡ λ x → g x ) -import Axiom.Extensionality.Propositional -postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ +-- import Axiom.Extensionality.Propositional +-- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ -- Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ ≡cong = Relation.Binary.PropositionalEquality.cong