Set-2.agda

infix 4 _∈_ _∉_
data _∈_ {f} {A : Set f} (x : A) (B : Set f) : Set (suc f) where
  in-eq : A ≡ B → x ∈ B

_∉_ : {B : Set} → B → Set → Set₁
X ∉ A = (X ∈ A) → ⊥

module elem-lemmas where
  elem-∈ : {A B : Set} → ∀{x : B} → x ∈ A → A
  elem-∈ {x = x} (in-eq ≡-refl) = x

  ≡-∈ : {A X : Set} {x y : X} → x ≡ y → x ∈ A → y ∈ A
  ≡-∈ x≡y x∈A rewrite x≡y = x∈A

  ∈-≡ : {A B : Set} → {X : A} → A ≡ B → X ∈ A → X ∈ B
  ∈-≡ {X = X} A≡B X∈A rewrite A≡B = X∈A
open elem-lemmas public

infix 5 _⊆_ _⊊_
_⊆_ : Set → Set → Set₁
_⊆_ A B = ∀ {X : Set} {x : X} → x ∈ A → x ∈ B

_⊊_ : Set → Set → Set₁
A ⊊ B = (A ≢ B) ∧ (A ⊆ B)

module ⊆-Hetero where
  ⊆-≡-reflˡ : {A B C : Set} → B ≡ C → A ⊆ B → A ⊆ C
  ⊆-≡-reflˡ B≡C A⊆B x∈A rewrite B≡C = A⊆B x∈A

  ⊆-≡-reflʳ : {A B C : Set} → A ≡ C → A ⊆ B → C ⊆ B
  ⊆-≡-reflʳ A≡C A⊆B x∈C rewrite A≡C = A⊆B x∈C
open ⊆-Hetero public

{-
how to express the axiom of pairing ?

∃-pairing : ∀(A B : Set) → ∃ \(P : Set) → ∀ x → x ∈ P ⇔ (x ≡ A) ∨ (x ≡ B)
-}

Set.agda

module Sets.Sets where

open import Level
open import Function
open import Algebra.Structures
open import Data.Empty using (⊥ ; ⊥-elim)
open import Data.Unit using (⊤)
open import Data.Product using (Σ ; proj₁ ; proj₂ ; _,_ ; ∃)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; _≢_ ; subst₂ ; cong₂)
  renaming (isEquivalence to ≡-isEquivalence ; refl to ≡-refl ; sym to ≡-sym ; trans to ≡-trans)
  public
open import Relation.Nullary
open import Relation.Nullary.Negation

infix 4 _∧_
record _∧_ {f} (P Q : Set f) : Set f where
  constructor _,_
  field
    ∧-left : P
    ∧-right : Q
open _∧_ public

infix 4 _∨_
data _∨_ {f} (P Q : Set f) : Set f where
  ∨-left : P → P ∨ Q
  ∨-right : Q → P ∨ Q

infix 2 _⇔_
_⇔_ : ∀{f} → (A B : Set f) → Set f
_⇔_ A B = (A → B) ∧ (B → A)

proj⃗ : ∀{f} {A B : Set f} → (A ⇔ B) → (A → B)
proj⃗ = ∧-left

proj⃖ : ∀{f} {A B : Set f} → (A ⇔ B) → (B → A)
proj⃖ = ∧-right

⇔-contraposition : ∀{f} {A B : Set f} → A ⇔ B → (¬ A) ⇔ (¬ B)
⇔-contraposition P = contraposition (proj⃖ P) , contraposition (proj⃗ P)

postulate
  ¬¬-elim : ∀{f} → Double-Negation-Elimination f

non-datur : ∀{f} {A : Set f} → A ∨ (¬ A)
non-datur = ¬¬-elim $ \nnp → nnp (∨-right $ \p → nnp $ ∨-left p)

module Axioms where
  infix 4 _∈_ _∉_

  postulate
    _∈_ : Set → Set → Set₁
    elem-∈ : {A : Set} → ∀ x → x ∈ A → A
    ≡-∈ : {A X Y : Set} → X ≡ Y → X ∈ A → Y ∈ A

    extensionality : {A B : Set} → A ≡ B ⇔ Lift {_} {zero} (∀ x → (x ∈ A ⇔ x ∈ B))

  _∉_ : Set → Set → Set₁
  X ∉ A = X ∈ A → ⊥

  ⇔-extensionality : {A B : Set} → (∀ X → (X ∈ A ⇔ X ∈ B)) → A ≡ B
  ⇔-extensionality f = proj⃖ extensionality (lift f)

  app-extensionality : {A B : Set} → A ≡ B → ∀ X → (X ∈ A ⇔ X ∈ B)
  app-extensionality eq = lower (proj⃗ extensionality eq)

  ∈-≡ : {A B : Set} → {X : Set} → A ≡ B → X ∈ A → X ∈ B
  ∈-≡ {X = X} A≡B X∈A = proj⃗ (app-extensionality A≡B X) X∈A

  infix 5 _⊆_ _⊊_
  _⊆_ : Set → Set → Set₁
  A ⊆ B = ∀ x → x ∈ A → x ∈ B

  _⊊_ : Set → Set → Set₁
  A ⊊ B = (A ≢ B) ∧ (A ⊆ B)

  ⊆-≡-reflˡ : {A B C : Set} → B ≡ C → A ⊆ B → A ⊆ C
  ⊆-≡-reflˡ B≡C A⊆B x x∈A = proj⃗ (app-extensionality B≡C x) $ A⊆B x x∈A

  ⊆-≡-reflʳ : {A B C : Set} → A ≡ C → A ⊆ B → C ⊆ B
  ⊆-≡-reflʳ A≡C A⊆B x x∈C = A⊆B x $ proj⃖ (app-extensionality A≡C x) x∈C

  ⊆-isPartialOrder : IsPartialOrder _≡_ _⊆_
  ⊆-isPartialOrder = record
    { isPreorder = record
      { isEquivalence = ≡-isEquivalence
      ; reflexive = refl-≡⇒⊆
      ; trans = trans-⊆ }
    ; antisym = antisym-⊆ }
    where
      open IsPartialOrder

      refl-≡⇒⊆ : ∀{i j} → i ≡ j → i ⊆ j
      refl-≡⇒⊆ i≡j x = proj⃗ (lower (proj⃗ extensionality i≡j) x)

      trans-⊆ : {A B C : Set} → A ⊆ B → B ⊆ C → A ⊆ C
      trans-⊆ A⊆B B⊆C x x∈A = B⊆C x (A⊆B x x∈A)

      antisym-⊆ : {A B : Set} → A ⊆ B → B ⊆ A → A ≡ B
      antisym-⊆ A⊆B B⊆A = proj⃖ extensionality (lift (\x → A⊆B x , B⊆A x))
  open IsPartialOrder ⊆-isPartialOrder public

  ⇔-isEquivalence : ∀{f} → IsEquivalence {suc f} _⇔_
  ⇔-isEquivalence {f} = record
    { refl = id , id
    ; sym = \iff → proj⃖ iff , proj⃗ iff
    ; trans = \ij jk → _∘_ (proj⃗ jk) (proj⃗ ij) , _∘_ {f} (proj⃖ ij) (proj⃖ jk) }

  module ⇔-Reasoning {f} where
    ⇔-refl : {A : Set f} → A ⇔ A
    ⇔-refl = IsEquivalence.refl ⇔-isEquivalence

    ⇔-sym : {A B : Set f} → A ⇔ B → B ⇔ A
    ⇔-sym = IsEquivalence.sym ⇔-isEquivalence

    ⇔-trans : {A B C : Set f} → A ⇔ B → B ⇔ C → A ⇔ C
    ⇔-trans = IsEquivalence.trans ⇔-isEquivalence

    infixr 2 _∎
    infixr 2 _⇔⟨⟩_ _↓⟨_⟩_ _↑⟨_⟩_
    infix 1 begin_

    data _IsRelatedTo_ (A B : Set f) : Set (suc f) where
      relTo : A ⇔ B → A IsRelatedTo B

    begin_ : {A B : Set f} → A IsRelatedTo B → A ⇔ B
    begin (relTo A⇔B) = A⇔B
 
    _↓⟨_⟩_ : (A : Set f) → {B C : Set f} → A ⇔ B → B IsRelatedTo C → A IsRelatedTo C
    _ ↓⟨ x⇔y ⟩ relTo y⇔z = relTo (⇔-trans x⇔y y⇔z)

    _↑⟨_⟩_ : (A : Set f) → {B C : Set f} → B ⇔ A → B IsRelatedTo C → A IsRelatedTo C
    _ ↑⟨ y≈x ⟩ relTo y≈z = relTo (⇔-trans (IsEquivalence.sym ⇔-isEquivalence y≈x) y≈z)

    _⇔⟨⟩_ : (A : Set f) → {B : Set f} → A IsRelatedTo B → A IsRelatedTo B
    _ ⇔⟨⟩ x∼y = x∼y

    _∎ : (A : Set f) → A IsRelatedTo A
    _∎ _ = relTo ⇔-refl

  ⇔-≡-reflʳ : ∀{f} {A B C : Set f} → A ≡ C → (A ⇔ B) ≡ (C ⇔ B)
  ⇔-≡-reflʳ A≡C = cong₂ _⇔_ A≡C ≡-refl

  ⇔-≡-reflˡ : ∀{f} {A B C : Set f} → A ≡ C → (B ⇔ A) ≡ (B ⇔ C)
  ⇔-≡-reflˡ A≡C = cong₂ _⇔_ ≡-refl A≡C

  ≡-⇔-reflʳ : ∀{f} {A B C : Set f} → A ≡ C → (A ≡ B) ⇔ (C ≡ B)
  ≡-⇔-reflʳ A≡C = (\A≡B → ≡-trans (≡-sym A≡C) A≡B) , (\C≡B → ≡-trans A≡C C≡B)

  ≡-⇔-reflˡ : ∀{f} {A B C : Set f} → A ≡ C → (B ≡ A) ⇔ (B ≡ C)
  ≡-⇔-reflˡ A≡C = (\B≡A → ≡-trans B≡A A≡C) , (\B≡C → ≡-trans B≡C (≡-sym A≡C))

  ∨-sym : ∀{f} {A B : Set f} → A ∨ B → B ∨ A
  ∨-sym (∨-left a) = ∨-right a
  ∨-sym (∨-right b) = ∨-left b

  ∨-assoc : ∀{f} {A B C : Set f} → A ∨ (B ∨ C) → (A ∨ B) ∨ C
  ∨-assoc (∨-left A) = ∨-left $ ∨-left A
  ∨-assoc (∨-right (∨-left B)) = ∨-left $ ∨-right B
  ∨-assoc (∨-right (∨-right C)) = ∨-right C

  ∨-assoc-inv : ∀{f} {A B C : Set f} → (A ∨ B) ∨ C → A ∨ (B ∨ C)
  ∨-assoc-inv (∨-left (∨-left A)) = ∨-left $ A
  ∨-assoc-inv (∨-left (∨-right B)) = ∨-right $ ∨-left B
  ∨-assoc-inv (∨-right C) = ∨-right $ ∨-right C

  ∨-unrefl : ∀{f} {A : Set f} → A ∨ A → A
  ∨-unrefl (∨-left a) = a
  ∨-unrefl (∨-right a) = a

  ∨-≡-reflʳ : ∀{f} {A B C : Set f} → A ≡ C → A ∨ B → C ∨ B
  ∨-≡-reflʳ A≡C = subst₂ _∨_ A≡C ≡-refl

  ∨-≡-reflˡ : ∀{f} {A B C : Set f} → B ≡ C → A ∨ B → A ∨ C
  ∨-≡-reflˡ B≡C = subst₂ _∨_ ≡-refl B≡C

  ∨-→-reflʳ : ∀{f} {A B C : Set f} → (A → C) → A ∨ B → C ∨ B
  ∨-→-reflʳ f (∨-left A) = ∨-left $ f A
  ∨-→-reflʳ f (∨-right B) = ∨-right B

  ∨-→-reflˡ : ∀{f} {A B C : Set f} → (B → C) → A ∨ B → A ∨ C
  ∨-→-reflˡ f (∨-left A) = ∨-left A
  ∨-→-reflˡ f (∨-right B) = ∨-right $ f B

  ∧-refl : ∀{f} {A : Set f} → A → A ∧ A
  ∧-refl A = A , A

  ∧-sym : ∀{f} {A B : Set f} → A ∧ B → B ∧ A
  ∧-sym (A , B) = B , A

  ∅ : Set
  ∅ = ⊥

  ∃-empty-prop : Set₁
  ∃-empty-prop = ∃ \(A : Set) → (∀ x → ¬ (x ∈ A))

  ∃-empty : ∃-empty-prop
  ∃-empty = ⊥ , elem-∈

  ∅⇔⊆ : ∃-empty-prop ⇔ (∀(A : Set) → ⊥ ⊆ A)
  ∅⇔⊆ = lemma , \_ → ∃-empty where
    lemma : ∃-empty-prop → (A : Set) → ⊥ ⊆ A
    lemma P A x x∈⊥ = ⊥-elim (elem-∈ x x∈⊥)

  ∅-⊆ : (A : Set) → ∅ ⊆ A
  ∅-⊆ = proj⃗ ∅⇔⊆ ∃-empty

  ∅-uniqueness : (P : ∃-empty-prop) → (proj₁ P) ≡ ⊥
  ∅-uniqueness P = proj⃖ extensionality (lift \x → (\x∈projP → ⊥-elim (proj₂ P x x∈projP)) , \x∈⊥ → ⊥-elim (elem-∈ x x∈⊥))

  postulate
    ∃-paring : ∀(A B : Set) → ∃ \(P : Set) → ∀ x → x ∈ P ⇔ (x ≡ A) ∨ (x ≡ B)

  [_,_] : ∀(A B : Set) → Set
  [ A , B ] = proj₁ (∃-paring A B)

  singleton : ∀(A : Set) → Set
  singleton A = [ A , A ]

  module paring-lemmas where
    [,]-comm : {A B : Set} → [ A , B ] ≡ [ B , A ]
    [,]-comm {A} {B} = proj⃖ extensionality (lift \x → lemma x)
      where
        lemma : (x : Set) → x ∈ [ A , B ] ⇔ x ∈ [ B , A ]
        lemma x = (\x∈[A,B] → proj⃖ (proj₂ (∃-paring B A) x) $ ∨-sym $ proj⃗ (proj₂ (∃-paring A B) x) x∈[A,B])
                , (\x∈[B,A] → proj⃖ (proj₂ (∃-paring A B) x) $ ∨-sym $ proj⃗ (proj₂ (∃-paring B A) x) x∈[B,A])

    in-[A,B] : {A B : Set} → (X : Set) → X ∈ [ A , B ] → (X ≡ A) ∨ (X ≡ B)
    in-[A,B] {A} {B} X X∈[A,B] = proj⃗ (proj₂ (∃-paring A B) X) X∈[A,B]

    A∈[A,B] : {A B : Set} → A ∈ [ A , B ]
    A∈[A,B] {A} {B} = proj⃖ (proj₂ (∃-paring A B) A) (∨-left (IsEquivalence.refl isEquivalence))

    B∈[A,B] : {A B : Set} → B ∈ [ A , B ]
    B∈[A,B] {A} {B} = proj⃖ (proj₂ (∃-paring A B) B) (∨-right (IsEquivalence.refl isEquivalence))

    in-[A,A] : {A : Set} → ∀ X → X ∈ singleton A → X ≡ A
    in-[A,A] {A} X X∈[A,A] = ∨-unrefl $ in-[A,B] X X∈[A,A]

    ≡-singleton : {A B : Set} → A ≡ B ⇔ singleton A ≡ singleton B
    ≡-singleton {A} {B} = lemma , (\eq → ∨-unrefl $ in-[A,B] A $ A∈[B,B] eq)
      where
        A∈[B,B] : singleton A ≡ singleton B → A ∈ singleton B
        A∈[B,B] eq = ∈-≡ eq A∈[A,B]

        lemma : A ≡ B → singleton A ≡ singleton B
        lemma A≡B = proj⃖ extensionality $ lift $ \X
          → (\X∈A → proj⃖(proj₂ (∃-paring B B) X) $ ∨-left $ ≡-trans (in-[A,A] {A} X X∈A) A≡B)
          , (\X∈B → proj⃖(proj₂ (∃-paring A A) X) $ ∨-left $ ≡-trans (in-[A,A] {B} X X∈B) $ ≡-sym A≡B)

    prop-1 : {A B : Set} → [ A , B ] ≡ singleton A ⇔ A ≡ B
    prop-1 {A} {B} = lemma-2 ∘ lemma , lemma-3
      where
        lemma : [ A , B ] ≡ singleton A → B ∈ singleton A
        lemma eq = proj⃗ (lower (proj⃗ extensionality eq) B) B∈[A,B]

        lemma-2 : B ∈ singleton A → A ≡ B
        lemma-2 B∈[A,A] = ≡-sym $ ∨-unrefl $ in-[A,B] B B∈[A,A]

        lemma-3 : A ≡ B → [ A , B ] ≡ singleton A
        lemma-3 iff = proj⃖ extensionality $ lift \X
          → (\X∈[A,B] → proj⃖ (proj₂ (∃-paring A A) X) $ ∨-≡-reflˡ (cong₂ _≡_ ≡-refl (≡-sym iff)) $ in-[A,B] X X∈[A,B])
          , (\X∈[A,A] → proj⃖ (proj₂ (∃-paring A B) X) $ ∨-≡-reflˡ (cong₂ _≡_ ≡-refl iff) $ in-[A,B] X X∈[A,A])

    prop-1-sym : {A B : Set} → [ B , A ] ≡ singleton A ⇔ A ≡ B
    prop-1-sym {A} {B} = let open ⇔-Reasoning in
      begin
        [ B , A ] ≡ singleton A ↓⟨ ≡-⇔-reflʳ [,]-comm ⟩
        [ A , B ] ≡ singleton A ↓⟨ prop-1 ⟩
        A ≡ B
      ∎

    ≡-[,C] : {A B C : Set} → A ≡ B → [ A , C ] ≡ [ B , C ]
    ≡-[,C] {A} {B} {C} A≡B = proj⃖ extensionality $ lift $ \X → lemma-1 X , lemma-3 X
      where
        lemma-2 : ∀ X → (X ≡ A) ∨ (X ≡ C) → X ∈ [ B , C ]
        lemma-2 X (∨-left X≡A) = proj⃖ (proj₂ (∃-paring B C) X) $ ∨-left $ ≡-trans X≡A A≡B
        lemma-2 X (∨-right X≡C) = proj⃖ (proj₂ (∃-paring B C) X) $ ∨-right X≡C

        lemma-1 : ∀ X → X ∈ [ A , C ] → X ∈ [ B , C ]
        lemma-1 X X∈[A,C] = lemma-2 X $ in-[A,B] X X∈[A,C]

        lemma-4 : ∀ X → (X ≡ B) ∨ (X ≡ C) → X ∈ [ A , C ]
        lemma-4 X (∨-left X≡B) = proj⃖ (proj₂ (∃-paring A C) X) $ ∨-left $ ≡-trans X≡B $ ≡-sym A≡B
        lemma-4 X (∨-right X≡C) = proj⃖ (proj₂ (∃-paring A C) X) $ ∨-right X≡C

        lemma-3 : ∀ X → X ∈ [ B , C ] → X ∈ [ A , C ]
        lemma-3 X X∈[B,C] = lemma-4 X $ in-[A,B] X X∈[B,C]

    prop-2 : {A B : Set} →
      [ singleton A , [ A , B ] ] ≡ [ singleton B , [ A , B ] ] ⇔ A ≡ B
    prop-2 {A} {B} = (\iff → lemma-2 $ in-[A,B] (singleton A) $ lemma iff)
      , (\A≡B → ≡-[,C] $ proj⃗ (≡-singleton) A≡B)
      where
        lemma : [ singleton A , [ A , B ] ] ≡ [ singleton B , [ A , B ] ] → singleton A ∈ [ singleton B , [ A , B ] ]
        lemma iff = proj⃗ (lower (proj⃗ extensionality iff) [ A , A ]) A∈[A,B]

        lemma-2 : (singleton A ≡ singleton B) ∨ (singleton A ≡ [ A , B ]) → A ≡ B
        lemma-2 (∨-left A≡B) = proj⃖ ≡-singleton A≡B
        lemma-2 (∨-right A≡[A,B]) = proj⃗ prop-1 $ ≡-sym A≡[A,B]

--    ≢-singleton : {A : Set} → A ≢ singleton A

--    prop-3 : ∅ ⊊ singleton ∅
--    prop-4 : singleton ∅ ⊊ [ ∅ , singleton ∅ ]
  open paring-lemmas

  ∈-singleton-⊆ : {A X : Set} → X ∈ A → singleton X ⊆ A
  ∈-singleton-⊆ X∈A x x∈[X] = ≡-∈ (≡-sym $ in-[A,A] x x∈[X]) X∈A

  postulate
    ∃-union : (A : Set) → ∃ \(B : Set) → ∀ X → X ∈ B ⇔ (∃ \C → (C ∈ A) ∧ (X ∈ C))

  infixr 6 _∪_
  _∪_ : (A B : Set) → Set
  A ∪ B = proj₁ (∃-union [ A , B ])

  ⋃_ : (F : Set) → Set
  ⋃ F = proj₁ (∃-union F)

  ⋃-∈-⊆ : {F X : Set} → X ∈ F → X ⊆ ⋃ F
  ⋃-∈-⊆ {F} {X} X∈⋃F x x∈X = proj⃖ (proj₂ (∃-union F) x) $ X , (X∈⋃F , x∈X)

  ⋃-cong : {A B : Set} → A ⊆ B → ⋃ A ⊆ ⋃ B
  ⋃-cong {A} {B} A⊆B x x∈⋃A = proj⃖ (proj₂ (∃-union B) x) $ y , (∧-→-refl (A⊆B y) y∈A∧x∈y)
    where
      y = proj₁ (proj⃗ (proj₂ (∃-union A) x) x∈⋃A)
      y∈A∧x∈y = proj₂ (proj⃗ (proj₂ (∃-union A) x) x∈⋃A)

      ∧-→-refl : ∀{f} {A B C : Set f} → (A → C) → A ∧ B → C ∧ B
      ∧-→-refl f (y , refl) = f y , refl

  ∪⇔∨ : {A B : Set} → ∀ X → X ∈ A ∪ B ⇔ (X ∈ A) ∨ (X ∈ B)
  ∪⇔∨ {A} {B} X = lemma ∘ X∈A , X∈A∪B
    where
      X∈A : X ∈ A ∪ B → ∃ \C → ((C ∈ [ A , B ]) ∧ (X ∈ C))
      X∈A X∈A∪B = proj⃗ (proj₂ (∃-union [ A , B ]) X) X∈A∪B

      lemma : (p : ∃ \C → ((C ∈ [ A , B ]) ∧ (X ∈ C))) → (X ∈ A) ∨ (X ∈ B)
      lemma p = let C∈[A,B] = ∧-left $ proj₂ p ; X∈C = ∧-right $ proj₂ p in
        X∈A∨B (proj⃗ (proj₂ (∃-paring A B) (proj₁ p)) C∈[A,B]) X∈C
        where
          X∈A∨B : (proj₁ p ≡ A) ∨ (proj₁ p ≡ B) → (X ∈ proj₁ p) → (X ∈ A) ∨ (X ∈ B)
          X∈A∨B (∨-left C≡A) X∈C = ∨-left $ ∈-≡ C≡A X∈C
          X∈A∨B (∨-right C≡B) X∈C = ∨-right $ ∈-≡ C≡B X∈C

      X∈A∪B : (X ∈ A) ∨ (X ∈ B) → X ∈ A ∪ B
      X∈A∪B (∨-left X∈A) = proj⃖ (proj₂ (∃-union [ A , B ]) X) $ A , (A∈[A,B] , X∈A)
      X∈A∪B (∨-right X∈B) = proj⃖ (proj₂ (∃-union [ A , B ]) X) $ B , (B∈[A,B] , X∈B)

  ∪-∨ : {A B : Set} → ∀ X → X ∈ A ∪ B → (X ∈ A) ∨ (X ∈ B)
  ∪-∨ X = proj⃗ $ ∪⇔∨ X

  ∨-∪ : {A B : Set} → ∀ X → (X ∈ A) ∨ (X ∈ B) → X ∈ A ∪ B
  ∨-∪ X = proj⃖ $ ∪⇔∨ X

  ⋃-singleton : {X : Set} → ⋃ singleton X ≡ X
  ⋃-singleton = ⇔-extensionality $ \Y →
    (\Y∈∪[X] → ∨-unrefl $ ∪-∨ Y Y∈∪[X]) ,
    (\Y∈X → ∨-∪ Y $ ∨-left $ Y∈X)

  module ∪-lemmas where
    ∪-idempotent : {A : Set} → A ∪ A ≡ A
    ∪-idempotent {A} = ⇔-extensionality $ \X →
      (\X∈A∪A → ∨-unrefl $ ∪-∨ X X∈A∪A) ,
      (\X∈A → ∨-∪ X $ ∨-left X∈A)

    ∪-comm : {A B : Set} → A ∪ B ≡ B ∪ A
    ∪-comm {A} {B} = ⇔-extensionality $ \X →
      (\X∈A∪B → ∨-∪ X $ ∨-sym $ ∪-∨ X X∈A∪B) ,
      (\X∈B∪A → ∨-∪ X $ ∨-sym $ ∪-∨ X X∈B∪A)

    ∪-assoc : {A B C : Set} → A ∪ (B ∪ C) ≡ (A ∪ B) ∪ C
    ∪-assoc = ⇔-extensionality $ \X →
      (\X∈A∪[B∪C] → ∨-∪ X $ ∨-→-reflʳ (∨-∪ X) $ ∨-assoc $ ∨-→-reflˡ (∪-∨ X) $ ∪-∨ X X∈A∪[B∪C]) ,
      (\X∈[A∪B]∪C → ∨-∪ X $ ∨-→-reflˡ (∨-∪ X) $ ∨-assoc-inv $ ∨-→-reflʳ (∪-∨ X) $ ∪-∨ X X∈[A∪B]∪C)

    ⊆⇔∪ : {A B : Set} → A ⊆ B ⇔ A ∪ B ≡ B
    ⊆⇔∪ {A} {B} =
      (\A⊆B → ⇔-extensionality $ \X → (\X∈A∪B → lemma X A⊆B $ ∪-∨ X X∈A∪B) , \X∈B → ∨-∪ X $ ∨-right X∈B) ,
      (\eq Y Y∈A → Y∈B Y Y∈A $ iff eq Y)
      where
        lemma : ∀ X → A ⊆ B → (X ∈ A) ∨ (X ∈ B) → X ∈ B
        lemma X A⊆B (∨-left X∈A) = A⊆B X X∈A
        lemma _ _ (∨-right X∈B) = X∈B

        iff : A ∪ B ≡ B → ∀ Y → (Y ∈ A ∪ B ⇔ Y ∈ B)
        iff eq X = app-extensionality eq X

        Y∈B : ∀ Y → Y ∈ A → (Y ∈ A ∪ B ⇔ Y ∈ B) → Y ∈ B
        Y∈B Y Y∈A eq = proj⃗ eq $ ∨-∪ Y $ ∨-left Y∈A

    ∪-∅ : {A : Set} → A ∪ ∅ ≡ A
    ∪-∅ {A} = ⇔-extensionality $ \X → (\X∈A∪∅ → lemma X $ ∪-∨ X X∈A∪∅) , (\X∈A → ∨-∪ X $ ∨-left X∈A)
      where
        lemma : ∀ X → (X ∈ A) ∨ (X ∈ ∅) → X ∈ A
        lemma X (∨-left X∈A) = X∈A
        lemma X (∨-right X∈∅) = ⊥-elim $ elem-∈ X X∈∅

  _⁺ : (A : Set) → Set
  A ⁺ = A ∪ (singleton A)

  postulate
    infinite : ∃ \A → (∅ ∈ A) ∧ (∀ X → X ∈ A → X ⁺ ∈ A)

    replacement : (A : Set) → (P : Set → Set₁) → ∃ \B → ∀ x → x ∈ B ⇔ (x ∈ A) ∧ P x

  cond-set : (A : Set) → (∀ X → Set₁) → Set
  cond-set A f = proj₁ (replacement A f)

  syntax cond-set A (\X → P) = ⟦ X ∈ A ∣ P ⟧

  prop-1-4 : {A : Set} → let B = ⟦ X ∈ A ∣ X ∉ X ⟧ in B ∉ A
  prop-1-4 {A} p = ¬Q∧Q p non-datur
    where
      B = ⟦ X ∈ A ∣ X ∉ X ⟧
      P = B ∈ A
      Q = B ∈ B
      prop = proj₂ (replacement A (\X → X ∉ X))

      lemma : P → (¬ Q) ⇔ Q
      lemma P = (\notQ → proj⃖ (prop B) $ P , notQ)
              , (\q → proj⃖ (⇔-contraposition (prop B)) $ \and → ∧-right and q)

      ¬Q∧Q : P → (Q ∨ (¬ Q)) → ⊥
      ¬Q∧Q p (∨-left q) = proj⃖ (lemma p) q $ q
      ¬Q∧Q p (∨-right nq) = nq $ proj⃗ (lemma p) nq

  cor-1-4 : (A : Set) → ∃ \B → B ∉ A
  cor-1-4 A = ⟦ X ∈ A ∣ X ∉ X ⟧ , prop-1-4

  infixr 7 _∩_
  _∩_ : (A B : Set) → Set
  A ∩ B = ⟦ X ∈ A ∣ X ∈ B ⟧

  ∩⇔∧ : {A B : Set} → ∀ X → X ∈ A ∩ B ⇔ (X ∈ A) ∧ (X ∈ B)
  ∩⇔∧ {A} {B} X = X∈A∧X∈B , X∈A∩B
    where
      X∈A∧X∈B : X ∈ A ∩ B → (X ∈ A) ∧ (X ∈ B)
      X∈A∧X∈B X∈A∩B = proj⃗ (proj₂ (replacement A $ \X → X ∈ B) X) X∈A∩B

      X∈A∩B : (X ∈ A) ∧ (X ∈ B) → X ∈ A ∩ B
      X∈A∩B and = proj⃖ (proj₂ (replacement A $ \X → X ∈ B) X) and

  ∩-∧ : {A B : Set} → ∀ X → X ∈ A ∩ B → (X ∈ A) ∧ (X ∈ B)
  ∩-∧ X = proj⃗ (∩⇔∧ X)

  ∧-∩ : {A B : Set} → ∀ X → (X ∈ A) ∧ (X ∈ B) → X ∈ A ∩ B
  ∧-∩ X = proj⃖ (∩⇔∧ X)

  ∩-⊆ˡ : {A B : Set} → A ∩ B ⊆ A
  ∩-⊆ˡ x x∈A∩B = ∧-left $ ∩-∧ x x∈A∩B

  ∩-⊆ʳ : {A B : Set} → A ∩ B ⊆ B
  ∩-⊆ʳ x x∈A∩B = ∧-right $ ∩-∧ x x∈A∩B

  module ∩-lemmas where
    ∩-idempotent : {A : Set} → A ∩ A ≡ A
    ∩-idempotent = ⇔-extensionality $ \X →
      (\X∈A∩A → ∧-left $ ∩-∧ X X∈A∩A) ,
      (\X∈A → ∧-∩ X $ ∧-refl X∈A)

    ∩-comm : {A B : Set} → A ∩ B ≡ B ∩ A
    ∩-comm = ⇔-extensionality $ \X → (∧-∩ X ∘ ∧-sym ∘ ∩-∧ X) , (∧-∩ X ∘ ∧-sym ∘ ∩-∧ X)
--    ∩-assoc : {A B C : Set} → (A ∩ B) ∩ C ≡ A ∩ (B ∩ C)
    ⊆⇔∩ : {A B : Set} → A ⊆ B ⇔ A ∩ B ≡ A
    ⊆⇔∩ = (\A⊆B → ⇔-extensionality $ \X →
      (\X∈A∩B → ∧-left $ ∩-∧ X X∈A∩B) , (\X∈A → ∧-∩ X $ X∈A , A⊆B X X∈A)) ,
      (\eq X X∈A → ∩-⊆ʳ X $ proj⃖ (app-extensionality eq X) X∈A)

    ∩-∅ : {A : Set} → A ∩ ∅ ≡ ∅
    ∩-∅ {A} = ⇔-extensionality $ \X →
      (\X∈A∩∅ → ∧-right $ ∩-∧ X X∈A∩∅) ,
      (\X∈∅ → ∧-∩ X $ (∅-⊆ A X X∈∅) , X∈∅)

--    distributive law, complement

  postulate
    powerset : (A : Set) → ∃ \B → ∀ X → X ∈ B ⇔ X ⊆ A

  P[_] : Set → Set
  P[ A ] = proj₁ (powerset A)

  ⊆-∈-power : {X A : Set} → A ⊆ X → A ∈ P[ X ]
  ⊆-∈-power {X} {A} = proj⃖ (proj₂ (powerset X) A)

  ∈-⊆-power : {X A : Set} → A ∈ P[ X ] → A ⊆ X
  ∈-⊆-power {X} {A} = proj⃗ (proj₂ (powerset X) A)

  ⋃-power : {X : Set} → ⋃ P[ X ] ≡ X
  ⋃-power {X} = antisym
    (\Y Y∈∪P → let ex = y∈P[X] Y Y∈∪P in y∈X Y (proj₁ ex) (proj₂ ex))
    (\Y Y∈X → proj⃖ (proj₂ (∃-union P[ X ]) Y) $ X , (⊆-∈-power (\_ → id)) , Y∈X)
    where
      y∈P[X] : ∀ Y → Y ∈ ⋃ P[ X ] → ∃ \Z → (Z ∈ P[ X ]) ∧ (Y ∈ Z)
      y∈P[X] Y Y∈∪P = (proj⃗ (proj₂ (∃-union P[ X ]) Y)) Y∈∪P

      y∈X : ∀ Y Z → (Z ∈ P[ X ]) ∧ (Y ∈ Z) → Y ∈ X
      y∈X Y Z and = ∈-⊆-power (∧-left and) Y (∧-right and)

open Axioms public