text:
open import Agda.Builtin.Equality using (_≡_; refl)

record ⊤ : Set where
  no-eta-equality
  constructor tt

data Box (A : Set) : Set where
  [_] : A → Box A

Unit : Set
Unit = Box ⊤

F : Unit → Set → Set
F [ _ ] x = x

G : {P : Unit → Set} → ((x : ⊤) → P [ x ]) → ((x : Unit) → P x)
G f [ x ] = f x

record R : Set₁ where
  no-eta-equality
  field
    f : (x : Unit) → Box (F x ⊤)

  data ⊥ : Set where

r : R
r = record { f = G [_] }

open R r

H : ⊥ → Set₁
H _ rewrite refl {x = tt} = Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2015-07-13  Better parse errors for illegal type signatures

A | B : Set

ext: agda


text:
{-
This file shows Hⁿ⁺ᵐ(Sⁿ×Sᵐ)≅ℤ for n, m ≥ 1. This can be done in several
ways (e.g. Mayer-Vietoris). We give the iso as explicitly
as possible. The idea:
Step 1: Hⁿ⁺ᵐ(Sⁿ×Sᵐ)≅H¹⁺ⁿ⁺ᵐ(S¹⁺ⁿ×Sᵐ) (i.e. some form of suspension
axiom).
Step 2: H¹⁺ᵐ(S¹×Sᵐ)≅ℤ
Step 3: Conclude Hⁿ⁺ᵐ(Sⁿ×Sᵐ)≅ℤ by induction on n.

The iso as defined here has the advantage that it looks a lot like
the cup product, making it trivial to show that e.g. gₗ ⌣ gᵣ ≡ e, where
gₗ, gᵣ are the two generators of H²(S²×S²) and e is the generator of
H⁴(S²×S²) -- this of interest since it is used in π₄S³≅ℤ/2.
-}

{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.Groups.SphereProduct where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws

open import Cubical.Relation.Nullary

open import Cubical.Data.Unit
open import Cubical.Data.Nat
open import Cubical.Data.Sigma

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Instances.Int

open import Cubical.HITs.Truncation as T
open import Cubical.HITs.SetTruncation as ST
open import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.HITs.S1
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp

open import Cubical.Homotopy.Loopspace

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.Groups.Sn
open import Cubical.ZCohomology.RingStructure.CupProduct

open Iso
open PlusBis

private
  ¬lem : (n m : ℕ) → ¬ suc (n + m) ≡ m
  ¬lem n zero = snotz
  ¬lem n (suc m) p =
    ¬lem n m (sym (+-suc n m) ∙ cong predℕ p)

{- Step 1: Hⁿ⁺ᵐ(Sⁿ×Sᵐ)≅H¹⁺ⁿ⁺ᵐ(S¹⁺ⁿ×Sᵐ) -}
-- The functions back and forth (suspension on the left component)
↓Sⁿ×Sᵐ→Kₙ₊ₘ : (n m : ℕ)
  → (S₊ (suc (suc n)) → S₊ (suc m) → coHomK (suc (suc ((suc n) + m))))
  → S₊ (suc n) → S₊ (suc m) → coHomK (suc (suc (n + m)))
↓Sⁿ×Sᵐ→Kₙ₊ₘ n m f x y =
  ΩKn+1→Kn ((suc ((suc n) + m)))
    (sym (rCancelₖ _ (f north y))
    ∙∙ cong (λ x → f x y -ₖ f north y) (merid x ∙ sym (merid (ptSn (suc n))))
    ∙∙ rCancelₖ _ (f north y))

↑Sⁿ×Sᵐ→Kₙ₊ₘ : (n m : ℕ)
  → (S₊ (suc n) → S₊ (suc m) → coHomK (suc (suc (n + m))))
  → (S₊ (suc (suc n)) → S₊ (suc m) → coHomK (suc (suc ((suc n) + m))))
↑Sⁿ×Sᵐ→Kₙ₊ₘ n m f north y = 0ₖ _
↑Sⁿ×Sᵐ→Kₙ₊ₘ n m f south y = 0ₖ _
↑Sⁿ×Sᵐ→Kₙ₊ₘ n m f (merid a i) y =
  Kn→ΩKn+1 _ (f a y) i

∥HⁿSᵐPath∥ : (n m : ℕ) → (f : S₊ (suc m) → coHomK (suc n))
       → ¬ (n ≡ m)
       → ∥ f ≡ (λ _ → 0ₖ (suc n)) ∥₁
∥HⁿSᵐPath∥ n m f p =
  fun PathIdTrunc₀Iso
    (isContr→isProp
      (isOfHLevelRetractFromIso 0 (fst (Hⁿ-Sᵐ≅0 n m p)) isContrUnit)
        ∣ f ∣₂ (0ₕ _))

-- The iso
×leftSuspensionIso : (n m : ℕ)
  → GroupIso (coHomGr (suc (((suc n) + m)))
                  (S₊ (suc n) × S₊ (suc m)))
              (coHomGr (suc (suc ((suc n) + m)))
                  (S₊ (suc (suc n)) × S₊ (suc m)))
fun (fst (×leftSuspensionIso n m)) =
  ST.map (uncurry ∘ ↑Sⁿ×Sᵐ→Kₙ₊ₘ n m ∘ curry)
inv (fst (×leftSuspensionIso n m)) =
  ST.map ((uncurry ∘ ↓Sⁿ×Sᵐ→Kₙ₊ₘ n m ∘ curry))
rightInv (fst (×leftSuspensionIso n m)) =
  ST.elim (λ _ → isSetPathImplicit)
    λ f → inv PathIdTrunc₀Iso
      (PT.rec squash₁
        (uncurry (λ g p
          → PT.map (λ gid → funExt λ {(x , y)
         → (λ i → uncurry (↑Sⁿ×Sᵐ→Kₙ₊ₘ n m
                    (↓Sⁿ×Sᵐ→Kₙ₊ₘ n m (curry (p (~ i))))) (x , y))
                ∙∙ main g gid x y
                ∙∙ funExt⁻ p (x , y)})
                   (∥Path∥ g)))
        (rewrte f))
  where
  lem : (n m : ℕ) → ¬ suc (suc (n + m)) ≡ m
  lem n zero = snotz
  lem n (suc m) p = lem n m (cong suc (sym (+-suc n m)) ∙ cong predℕ p)

  charac-fun :
      (S₊ (suc n) → S₊ (suc m)
              → typ (Ω (coHomK-ptd (suc (suc (suc n + m))))))
    → S₊ (suc (suc n)) × S₊ (suc m) → coHomK (suc (suc (suc n + m)))
  charac-fun g (north , y) = 0ₖ _
  charac-fun g (south , y) = 0ₖ _
  charac-fun g (merid c i , y) = g c y i

  rewrte : (f : S₊ (suc (suc n)) × S₊ (suc m)
           → coHomK (suc (suc (suc n + m))))
       → ∃[ g ∈ (S₊ (suc n) → S₊ (suc m)
              → typ (Ω (coHomK-ptd (suc (suc (suc n + m)))))) ]
            charac-fun g ≡ f
  rewrte f =
    PT.map (λ p
      → (λ x y → sym (funExt⁻ p y)
                ∙∙ (λ i → f ((merid x ∙ sym (merid (ptSn (suc n)))) i , y))
                ∙∙ funExt⁻ p y)
       , funExt λ { (north , y) → sym (funExt⁻ p y)
                  ; (south , y) → sym (funExt⁻ p y)
                                ∙ λ i → f (merid (ptSn (suc n)) i , y)
                  ; (merid a i , y) j
              → hcomp (λ k → λ { (i = i0) → p (~ j ∧ k) y
                                 ; (i = i1)
                                  → compPath-filler'
                                      (sym (funExt⁻ p y))
                                      (λ i → f (merid (ptSn (suc n)) i , y)) k j
                                 ; (j = i1) → f (merid a i , y) })
                       (f (compPath-filler (merid a)
                          (sym (merid (ptSn (suc n)))) (~ j) i
                         , y))})
      (∥HⁿSᵐPath∥ _ _ (λ x → f (north , x))
        (lem n m))

  ∥Path∥ :
    (g : S₊ (suc n) → S₊ (suc m)
         → typ (Ω (coHomK-ptd (suc (suc (suc n + m))))))
       → ∥ (g (ptSn _)) ≡ (λ _ → refl) ∥₁
  ∥Path∥ g =
      fun PathIdTrunc₀Iso
        (isContr→isProp
          (isOfHLevelRetractFromIso 0
            ((invIso (fst (coHom≅coHomΩ _ (S₊ (suc m))))))
             (0ₕ _ , ST.elim (λ _ → isProp→isSet (squash₂ _ _))
                 λ f → PT.rec (squash₂ _ _) (sym ∘ cong ∣_∣₂)
                   (∥HⁿSᵐPath∥ _ _ f (¬lem n m))))
          ∣ g (ptSn (suc n)) ∣₂ ∣ (λ _ → refl) ∣₂)

  main : (g : _) → (g (ptSn _)) ≡ (λ _ → refl)
     → (x : S₊ (suc (suc n))) (y : S₊ (suc m))
    → uncurry (↑Sⁿ×Sᵐ→Kₙ₊ₘ n m
         (↓Sⁿ×Sᵐ→Kₙ₊ₘ n m (curry (charac-fun g)))) (x , y)
      ≡ charac-fun g (x , y)
  main g gid north y = refl
  main g gid south y = refl
  main g gid (merid a i) y j = helper j i
    where
    helper : (λ i → uncurry (↑Sⁿ×Sᵐ→Kₙ₊ₘ n m
                    (↓Sⁿ×Sᵐ→Kₙ₊ₘ n m (curry (charac-fun g))))
                     (merid a i , y))
      ≡ g a y
    helper = (λ i → rightInv (Iso-Kn-ΩKn+1 _)
                  ((sym (rCancel≡refl _ i)
           ∙∙ cong-∙ (λ x → rUnitₖ _ (charac-fun g (x , y)) i)
                (merid a) (sym (merid (ptSn (suc n)))) i
           ∙∙ rCancel≡refl _ i)) i)
        ∙∙ sym (rUnit _)
        ∙∙ (cong (g a y ∙_) (cong sym (funExt⁻ gid y))
          ∙ sym (rUnit (g a y)))
leftInv (fst (×leftSuspensionIso n m)) =
  ST.elim (λ _ → isSetPathImplicit)
        λ f → PT.rec (squash₂ _ _)
          (λ id
            → cong ∣_∣₂
              (funExt (λ {(x , y) → (λ i → ΩKn+1→Kn _ (sym (rCancel≡refl _ i)
                       ∙∙ ((λ j → rUnitₖ _
                             (↑Sⁿ×Sᵐ→Kₙ₊ₘ n m (curry f)
                               ((merid x ∙ sym (merid (ptSn (suc n)))) j) y) i))
                       ∙∙ rCancel≡refl _ i))
                ∙ (λ i → ΩKn+1→Kn _  (rUnit
                           (cong-∙ (λ r → ↑Sⁿ×Sᵐ→Kₙ₊ₘ n m (curry f) r y)
                              (merid x) (sym (merid (ptSn (suc n)))) i) (~ i)))
                ∙ cong (ΩKn+1→Kn _) (cong (Kn→ΩKn+1 _ (f (x , y)) ∙_)
                       (cong sym (cong (Kn→ΩKn+1 _)
                                  (funExt⁻ id y) ∙ (Kn→ΩKn+10ₖ _)))
                         ∙ sym (rUnit _))
                ∙ leftInv (Iso-Kn-ΩKn+1 _) (f (x , y))})))
          (∥HⁿSᵐPath∥ (suc n + m) m (λ x → f (ptSn _ , x))
            (¬lem n m))
snd (×leftSuspensionIso n m) =
  makeIsGroupHom (ST.elim2 (λ _ _ → isSetPathImplicit)
    λ f g → cong ∣_∣₂
      (funExt λ { (north , y) → refl
                ; (south , y) → refl
                ; (merid a i , y) j
                 → (sym (∙≡+₂ _ (Kn→ΩKn+1 _ (f (a , y)))
                         (Kn→ΩKn+1 _ (g (a , y))))
                   ∙ sym (Kn→ΩKn+1-hom _
                          (f (a , y)) (g (a , y)))) (~ j) i}))

{- Step 2: H¹⁺ᵐ(S¹×Sᵐ)≅ℤ -}

-- The functions back and forth
Hⁿ-S¹×Sⁿ→Hⁿ-Sⁿ : (m : ℕ)
  → (S₊ (suc m) → coHomK (suc m))
  → S₊ (suc zero) → S₊ (suc m) → coHomK (suc (suc m))
Hⁿ-S¹×Sⁿ→Hⁿ-Sⁿ m f base y = 0ₖ _
Hⁿ-S¹×Sⁿ→Hⁿ-Sⁿ m f (loop i) y = Kn→ΩKn+1 (suc m) (f y) i

Hⁿ-Sⁿ→Hⁿ-S¹×Sⁿ : (m : ℕ)
  → (S₊ (suc zero) → S₊ (suc m) → coHomK (suc (suc m)))
  → (S₊ (suc m) → coHomK (suc m))
Hⁿ-Sⁿ→Hⁿ-S¹×Sⁿ m f x =
  ΩKn+1→Kn (suc m)
       (sym (rCancelₖ _ (f base x))
    ∙∙ ((λ i → f (loop i) x -ₖ f base x))
    ∙∙ rCancelₖ _ (f base x))

Hⁿ-Sⁿ≅Hⁿ-S¹×Sⁿ : (m : ℕ)
  → GroupIso (coHomGr (suc m) (S₊ (suc m)))
              (coHomGr (suc (suc m)) (S₊ (suc zero) × S₊ (suc m)))
fun (fst (Hⁿ-Sⁿ≅Hⁿ-S¹×Sⁿ m)) = ST.map (uncurry ∘ Hⁿ-S¹×Sⁿ→Hⁿ-Sⁿ m)
inv (fst (Hⁿ-Sⁿ≅Hⁿ-S¹×Sⁿ m)) = ST.map (Hⁿ-Sⁿ→Hⁿ-S¹×Sⁿ m ∘ curry)
rightInv (fst (Hⁿ-Sⁿ≅Hⁿ-S¹×Sⁿ m)) =
  ST.elim (λ _ → isSetPathImplicit)
    λ f → inv PathIdTrunc₀Iso
      (PT.map (uncurry (λ g p
        → funExt λ {(x , y)
          → (λ i → uncurry
                      (Hⁿ-S¹×Sⁿ→Hⁿ-Sⁿ m
                        (Hⁿ-Sⁿ→Hⁿ-S¹×Sⁿ m (curry (p i)))) (x , y))
          ∙∙ main g x y
          ∙∙ sym (funExt⁻ p (x , y))}))
        (rewrte f))
  where
  characFun : (x : S₊ (suc m) → coHomK (suc m))
           → S₊ 1 × S₊ (suc m) → coHomK (suc (suc m))
  characFun f (base , y) = 0ₖ _
  characFun f (loop i , y) = Kn→ΩKn+1 _ (f y) i

  main : (g : _) (x : S¹) (y : S₊ (suc m))
    → uncurry (Hⁿ-S¹×Sⁿ→Hⁿ-Sⁿ m (Hⁿ-Sⁿ→Hⁿ-S¹×Sⁿ m (curry (characFun g))))
         (x , y)
      ≡ characFun g (x , y)
  main g base y = refl
  main g (loop i) y j = help j i
    where
    help : cong (λ x → Hⁿ-S¹×Sⁿ→Hⁿ-Sⁿ m
                         (Hⁿ-Sⁿ→Hⁿ-S¹×Sⁿ m (curry (characFun g))) x y) loop
         ≡ Kn→ΩKn+1 _ (g y)
    help = rightInv (Iso-Kn-ΩKn+1 (suc m))
                 (sym (rCancelₖ _ (0ₖ _))
              ∙∙ ((λ i → Kn→ΩKn+1 _ (g y) i -ₖ 0ₖ _))
              ∙∙ rCancelₖ _ (0ₖ _))
        ∙∙ (λ i → sym (rCancel≡refl _ i)
                ∙∙ (λ j → rUnitₖ _ (Kn→ΩKn+1 _ (g y) j) i)
                ∙∙ rCancel≡refl _ i)
        ∙∙ sym (rUnit _)

  lem : (m : ℕ) → ¬ suc m ≡ m
  lem zero = snotz
  lem (suc m) p = lem m (cong predℕ p)

  rewrte : (f : S₊ 1 × S₊ (suc m) → coHomK (suc (suc m)))
     → ∃[ g ∈ (S₊ (suc m) → coHomK (suc m)) ] f ≡ characFun g
  rewrte f =
    PT.map (λ p →
       (λ x → ΩKn+1→Kn _
                (sym (funExt⁻ p x) ∙∙ (λ i → f (loop i , x)) ∙∙ funExt⁻ p x))
      , funExt λ { (base , y) → funExt⁻ p y
                 ; (loop i , x) j →
                   hcomp (λ k → λ {(i = i0) → funExt⁻ p x j
                                  ; (i = i1) → funExt⁻ p x j
                                  ; (j = i0) → f (loop i , x)
                                  ; (j = i1) →
                                      rightInv (Iso-Kn-ΩKn+1 (suc m))
                                        (sym (funExt⁻ p x)
                                        ∙∙ (λ i → f (loop i , x))
                                        ∙∙ funExt⁻ p x) (~ k) i})
                          (doubleCompPath-filler
                            (sym (funExt⁻ p x))
                            (λ i → f (loop i , x))
                            (funExt⁻ p x) j i)})
     (∥HⁿSᵐPath∥ (suc m) m (λ x → f (base , x)) (lem m))
leftInv (fst (Hⁿ-Sⁿ≅Hⁿ-S¹×Sⁿ m)) =
  ST.elim (λ _ → isSetPathImplicit)
    λ f
      → cong ∣_∣₂ (funExt λ x
        → cong (ΩKn+1→Kn (suc m))
               ((λ i → sym (rCancel≡refl _ i)
                 ∙∙ cong (λ z → rUnitₖ _ (Hⁿ-S¹×Sⁿ→Hⁿ-Sⁿ m f z x) i) loop
                 ∙∙ rCancel≡refl _ i) ∙ sym (rUnit (Kn→ΩKn+1 (suc m) (f x))))
        ∙ leftInv (Iso-Kn-ΩKn+1 _) (f x))
snd (Hⁿ-Sⁿ≅Hⁿ-S¹×Sⁿ m) =
  makeIsGroupHom
    (ST.elim2
      (λ _ _ → isSetPathImplicit)
      λ f g → cong ∣_∣₂
        (funExt λ { (base , y) → refl
                  ; (loop i , y) j →
                          (sym (∙≡+₂ _ (Kn→ΩKn+1 _ (f y)) (Kn→ΩKn+1 _ (g y)))
                         ∙ sym (Kn→ΩKn+1-hom _ (f y) (g y))) (~ j) i}))

Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ : (n m : ℕ)
  → GroupIso (coHomGr ((suc n) +' (suc m))
                  (S₊ (suc n) × S₊ (suc m)))
              ℤGroup
Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ zero m =
  compGroupIso (invGroupIso (Hⁿ-Sⁿ≅Hⁿ-S¹×Sⁿ m)) (Hⁿ-Sⁿ≅ℤ m)
Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ (suc n) m =
  compGroupIso
          (invGroupIso (×leftSuspensionIso n m))
            (Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ n m)

-- Proof that ⌣ respects generators for H²×H²→H⁴
-- Todo: generalise

H²-S²×S²-genₗ : coHom 2 (S₊ 2 × S₊ 2)
H²-S²×S²-genₗ = ∣ (λ x → ∣ fst x ∣) ∣₂

H²-S²×S²-genᵣ : coHom 2 (S₊ 2 × S₊ 2)
H²-S²×S²-genᵣ = ∣ (λ x → ∣ snd x ∣) ∣₂

H²-S²≅H⁴-S²×S² : GroupIso (coHomGr 2 (S₊ 2)) (coHomGr 4 (S₊ 2 × S₊ 2))
H²-S²≅H⁴-S²×S² = (compGroupIso (Hⁿ-Sⁿ≅Hⁿ-S¹×Sⁿ 1) (×leftSuspensionIso 0 1))

H²-S²≅H⁴-S²×S²⌣ :
  fun (fst (H²-S²≅H⁴-S²×S²)) ∣ ∣_∣ₕ ∣₂ ≡ H²-S²×S²-genₗ ⌣ H²-S²×S²-genᵣ
H²-S²≅H⁴-S²×S²⌣ =
  cong ∣_∣₂ (funExt (uncurry
    (λ { north y → refl
       ; south y → refl
       ; (merid a i) y j → Kn→ΩKn+1 3 (lem a y j) i})))
  where
  lem : (a : S¹) (y : S₊ 2)
      → Hⁿ-S¹×Sⁿ→Hⁿ-Sⁿ 1 ∣_∣ₕ a y ≡ _⌣ₖ_ {n = 1} {m = 2} ∣ a ∣ₕ ∣ y ∣ₕ
  lem base y = refl
  lem (loop i) y = refl

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --cubical --safe #-}

module Function where

open import Level
open import Path

infixr 9 _∘_ _∘′_
_∘_ : ∀ {A : Type a} {B : A → Type b} {C : {x : A} → B x → Type c} →
        (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
        ((x : A) → C (g x))
f ∘ g = λ x → f (g x)

_∘′_ : (B → C) → (A → B) → A → C
f ∘′ g = λ x → f (g x)

flip : ∀ {A : Type a} {B : Type b} {C : A → B → Type c} →
        ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
flip f = λ y x → f x y

id : ∀ {A : Type a} → A → A
id x = x

const : A → B → A
const x _ = x

infixr -1 _$_
_$_ : ∀ {A : Type a} {B : A → Type b}
      → (∀ (x : A) → B x)
      → (x : A)
      → B x
f $ x = f x

infixl 1 _⟨_⟩_
_⟨_⟩_ : A → (A → B → C) → B → C
x ⟨ f ⟩ y = f x y

infixl 0 _∋_
_∋_ : (A : Type a) → A → A
A ∋ x = x

infix 0 case_of_
case_of_ : A → (A → B) → B
case x of f = f x

record Reveal_·_is_ {A : Type a} {B : A → Type b} (f : (x : A) → B x) (x : A) (y : B x) : Type b where
  constructor 〖_〗
  field eq : f x ≡ y

inspect : {A : Type a} {B : A → Type b} (f : (x : A) → B x) (x : A) → Reveal f · x is f x
inspect f x = 〖 refl 〗

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module Structure.Type.Identity.Proofs.Eliminator where

import      Lvl
open import Functional using (_→ᶠ_ ; id ; _on₂_ ; swap ; apply)
open import Logic
open import Logic.Propositional
open import Logic.Propositional.Proofs.Structures
open import Structure.Categorical.Properties
open import Structure.Function
open import Structure.Operator
open import Structure.Groupoid
open import Structure.Setoid using (Equiv ; intro) renaming (_≡_ to _≡ₛ_)
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Relator.Properties.Proofs
open import Structure.Relator
open import Structure.Type.Identity
open import Structure.Type.Identity.Proofs
open import Syntax.Function
open import Syntax.Transitivity
open import Syntax.Type
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓₑ₁ ℓₑ₂ ℓₑ ℓₘₑ ℓₚ ℓₒ : Lvl.Level
private variable T A B : Type{ℓ}
private variable x y : T
private variable Id _≡_ _▫_ : T → T → Stmt{ℓ}

module Oper (Id : T → T → Type{ℓₑ}) ⦃ refl :  Reflexivity(Id) ⦄ ⦃ identElim : IdentityEliminator{ℓₚ = ℓₑ}(Id) ⦄ where
  open Symmetry    (identity-eliminator-to-symmetry     {Id = Id}) using () renaming (proof to sym)   public
  open Transitivity(identity-eliminator-to-transitivity {Id = Id}) using () renaming (proof to trans) public
  ftrans = identity-eliminator-to-flipped-transitivityᵣ ⦃ refl ⦄ ⦃ identElim ⦄

module Oper2 (Id : A → A → Type{ℓₑ}) ⦃ refl :  Reflexivity(Id) ⦄ ⦃ identElim : IdentityEliminator{ℓₚ = ℓₚ}(Id) ⦄ where
  open Reflexivity (refl) using () renaming (proof to refl)  public
  module _ (_▫_ : A → A → Type{ℓₚ}) ⦃ [▫]-refl : Reflexivity(_▫_) ⦄ where
    open _⊆₂_ identity-eliminator-to-reflexive-subrelation using () renaming (proof to sub) public
  module _ (_▫_ : B → B → Type{ℓₚ}) ⦃ [▫]-refl : Reflexivity(_▫_) ⦄ (f : A → B) where
    open _⊆₂_ (minimal-reflection-transport ⦃ minRefl = identity-eliminator-to-reflexive-subrelation ⦄ {_▫_ = _▫_} {f = f}) using () renaming (proof to transp) public

module _
  {Id : T → T → Type{ℓₑ}} ⦃ refle-T :  Reflexivity(Id) ⦄  ⦃ identElim-T : IdentityEliminator(Id) ⦄
  {_≡_ : ∀{T : Type{ℓₑ}} → T → T → Type{ℓₘₑ}}
  ⦃ identElimOfIntro : IdentityEliminationOfIntro(Id)(_≡_) ⦄
  where

  open Oper(Id)
  open Oper2{ℓₚ = ℓₑ}(Id)

  identity-eliminator-symmetry-of-refl : ∀{x} → (sym refl ≡ refl{x})
  identity-eliminator-symmetry-of-refl = idElimOfIntro(Id)(_≡_) (\{x y} _ → (Id y x)) refl

module _
  {Id : T → T → Type{ℓₑ₁}} ⦃ refle-T :  Reflexivity(Id) ⦄  ⦃ identElim-T : IdentityEliminator(Id) ⦄
  {_≡_ : ∀{T : Type{ℓₑ₂}} → T → T → Type{ℓₘₑ}}
  ⦃ identElimOfIntro : IdentityEliminationOfIntro(Id)(_≡_) ⦄
  {_▫_ : T → T → Type{ℓₑ₂}} ⦃ refl-op : Reflexivity(_▫_) ⦄
  where

  open Oper(Id)
  open Oper2{ℓₚ = ℓₑ₂}(Id)

  identity-eliminator-reflexive-subrelation-of-refl : ∀{x} → (sub(_▫_) refl ≡ reflexivity(_▫_){x})
  identity-eliminator-reflexive-subrelation-of-refl = idElimOfIntro(Id)(_≡_) (\{x y} _ → (x ▫ y)) (reflexivity(_▫_))

module _
  {Id : A → A → Type{ℓₑ₁}} ⦃ refle-A :  Reflexivity(Id) ⦄  ⦃ identElim-A : IdentityEliminator(Id) ⦄
  {_≡_ : ∀{T : Type{ℓₑ₂}} → T → T → Type{ℓₘₑ}}
  ⦃ identElimOfIntro : IdentityEliminationOfIntro(Id)(_≡_) ⦄
  {_▫_ : B → B → Type{ℓₑ₂}} ⦃ refle-B : Reflexivity(_▫_) ⦄
  {f : A → B}
  where

  open Oper(Id)
  open Oper2{ℓₚ = ℓₑ₂}(Id)

  identity-eliminator-transport-of-refl : ∀{a} → (transp(_▫_)(f) (refl{a}) ≡ reflexivity(_▫_) {f(a)})
  identity-eliminator-transport-of-refl {a} = identity-eliminator-reflexive-subrelation-of-refl {_≡_ = _≡_} {_▫_ = (_▫_) on₂ f} ⦃ on₂-reflexivity ⦄ {x = a}

module _
  {Id : T → T → Type{ℓₑ}}
    ⦃ refle-T :  Reflexivity(Id) ⦄
    ⦃ identElim-T : IdentityEliminator(Id) ⦄
  {_≡_ : ∀{T : Type{ℓₑ}} → T → T → Type{ℓₘₑ}}
    ⦃ refle-eq : ∀{T : Type} → Reflexivity(_≡_ {T = T}) ⦄
    ⦃ identElim-eq : ∀{T : Type} → IdentityEliminator{ℓₚ = ℓₘₑ}(_≡_ {T = T}) ⦄
  ⦃ identElimOfIntro : IdentityEliminationOfIntro(Id)(_≡_) ⦄
  where

  open Oper(Id)
  open Oper2{ℓₚ = ℓₑ}(Id)
  instance _ = identity-eliminator-to-reflexive-subrelation

  identity-eliminator-flipped-transitivityᵣ-of-refl : ∀{x} → (ftrans refl refl ≡ refl{x})
  identity-eliminator-flipped-transitivityᵣ-of-refl {z} = sub₂(_≡_)((_≡_) on₂ (apply refl)) ⦃ minimal-reflection-transport ⦄ identity-eliminator-transport-of-refl

  identity-eliminator-transitivity-of-refl : ∀{x} → (trans refl refl ≡ refl{x})
  identity-eliminator-transitivity-of-refl = transitivity(_≡_) ⦃ identity-eliminator-to-transitivity ⦄ p identity-eliminator-flipped-transitivityᵣ-of-refl where
    p : trans refl refl ≡ ftrans refl refl
    p = sub₂(_≡_)((_≡_) on₂ (p ↦ identity-eliminator-to-flipped-transitivityᵣ p refl)) ⦃ minimal-reflection-transport ⦄ identity-eliminator-symmetry-of-refl

module _
  ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
    ⦃ identElim-A : IdentityEliminator(Equiv._≡_ equiv-A) ⦄
  ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  {_≡_ : ∀{T : Type{ℓₑ₂}} → T → T → Type{ℓₘₑ}}
  ⦃ identElimOfIntro : IdentityEliminationOfIntro(Equiv._≡_ equiv-A)(_≡_) ⦄
  where

  open Reflexivity(Equiv.reflexivity equiv-A) using () renaming (proof to refl-A)
  open Reflexivity(Equiv.reflexivity equiv-B) using () renaming (proof to refl-B)
  instance _ = identity-eliminator-to-reflexive-subrelation
  instance _ = minimal-reflection-to-function

  identity-eliminator-function-of-refl : ∀{f : A → B}{a} → (congruence₁(f) (refl-A {a}) ≡ refl-B {f(a)})
  identity-eliminator-function-of-refl = identity-eliminator-transport-of-refl

module _
  ⦃ equiv-T : Equiv{ℓₑ₁}(T) ⦄
    ⦃ identElim-T : IdentityEliminator(Equiv._≡_ equiv-T) ⦄
  {_≡_ : ∀{T : Type{ℓₑ₂}} → T → T → Type{ℓₘₑ}}
    ⦃ refle-eq : ∀{T : Type} → Reflexivity(_≡_ {T = T}) ⦄
    ⦃ identElim-eq : ∀{T : Type} → IdentityEliminator{ℓₚ = ℓₘₑ}(_≡_ {T = T}) ⦄
  ⦃ identElimOfIntro : IdentityEliminationOfIntro(Equiv._≡_ equiv-T)(_≡_) ⦄
  where

  open Reflexivity(Equiv.reflexivity equiv-T) using () renaming (proof to refl)
  instance _ = identity-eliminator-to-reflexive-subrelation
  instance _ = minimal-reflection-to-relator

  identity-eliminator-relator-of-refl : ∀{P : T → Stmt}{x}{p : P(x)} → (substitute₁(P) refl p ≡ p)
  identity-eliminator-relator-of-refl {p = p} = sub₂(_≡_)((_≡_) on₂ (apply p)) ⦃ minimal-reflection-transport ⦄ identity-eliminator-transport-of-refl
module _
  {Id : T → T → Type{ℓₑ}}
    ⦃ refle-T :  Reflexivity(Id) ⦄
    ⦃ identElim-T : ∀{ℓₚ} → IdentityEliminator{ℓₚ = ℓₚ}(Id) ⦄
    -- ⦃ identElim₁-T : IdentityEliminator{ℓₚ = ℓₑ}(Id) ⦄
    -- ⦃ identElim₂-T : IdentityEliminator{ℓₚ = ℓₘₑ}(Id) ⦄
    -- ⦃ identElim₃-T : IdentityEliminator{ℓₚ = ℓₑ Lvl.⊔ ℓₘₑ}(Id) ⦄
  {_≡_ : ∀{T : Type{ℓₑ}} → T → T → Type{ℓₘₑ}}
    ⦃ refle-eq : ∀{T : Type} → Reflexivity(_≡_ {T = T}) ⦄
    ⦃ identElim-eq : ∀{T : Type} → IdentityEliminator{ℓₚ = ℓₘₑ}(_≡_ {T = T}) ⦄ -- TODO: Try to not have these and instead have the properties that are used
  ⦃ identElimOfIntro : IdentityEliminationOfIntro(Id)(_≡_) ⦄
  where

  open Reflexivity (refle-T)                                       using () renaming (proof to refl)
  open Symmetry    (identity-eliminator-to-symmetry     {Id = Id}) using () renaming (proof to sym)
  open Transitivity(identity-eliminator-to-transitivity {Id = Id}) using () renaming (proof to trans)
  instance _ = identity-eliminator-to-reflexive-subrelation
  instance _ = \{T} → identity-eliminator-to-symmetry     {Id = _≡_ {T = T}} ⦃ refl = refle-eq ⦄ ⦃ identElim = identElim-eq ⦄
  instance _ = \{T} → identity-eliminator-to-transitivity {Id = _≡_ {T = T}} ⦃ refl = refle-eq ⦄ ⦃ identElim = identElim-eq ⦄
  instance _ = \{T} → Structure.Setoid.intro(_) ⦃ identity-eliminator-to-equivalence {Id = _≡_ {T = T}} ⦃ refl = refle-eq ⦄ ⦃ identElim = identElim-eq ⦄ ⦄

  identity-eliminator-identityₗ : ∀{x y}{p : Id x y} → (trans refl p ≡ p)
  identity-eliminator-identityₗ {p = p} = idElim(Id) (p ↦ (trans refl p ≡ p)) identity-eliminator-transitivity-of-refl p

  identity-eliminator-identityᵣ : ∀{x y}{p : Id x y} → (trans p refl ≡ p)
  identity-eliminator-identityᵣ {p = p} = idElim(Id) (p ↦ (trans p refl ≡ p)) identity-eliminator-transitivity-of-refl p

  identity-eliminator-associativity : ∀{x y z w}{p : Id x y}{q : Id y z}{r : Id z w} → (trans (trans p q) r ≡ trans p (trans q r))
  identity-eliminator-associativity {p = p} {q = q} {r = r} =
    idElim(Id)
      (p ↦ ∀ q r → (trans (trans p q) r ≡ trans p (trans q r)))
      (q ↦ r ↦ (
        trans (trans refl q) r 🝖[ _≡_ ]-[ sub₂(_≡_)((_≡_) on₂ (expr ↦ trans expr r)) ⦃ identity-eliminator-to-reflexive-subrelation ⦃ refl = on₂-reflexivity ⦄ ⦄ identity-eliminator-identityₗ ]
        trans q r              🝖[ _≡_ ]-[ identity-eliminator-identityₗ ]-sym
        trans refl (trans q r) 🝖-end
      ))
      p q r

  identity-eliminator-inverseₗ : ∀{x y}{p : Id x y} → (trans (sym p) p ≡ refl)
  identity-eliminator-inverseₗ {p = p} =
    idElim(Id)
      (p ↦ trans (sym p) p ≡ refl)
      (
        trans (sym refl) refl 🝖[ _≡_ ]-[ identity-eliminator-identityᵣ ]
        sym refl              🝖[ _≡_ ]-[ identity-eliminator-symmetry-of-refl ]
        refl                  🝖-end
      )
      p

  identity-eliminator-inverseᵣ : ∀{x y}{p : Id x y} → (trans p (sym p) ≡ refl)
  identity-eliminator-inverseᵣ {p = p} =
    idElim(Id)
      (p ↦ trans p (sym p) ≡ refl)
      (
        trans refl (sym refl) 🝖[ _≡_ ]-[ identity-eliminator-identityₗ ]
        sym refl              🝖[ _≡_ ]-[ identity-eliminator-symmetry-of-refl ]
        refl                  🝖-end
      )
      p

  identity-eliminator-categorical-identityₗ : Morphism.Identityₗ{Obj = T} (\{x} → swap(trans{x})) (refl)
  identity-eliminator-categorical-identityₗ = Morphism.intro identity-eliminator-identityᵣ

  identity-eliminator-categorical-identityᵣ : Morphism.Identityᵣ{Obj = T} (\{x} → swap(trans{x})) (refl)
  identity-eliminator-categorical-identityᵣ = Morphism.intro identity-eliminator-identityₗ

  identity-eliminator-categorical-identity : Morphism.Identity{Obj = T} (\{x} → swap(trans{x})) (refl)
  identity-eliminator-categorical-identity = [∧]-intro identity-eliminator-categorical-identityₗ identity-eliminator-categorical-identityᵣ

  identity-eliminator-categorical-associativity : Morphism.Associativity{Obj = T} (\{x} → swap(trans{x}))
  identity-eliminator-categorical-associativity = Morphism.intro (symmetry(_≡_) identity-eliminator-associativity)

  identity-eliminator-categorical-inverterₗ : Polymorphism.Inverterₗ{Obj = T} (\{x} → swap(trans{x})) (refl) (sym)
  identity-eliminator-categorical-inverterₗ = Polymorphism.intro identity-eliminator-inverseᵣ

  identity-eliminator-categorical-inverterᵣ : Polymorphism.Inverterᵣ{Obj = T} (\{x} → swap(trans{x})) (refl) (sym)
  identity-eliminator-categorical-inverterᵣ = Polymorphism.intro identity-eliminator-inverseₗ

  identity-eliminator-categorical-inverter : Polymorphism.Inverter{Obj = T} (\{x} → swap(trans{x})) (refl) (sym)
  identity-eliminator-categorical-inverter = [∧]-intro identity-eliminator-categorical-inverterₗ identity-eliminator-categorical-inverterᵣ

  identity-eliminator-groupoid : Groupoid(Id)
  Groupoid._∘_ identity-eliminator-groupoid = swap(trans)
  Groupoid.id  identity-eliminator-groupoid = refl
  Groupoid.inv identity-eliminator-groupoid = sym
  Groupoid.associativity  identity-eliminator-groupoid = identity-eliminator-categorical-associativity
  Groupoid.identity       identity-eliminator-groupoid = identity-eliminator-categorical-identity
  Groupoid.inverter       identity-eliminator-groupoid = identity-eliminator-categorical-inverter
  Groupoid.binaryOperator identity-eliminator-groupoid = intro a where postulate a : ∀{a} → a -- TODO

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- Well-founded induction
------------------------------------------------------------------------

-- I want universe polymorphism.

open import Relation.Binary

module Induction1.WellFounded {a : Set} (_<_ : Rel a) where

open import Induction1

-- When using well-founded recursion you can recurse arbitrarily, as
-- long as the arguments become smaller, and "smaller" is
-- well-founded.

WfRec : RecStruct a
WfRec P x = ∀ y → y < x → P y

-- The accessibility predicate encodes what it means to be
-- well-founded; if all elements are accessible, then _<_ is
-- well-founded.

data Acc (x : a) : Set₁ where
  acc : (rs : WfRec Acc x) → Acc x

-- Well-founded induction for the subset of accessible elements:

module Some where

  wfRec-builder : SubsetRecursorBuilder Acc WfRec
  wfRec-builder P f x (acc rs) = λ y y<x →
    f y (wfRec-builder P f y (rs y y<x))

  wfRec : SubsetRecursor Acc WfRec
  wfRec = subsetBuild wfRec-builder

-- Well-founded induction for all elements, assuming they are all
-- accessible:

module All (allAcc : ∀ x → Acc x) where

  wfRec-builder : RecursorBuilder WfRec
  wfRec-builder P f x = Some.wfRec-builder P f x (allAcc x)

  wfRec : Recursor WfRec
  wfRec = build wfRec-builder

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module HasDecidableSubstantiveDischarge where

open import OscarPrelude
open import HasSubstantiveDischarge

record HasDecidableSubstantiveDischarge (A : Set) : Set₁
 where
  field
    ⦃ hasSubstantiveDischarge ⦄ : HasSubstantiveDischarge A
    _≽?_ : (+ - : A) → Dec $ + ≽ -

open HasDecidableSubstantiveDischarge ⦃ … ⦄ public

{-# DISPLAY HasDecidableSubstantiveDischarge._≽?_ _ = _≽?_ #-}

open import Membership

_⋆≽?_ : ∀ {A} ⦃ _ : HasDecidableSubstantiveDischarge A ⦄ → (+s : List A) → (- : A) → Dec (+s ⋆≽ -)
_⋆≽?_ [] - = no λ { (_ , () , _)}
_⋆≽?_ (+ ∷ +s) - with + ≽? -
… | yes +≽- = yes $ _ , zero , +≽-
… | no +⋡- with +s ⋆≽? -
… | yes (+' , +'∈+s , +'≽-) = yes $ _ , suc +'∈+s , +'≽-
… | no +s⋡- = no λ { (_ , zero , +≽-) → +⋡- +≽-
                   ; (+' , suc +'∈+s , +'≽-) → +s⋡- $ _ , +'∈+s , +'≽- }

_≽⋆?_ : ∀ {A} ⦃ _ : HasDecidableSubstantiveDischarge A ⦄ → (+ : A) → (-s : List A) → Dec (+ ≽⋆ -s)
+ ≽⋆? [] = no (λ { (fst₁ , () , snd₁)})
+ ≽⋆? (- ∷ -s) with + ≽? -
… | yes +≽- = yes (_ , zero , +≽-)
… | no +⋡- with + ≽⋆? -s
… | yes (_ , i∈-s , +≽⋆i) = yes (_ , suc i∈-s , +≽⋆i)
… | no +⋡⋆-s = no (λ { (_ , zero , +≽-) → +⋡- +≽-
                     ; (_ , suc -'∈-s , +≽-') → +⋡⋆-s (_ , -'∈-s , +≽-')})

_⋆≽⋆?_ : ∀ {A} ⦃ _ : HasDecidableSubstantiveDischarge A ⦄ → (+s : List A) → (-s : List A) → Dec (+s ⋆≽⋆ -s)
_⋆≽⋆?_ +s [] = yes λ _ ()
_⋆≽⋆?_ +s (- ∷ -s) with +s ⋆≽? -
… | no +s⋡- = no λ +s≽-∷-s → +s⋡- $ +s≽-∷-s (-) zero
… | yes +s≽- with +s ⋆≽⋆? -s
… | yes +s≽-s = yes λ { _ zero → +s≽-
                      ; -' (suc -'∈-∷-s) → +s≽-s -' -'∈-∷-s }
… | no +s⋡-s = no λ +s≽-∷-s → +s⋡-s λ +' +'∈-s → +s≽-∷-s +' (suc +'∈-s)

open import HasNegation

◁?_ : ∀ {+} ⦃ _ : HasDecidableSubstantiveDischarge (+) ⦄
            → (+s : List +) → Dec $ ◁ +s
◁? [] = no λ {(_ , () , _)}
◁?_ (+ ∷ +s) with +s ⋆≽? ~ +
… | yes (_ , +'∈+s , +'≽~+) = yes $ _ , zero , _ , suc +'∈+s , +'≽~+
… | no +s⋆⋡~+ with ~ + ≽⋆? +s
… | yes (_ , c∈+s , ~+≽c) = yes (_ , suc c∈+s , _ , zero , ≽-contrapositive (+) _ ~+≽c)
… | no ~+⋡⋆+s with ◁? +s
… | yes (s , s∈+s , c , c∈+s , c≽~s) = yes $ _ , suc s∈+s , _ , suc c∈+s , c≽~s
… | no ⋪+s = no
  λ { (_ , zero , _ , zero , c≽~s) → ≽-consistent (+) (+) (≽-reflexive +) c≽~s
  ; (_ , zero , c , suc c∈+s , c≽~s) → +s⋆⋡~+ (_ , c∈+s , c≽~s)
  ; (s , suc s∈+s , .+ , zero , +≽~s) → ~+⋡⋆+s (_ , s∈+s , ≽-contrapositive' (+) s +≽~s)
  ; (s , suc s∈+s , c , suc c∈+s , c≽~s) → ⋪+s (_ , s∈+s , _ , c∈+s , c≽~s) }


text:
module HasDecidableVacuousDischarge where

open import OscarPrelude
--open import HasVacuousDischarge
open import HasSubstantiveDischarge
open import HasNegation

record HasDecidableVacuousDischarge (A : Set) : Set₁
 where
  field
    -- ⦃ hasVacuousDischarge ⦄ : HasVacuousDischarge A
    ⦃ hasNegation ⦄ : HasNegation A
    ⦃ hasSubstantiveDischarge ⦄ : HasSubstantiveDischarge A
    ◁?_ : (x : List A) → Dec $ ◁ x

open HasDecidableVacuousDischarge ⦃ … ⦄ public

{-# DISPLAY HasDecidableVacuousDischarge.◁?_ _ = ◁?_ #-}


text:
-- Monoidal categories
{-# OPTIONS --safe #-}

module Cubical.Categories.Monoidal where

open import Cubical.Categories.Monoidal.Base public
open import Cubical.Categories.Monoidal.Enriched public

max_stars_repo_name: FernandoLarrain/cubical


text:
------------------------------------------------------------------------------
-- All the predicate logic modules
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOL.Everything where

open import FOL.Base
open import FOL.ExclusiveDisjunction.Base
open import FOL.ExclusiveDisjunction.TheoremsATP
open import FOL.ExclusiveDisjunction.TheoremsI
open import FOL.NonEmptyDomain.TheoremsATP
open import FOL.NonEmptyDomain.TheoremsI
open import FOL.NonIntuitionistic.TheoremsATP
open import FOL.NonIntuitionistic.TheoremsI
open import FOL.PropositionalLogic.TheoremsATP
open import FOL.PropositionalLogic.TheoremsI
open import FOL.SchemataATP
open import FOL.TheoremsATP
open import FOL.TheoremsI

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- Listed finite subsets
------------------------------------------------------------------------

-- Based on Frumin, Geuvers, Gondelman and van der Weide's "Finite
-- Sets in Homotopy Type Theory".

{-# OPTIONS --cubical --safe #-}

import Equality.Path as P

module Finite-subset.Listed
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

open import Dec
open import Logical-equivalence using (_⇔_)
open import Prelude as P hiding ([_,_]; swap)

open import Bag-equivalence equality-with-J as BE using (_∼[_]_; set)
open import Bijection equality-with-J as Bijection using (_↔_)
open import Equality.Decision-procedures equality-with-J
open import Equality.Path.Isomorphisms eq
open import Equality.Path.Isomorphisms.Univalence eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Erased.Cubical eq as EC
  using (Erased; [_]; Dec-Erased; Dec→Dec-Erased)
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as Trunc
  using (∥_∥; ∣_∣; _∥⊎∥_)
open import Injection equality-with-J using (Injective)
import List equality-with-J as L
import Maybe equality-with-J as Maybe
open import Monad equality-with-J as M using (Raw-monad; Monad; _=<<_)
open import Nat equality-with-J as Nat using (_<_)
open import Quotient eq as Q using (_/_)
open import Surjection equality-with-J using (_↠_)
import Univalence-axiom equality-with-J as Univ

private
  variable
    a b                                  : Level
    A B                                  : Type a
    H ms p q x x₁ x₂ xs y y₁ y₂ ys z _≟_ : A
    P                                    : A → Type p
    f g                                  : (x : A) → P x
    m n                                  : ℕ

------------------------------------------------------------------------
-- Listed finite subsets

-- Listed finite subsets of a given type.

infixr 5 _∷_

data Finite-subset-of (A : Type a) : Type a where
  []      : Finite-subset-of A
  _∷_     : A → Finite-subset-of A → Finite-subset-of A
  dropᴾ   : x ∷ x ∷ y P.≡ x ∷ y
  swapᴾ   : x ∷ y ∷ z P.≡ y ∷ x ∷ z
  is-setᴾ : P.Is-set (Finite-subset-of A)

-- Variants of some of the constructors.

drop :
  {x : A} {y : Finite-subset-of A} →
  x ∷ x ∷ y ≡ x ∷ y
drop = _↔_.from ≡↔≡ dropᴾ

swap :
  {x y : A} {z : Finite-subset-of A} →
  x ∷ y ∷ z ≡ y ∷ x ∷ z
swap = _↔_.from ≡↔≡ swapᴾ

is-set : Is-set (Finite-subset-of A)
is-set =
  _↔_.from (H-level↔H-level 2) Finite-subset-of.is-setᴾ

------------------------------------------------------------------------
-- Eliminators

-- A dependent eliminator, expressed using paths.

record Elimᴾ {A : Type a} (P : Finite-subset-of A → Type p) :
             Type (a ⊔ p) where
  no-eta-equality
  field
    []ʳ     : P []
    ∷ʳ      : ∀ x → P y → P (x ∷ y)
    dropʳ   : ∀ x (p : P y) →
              P.[ (λ i → P (dropᴾ {x = x} {y = y} i)) ]
                ∷ʳ x (∷ʳ x p) ≡ ∷ʳ x p
    swapʳ   : ∀ x y (p : P z) →
              P.[ (λ i → P (swapᴾ {x = x} {y = y} {z = z} i)) ]
                ∷ʳ x (∷ʳ y p) ≡ ∷ʳ y (∷ʳ x p)
    is-setʳ : ∀ x → P.Is-set (P x)

open Elimᴾ public

elimᴾ : Elimᴾ P → (x : Finite-subset-of A) → P x
elimᴾ {A = A} {P = P} e = helper
  where
  module E = Elimᴾ e

  helper : (x : Finite-subset-of A) → P x
  helper []      = E.[]ʳ
  helper (x ∷ y) = E.∷ʳ x (helper y)

  helper (dropᴾ {x = x} {y = y} i) =
    E.dropʳ x (helper y) i

  helper (swapᴾ {x = x} {y = y} {z = z} i) =
    E.swapʳ x y (helper z) i

  helper (is-setᴾ x y i j) =
    P.heterogeneous-UIP
      E.is-setʳ (Finite-subset-of.is-setᴾ x y)
      (λ i → helper (x i)) (λ i → helper (y i)) i j

-- A non-dependent eliminator, expressed using paths.

record Recᴾ (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    []ʳ     : B
    ∷ʳ      : A → Finite-subset-of A → B → B
    dropʳ   : ∀ x y p →
              ∷ʳ x (x ∷ y) (∷ʳ x y p) P.≡ ∷ʳ x y p
    swapʳ   : ∀ x y z p →
              ∷ʳ x (y ∷ z) (∷ʳ y z p) P.≡ ∷ʳ y (x ∷ z) (∷ʳ x z p)
    is-setʳ : P.Is-set B

open Recᴾ public

recᴾ : Recᴾ A B → Finite-subset-of A → B
recᴾ r = elimᴾ e
  where
  module R = Recᴾ r

  e : Elimᴾ _
  e .[]ʳ               = R.[]ʳ
  e .∷ʳ {y = y} x      = R.∷ʳ x y
  e .dropʳ {y = y} x   = R.dropʳ x y
  e .swapʳ {z = z} x y = R.swapʳ x y z
  e .is-setʳ _         = R.is-setʳ

-- A dependent eliminator, expressed using equality.

record Elim {A : Type a} (P : Finite-subset-of A → Type p) :
            Type (a ⊔ p) where
  no-eta-equality
  field
    []ʳ     : P []
    ∷ʳ      : ∀ x → P y → P (x ∷ y)
    dropʳ   : ∀ x (p : P y) →
              subst P (drop {x = x} {y = y}) (∷ʳ x (∷ʳ x p)) ≡ ∷ʳ x p
    swapʳ   : ∀ x y (p : P z) →
              subst P (swap {x = x} {y = y} {z = z}) (∷ʳ x (∷ʳ y p)) ≡
              ∷ʳ y (∷ʳ x p)
    is-setʳ : ∀ x → Is-set (P x)

open Elim public

elim : Elim P → (x : Finite-subset-of A) → P x
elim e = elimᴾ e′
  where
  module E = Elim e

  e′ : Elimᴾ _
  e′ .[]ʳ         = E.[]ʳ
  e′ .∷ʳ          = E.∷ʳ
  e′ .dropʳ x p   = subst≡→[]≡ (E.dropʳ x p)
  e′ .swapʳ x y p = subst≡→[]≡ (E.swapʳ x y p)
  e′ .is-setʳ x   = _↔_.to (H-level↔H-level 2) (E.is-setʳ x)

-- A non-dependent eliminator, expressed using equality.

record Rec (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    []ʳ     : B
    ∷ʳ      : A → Finite-subset-of A → B → B
    dropʳ   : ∀ x y p →
              ∷ʳ x (x ∷ y) (∷ʳ x y p) ≡ ∷ʳ x y p
    swapʳ   : ∀ x y z p →
              ∷ʳ x (y ∷ z) (∷ʳ y z p) ≡ ∷ʳ y (x ∷ z) (∷ʳ x z p)
    is-setʳ : Is-set B

open Rec public

rec : Rec A B → Finite-subset-of A → B
rec r = recᴾ r′
  where
  module R = Rec r

  r′ : Recᴾ _ _
  r′ .[]ʳ           = R.[]ʳ
  r′ .∷ʳ            = R.∷ʳ
  r′ .dropʳ x y p   = _↔_.to ≡↔≡ (R.dropʳ x y p)
  r′ .swapʳ x y z p = _↔_.to ≡↔≡ (R.swapʳ x y z p)
  r′ .is-setʳ       = _↔_.to (H-level↔H-level 2) R.is-setʳ

-- A dependent eliminator for propositions.

record Elim-prop
         {A : Type a} (P : Finite-subset-of A → Type p) :
         Type (a ⊔ p) where
  no-eta-equality
  field
    []ʳ             : P []
    ∷ʳ              : ∀ x → P y → P (x ∷ y)
    is-propositionʳ : ∀ x → Is-proposition (P x)

open Elim-prop public

elim-prop : Elim-prop P → (x : Finite-subset-of A) → P x
elim-prop e = elim e′
  where
  module E = Elim-prop e

  e′ : Elim _
  e′ .[]ʳ         = E.[]ʳ
  e′ .∷ʳ          = E.∷ʳ
  e′ .dropʳ _ _   = E.is-propositionʳ _ _ _
  e′ .swapʳ _ _ _ = E.is-propositionʳ _ _ _
  e′ .is-setʳ _   = mono₁ 1 (E.is-propositionʳ _)

-- A non-dependent eliminator for propositions.

record Rec-prop (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    []ʳ             : B
    ∷ʳ              : A → Finite-subset-of A → B → B
    is-propositionʳ : Is-proposition B

open Rec-prop public

rec-prop : Rec-prop A B → Finite-subset-of A → B
rec-prop r = elim-prop e
  where
  module R = Rec-prop r

  e : Elim-prop _
  e .[]ʳ               = R.[]ʳ
  e .∷ʳ {y = y} x      = R.∷ʳ x y
  e .is-propositionʳ _ = R.is-propositionʳ

------------------------------------------------------------------------
-- Some operations

-- Singleton subsets.

singleton : A → Finite-subset-of A
singleton x = x ∷ []

-- The union of two finite subsets.

infixr 5 _∪_

_∪_ :
  Finite-subset-of A → Finite-subset-of A →
  Finite-subset-of A
[] ∪ y      = y
(x ∷ y) ∪ z = x ∷ (y ∪ z)

dropᴾ {x = x} {y = y} i ∪ z =
  dropᴾ {x = x} {y = y ∪ z} i

swapᴾ {x = x} {y = y} {z = z} i ∪ u =
  swapᴾ {x = x} {y = y} {z = z ∪ u} i

is-setᴾ x y i j ∪ z =
  is-setᴾ (λ i → x i ∪ z) (λ i → y i ∪ z) i j

-- [] is a right identity for _∪_.

∪[] :
  (x : Finite-subset-of A) →
  x ∪ [] ≡ x
∪[] = elim-prop e
  where
  e : Elim-prop _
  e .is-propositionʳ _ = is-set
  e .[]ʳ               = refl _
  e .∷ʳ {y = y} x hyp  =
    x ∷ y ∪ []  ≡⟨ cong (x ∷_) hyp ⟩∎
    x ∷ y        ∎

-- A lemma relating _∪_ and _∷_.

∪∷ :
  (x : Finite-subset-of A) →
  x ∪ (y ∷ z) ≡ y ∷ x ∪ z
∪∷ {y = y} {z = z} = elim-prop e
  where
  e : Elim-prop _
  e .is-propositionʳ _ = is-set

  e .[]ʳ = refl _

  e .∷ʳ {y = u} x hyp =
    (x ∷ u) ∪ (y ∷ z)  ≡⟨⟩
    x ∷ u ∪ (y ∷ z)    ≡⟨ cong (x ∷_) hyp ⟩
    x ∷ y ∷ u ∪ z      ≡⟨ swap ⟩
    y ∷ x ∷ u ∪ z      ≡⟨⟩
    y ∷ (x ∷ u) ∪ z    ∎

-- Union is associative.

assoc :
  (x : Finite-subset-of A) →
  x ∪ (y ∪ z) ≡ (x ∪ y) ∪ z
assoc {y = y} {z = z} = elim-prop e
  where
  e : Elim-prop _
  e .is-propositionʳ _ = is-set

  e .[]ʳ = refl _

  e .∷ʳ {y = u} x hyp =
    x ∷ u ∪ (y ∪ z)  ≡⟨ cong (x ∷_) hyp ⟩∎
    x ∷ (u ∪ y) ∪ z  ∎

-- Union is commutative.

comm :
  (x : Finite-subset-of A) →
  x ∪ y ≡ y ∪ x
comm {y = y} = elim-prop e
  where
  e : Elim-prop _
  e .is-propositionʳ _ = is-set

  e .[]ʳ =
    [] ∪ y  ≡⟨⟩
    y       ≡⟨ sym (∪[] y) ⟩∎
    y ∪ []  ∎

  e .∷ʳ {y = z} x hyp =
    x ∷ z ∪ y    ≡⟨ cong (x ∷_) hyp ⟩
    x ∷ y ∪ z    ≡⟨ sym (∪∷ y) ⟩∎
    y ∪ (x ∷ z)  ∎

-- Union is idempotent.

idem : (x : Finite-subset-of A) → x ∪ x ≡ x
idem = elim-prop e
  where
  e : Elim-prop _
  e .[]ʳ =
    [] ∪ []  ≡⟨⟩
    []       ∎

  e .∷ʳ {y = y} x hyp =
    (x ∷ y) ∪ (x ∷ y)  ≡⟨⟩
    x ∷ y ∪ x ∷ y      ≡⟨ cong (_ ∷_) (∪∷ y) ⟩
    x ∷ x ∷ y ∪ y      ≡⟨ drop ⟩
    x ∷ y ∪ y          ≡⟨ cong (_ ∷_) hyp ⟩∎
    x ∷ y              ∎

  e .is-propositionʳ = λ _ → is-set

-- Union distributes from the left and right over union.

∪-distrib-left : ∀ x → x ∪ (y ∪ z) ≡ (x ∪ y) ∪ (x ∪ z)
∪-distrib-left {y = y} {z = z} x =
  x ∪ (y ∪ z)        ≡⟨ cong (_∪ _) $ sym (idem x) ⟩
  (x ∪ x) ∪ (y ∪ z)  ≡⟨ sym $ assoc x ⟩
  x ∪ (x ∪ (y ∪ z))  ≡⟨ cong (x ∪_) $ assoc x ⟩
  x ∪ ((x ∪ y) ∪ z)  ≡⟨ cong ((x ∪_) ∘ (_∪ _)) $ comm x ⟩
  x ∪ ((y ∪ x) ∪ z)  ≡⟨ cong (x ∪_) $ sym $ assoc y ⟩
  x ∪ (y ∪ (x ∪ z))  ≡⟨ assoc x ⟩∎
  (x ∪ y) ∪ (x ∪ z)  ∎

∪-distrib-right : ∀ x → (x ∪ y) ∪ z ≡ (x ∪ z) ∪ (y ∪ z)
∪-distrib-right {y = y} {z = z} x =
  (x ∪ y) ∪ z        ≡⟨ comm (x ∪ _) ⟩
  z ∪ (x ∪ y)        ≡⟨ ∪-distrib-left z ⟩
  (z ∪ x) ∪ (z ∪ y)  ≡⟨ cong₂ _∪_ (comm z) (comm z) ⟩∎
  (x ∪ z) ∪ (y ∪ z)  ∎

-- A map function.

map : (A → B) → Finite-subset-of A → Finite-subset-of B
map f = recᴾ r
  where
  r : Recᴾ _ _
  r .[]ʳ           = []
  r .∷ʳ x _ y      = f x ∷ y
  r .dropʳ _ _ _   = dropᴾ
  r .swapʳ _ _ _ _ = swapᴾ
  r .is-setʳ       = is-setᴾ

-- Join.

join : Finite-subset-of (Finite-subset-of A) → Finite-subset-of A
join = rec r
  where
  r : Rec _ _
  r .[]ʳ           = []
  r .∷ʳ x _        = x ∪_
  r .dropʳ x y z   = x ∪ x ∪ z    ≡⟨ assoc x ⟩
                     (x ∪ x) ∪ z  ≡⟨ cong (_∪ _) (idem x) ⟩∎
                     x ∪ z        ∎
  r .swapʳ x y z u = x ∪ y ∪ u    ≡⟨ assoc x ⟩
                     (x ∪ y) ∪ u  ≡⟨ cong (_∪ _) (comm x) ⟩
                     (y ∪ x) ∪ u  ≡⟨ sym (assoc y) ⟩∎
                     y ∪ x ∪ u    ∎
  r .is-setʳ       = is-set

-- A universe-polymorphic variant of bind.

infixl 5 _>>=′_

_>>=′_ :
  Finite-subset-of A → (A → Finite-subset-of B) → Finite-subset-of B
x >>=′ f = join (map f x)

-- Bind distributes from the right over union.

>>=-right-distributive :
  ∀ x → (x ∪ y) >>=′ f ≡ (x >>=′ f) ∪ (y >>=′ f)
>>=-right-distributive {y = y} {f = f} = elim-prop e
  where
  e : Elim-prop _
  e .[]ʳ               = refl _
  e .is-propositionʳ _ = is-set
  e .∷ʳ {y = z} x hyp  =
    ((x ∷ z) ∪ y) >>=′ f             ≡⟨⟩
    f x ∪ ((z ∪ y) >>=′ f)           ≡⟨ cong (f x ∪_) hyp ⟩
    f x ∪ ((z >>=′ f) ∪ (y >>=′ f))  ≡⟨ assoc (f x) ⟩
    (f x ∪ (z >>=′ f)) ∪ (y >>=′ f)  ≡⟨⟩
    ((x ∷ z) >>=′ f) ∪ (y >>=′ f)    ∎

-- Bind distributes from the left over union.

>>=-left-distributive :
  ∀ x → (x >>=′ λ x → f x ∪ g x) ≡ (x >>=′ f) ∪ (x >>=′ g)
>>=-left-distributive {f = f} {g = g} = elim-prop e
  where
  e : Elim-prop _
  e .[]ʳ               = refl _
  e .is-propositionʳ _ = is-set
  e .∷ʳ {y = y} x hyp  =
    (x ∷ y) >>=′ (λ x → f x ∪ g x)           ≡⟨⟩
    (f x ∪ g x) ∪ (y >>=′ λ x → f x ∪ g x)   ≡⟨ cong ((f x ∪ g x) ∪_) hyp ⟩
    (f x ∪ g x) ∪ ((y >>=′ f) ∪ (y >>=′ g))  ≡⟨ sym (assoc (f x)) ⟩
    f x ∪ (g x ∪ ((y >>=′ f) ∪ (y >>=′ g)))  ≡⟨ cong (f x ∪_) (assoc (g x)) ⟩
    f x ∪ ((g x ∪ (y >>=′ f)) ∪ (y >>=′ g))  ≡⟨ cong ((f x ∪_) ∘ (_∪ (y >>=′ g))) (comm (g x)) ⟩
    f x ∪ (((y >>=′ f) ∪ g x) ∪ (y >>=′ g))  ≡⟨ cong (f x ∪_) (sym (assoc (y >>=′ f))) ⟩
    f x ∪ ((y >>=′ f) ∪ (g x ∪ (y >>=′ g)))  ≡⟨ assoc (f x) ⟩
    (f x ∪ (y >>=′ f)) ∪ (g x ∪ (y >>=′ g))  ≡⟨⟩
    ((x ∷ y) >>=′ f) ∪ ((x ∷ y) >>=′ g)      ∎

-- Monad laws.

singleton->>= :
  (f : A → Finite-subset-of B) →
  singleton x >>=′ f ≡ f x
singleton->>= {x = x} f =
  f x ∪ []  ≡⟨ ∪[] _ ⟩∎
  f x       ∎

>>=-singleton : x >>=′ singleton ≡ x
>>=-singleton = elim-prop e _
  where
  e : Elim-prop (λ x → x >>=′ singleton ≡ x)
  e .[]ʳ               = refl _
  e .is-propositionʳ _ = is-set
  e .∷ʳ {y = y} x hyp  =
    x ∷ (y >>=′ singleton)  ≡⟨ cong (_ ∷_) hyp ⟩∎
    x ∷ y                   ∎

>>=-assoc : ∀ x → x >>=′ (λ x → f x >>=′ g) ≡ x >>=′ f >>=′ g
>>=-assoc {f = f} {g = g} = elim-prop e
  where
  e : Elim-prop _
  e .[]ʳ               = refl _
  e .is-propositionʳ _ = is-set
  e .∷ʳ {y = y} x hyp  =
    (x ∷ y) >>=′ (λ x → f x >>=′ g)           ≡⟨⟩
    (f x >>=′ g) ∪ (y >>=′ λ x → f x >>=′ g)  ≡⟨ cong ((f x >>=′ g) ∪_) hyp ⟩
    (f x >>=′ g) ∪ (y >>=′ f >>=′ g)          ≡⟨ sym (>>=-right-distributive (f x)) ⟩
    (f x ∪ (y >>=′ f)) >>=′ g                 ≡⟨⟩
    (x ∷ y) >>=′ f >>=′ g                     ∎

-- A monad instance.

instance

  raw-monad : Raw-monad {d = a} Finite-subset-of
  raw-monad .M.return = singleton
  raw-monad .M._>>=_  = _>>=′_

  monad : Monad {d = a} Finite-subset-of
  monad .M.Monad.raw-monad           = raw-monad
  monad .M.Monad.left-identity _     = singleton->>=
  monad .M.Monad.right-identity _    = >>=-singleton
  monad .M.Monad.associativity x _ _ = >>=-assoc x

------------------------------------------------------------------------
-- Membership

private

  -- Membership is used to define _∈_ and ∈-propositional below.

  Membership : {A : Type a} → A → Finite-subset-of A → Proposition a
  Membership x = rec r
    where
    r : Rec _ _
    r .[]ʳ = ⊥ , ⊥-propositional

    r .∷ʳ y z (x∈z , _) =
      (x ≡ y ∥⊎∥ x∈z) , Trunc.truncation-is-proposition

    r .dropʳ y z (P , P-prop) =
      _↔_.to (ignore-propositional-component
                (H-level-propositional ext 1)) $
      Univ.≃⇒≡ univ
        (x ≡ y ∥⊎∥ x ≡ y ∥⊎∥ P    ↔⟨ Trunc.∥⊎∥-assoc ⟩
         (x ≡ y ∥⊎∥ x ≡ y) ∥⊎∥ P  ↔⟨ Trunc.idempotent Trunc.∥⊎∥-cong F.id ⟩
         ∥ x ≡ y ∥ ∥⊎∥ P          ↔⟨ inverse Trunc.truncate-left-∥⊎∥ ⟩□
         x ≡ y ∥⊎∥ P              □)

    r .swapʳ y z u (P , P-prop) =
      _↔_.to (ignore-propositional-component
                (H-level-propositional ext 1)) $
      Univ.≃⇒≡ univ
        (x ≡ y ∥⊎∥ x ≡ z ∥⊎∥ P    ↔⟨ Trunc.∥⊎∥-assoc ⟩
         (x ≡ y ∥⊎∥ x ≡ z) ∥⊎∥ P  ↔⟨ (Trunc.∥⊎∥-comm Trunc.∥⊎∥-cong F.id) ⟩
         (x ≡ z ∥⊎∥ x ≡ y) ∥⊎∥ P  ↔⟨ inverse Trunc.∥⊎∥-assoc ⟩□
         x ≡ z ∥⊎∥ x ≡ y ∥⊎∥ P    □)

    r .is-setʳ = Univ.∃-H-level-H-level-1+ ext univ 1

-- Membership.
--
-- The type is wrapped to make it easier for Agda to infer the subset
-- argument.

private
 module Dummy where

  infix 4 _∈_

  record _∈_ {A : Type a} (x : A) (y : Finite-subset-of A) : Type a where
    constructor box
    field
      unbox : proj₁ (Membership x y)

open Dummy public using (_∈_) hiding (module _∈_)

-- The negation of membership.

infix 4 _∉_

_∉_ : {A : Type a} → A → Finite-subset-of A → Type a
x ∉ y = ¬ x ∈ y

private

  -- An unfolding lemma.

  ∈≃ : (x ∈ y) ≃ proj₁ (Membership x y)
  ∈≃ = Eq.↔⇒≃ (record
    { surjection = record
      { logical-equivalence = record
        { to   = Dummy._∈_.unbox
        ; from = Dummy.box
        }
      ; right-inverse-of = refl
      }
    ; left-inverse-of = refl
    })

-- Membership is propositional.

∈-propositional : Is-proposition (x ∈ y)
∈-propositional {x = x} {y = y} =          $⟨ proj₂ (Membership x y) ⟩
  Is-proposition (proj₁ (Membership x y))  ↝⟨ H-level-cong _ 1 (inverse ∈≃) ⦂ (_ → _) ⟩□
  Is-proposition (x ∈ y)                   □

-- A lemma characterising [].

∈[]≃ : (x ∈ []) ≃ ⊥₀
∈[]≃ {x = x} =
  x ∈ []  ↝⟨ ∈≃ ⟩
  ⊥       ↔⟨ ⊥↔⊥ ⟩□
  ⊥₀      □

-- A lemma characterising _∷_.

∈∷≃ : (x ∈ y ∷ z) ≃ (x ≡ y ∥⊎∥ x ∈ z)
∈∷≃ {x = x} {y = y} {z = z} =
  x ∈ y ∷ z                         ↝⟨ ∈≃ ⟩
  x ≡ y ∥⊎∥ proj₁ (Membership x z)  ↝⟨ F.id Trunc.∥⊎∥-cong inverse ∈≃ ⟩□
  x ≡ y ∥⊎∥ x ∈ z                   □

-- A variant.

∈≢∷≃ : x ≢ y → (x ∈ y ∷ z) ≃ (x ∈ z)
∈≢∷≃ {x = x} {y = y} {z = z} x≢y =
  x ∈ y ∷ z        ↝⟨ ∈∷≃ ⟩
  x ≡ y ∥⊎∥ x ∈ z  ↔⟨ Trunc.drop-⊥-left-∥⊎∥ ∈-propositional x≢y ⟩□
  x ∈ z            □

-- A lemma characterising singleton.

∈singleton≃ :
  (x ∈ singleton y) ≃ ∥ x ≡ y ∥
∈singleton≃ {x = x} {y = y} =
  x ∈ singleton y   ↝⟨ ∈∷≃ ⟩
  x ≡ y ∥⊎∥ x ∈ []  ↔⟨ Trunc.∥∥-cong $ drop-⊥-right ∈[]≃ ⟩□
  ∥ x ≡ y ∥         □

-- Some "introduction rules" for _∈_.

∈→∈∷ : x ∈ z → x ∈ y ∷ z
∈→∈∷ {x = x} {z = z} {y = y} =
  x ∈ z            ↝⟨ ∣_∣ ∘ inj₂ ⟩
  x ≡ y ∥⊎∥ x ∈ z  ↔⟨ inverse ∈∷≃ ⟩□
  x ∈ y ∷ z        □

∥≡∥→∈∷ : ∥ x ≡ y ∥ → x ∈ y ∷ z
∥≡∥→∈∷ {x = x} {y = y} {z = z} =
  ∥ x ≡ y ∥        ↝⟨ Trunc.∥∥-map inj₁ ⟩
  x ≡ y ∥⊎∥ x ∈ z  ↔⟨ inverse ∈∷≃ ⟩□
  x ∈ y ∷ z        □

≡→∈∷ : x ≡ y → x ∈ y ∷ z
≡→∈∷ = ∥≡∥→∈∷ ∘ ∣_∣

∥≡∥→∈singleton : ∥ x ≡ y ∥ → x ∈ singleton y
∥≡∥→∈singleton = ∥≡∥→∈∷

≡→∈singleton : x ≡ y → x ∈ singleton y
≡→∈singleton = ≡→∈∷

-- Membership of a union of two subsets can be expressed in terms of
-- membership of the subsets.

∈∪≃ : (x ∈ y ∪ z) ≃ (x ∈ y ∥⊎∥ x ∈ z)
∈∪≃ {x = x} {y = y} {z = z} = elim-prop e y
  where
  e : Elim-prop (λ y → (x ∈ y ∪ z) ≃ (x ∈ y ∥⊎∥ x ∈ z))
  e .[]ʳ =
    x ∈ z             ↔⟨ inverse $ Trunc.∥∥↔ ∈-propositional ⟩
    ∥ x ∈ z ∥         ↔⟨ Trunc.∥∥-cong (inverse $ drop-⊥-left ∈[]≃) ⟩□
    x ∈ [] ∥⊎∥ x ∈ z  □

  e .∷ʳ {y = u} y hyp =
    x ∈ y ∷ u ∪ z                ↝⟨ ∈∷≃ ⟩
    x ≡ y ∥⊎∥ x ∈ u ∪ z          ↝⟨ F.id Trunc.∥⊎∥-cong hyp ⟩
    x ≡ y ∥⊎∥ x ∈ u ∥⊎∥ x ∈ z    ↔⟨ Trunc.∥⊎∥-assoc ⟩
    (x ≡ y ∥⊎∥ x ∈ u) ∥⊎∥ x ∈ z  ↝⟨ Trunc.∥∥-cong (inverse ∈∷≃ ⊎-cong F.id) ⟩□
    x ∈ y ∷ u ∥⊎∥ x ∈ z          □

  e .is-propositionʳ _ =
    Eq.left-closure ext 0 ∈-propositional

-- More "introduction rules".

∈→∈∪ˡ : x ∈ y → x ∈ y ∪ z
∈→∈∪ˡ {x = x} {y = y} {z = z} =
  x ∈ y            ↝⟨ ∣_∣ ∘ inj₁ ⟩
  x ∈ y ∥⊎∥ x ∈ z  ↔⟨ inverse ∈∪≃ ⟩□
  x ∈ y ∪ z        □

∈→∈∪ʳ : ∀ y → x ∈ z → x ∈ y ∪ z
∈→∈∪ʳ {x = x} {z = z} y =
  x ∈ z      ↝⟨ ∈→∈∪ˡ ⟩
  x ∈ z ∪ y  ↝⟨ ≡⇒↝ _ (cong (_ ∈_) (comm z)) ⟩□
  x ∈ y ∪ z  □

-- A lemma characterising join.

∈join≃ : (x ∈ join z) ≃ ∥ (∃ λ y → x ∈ y × y ∈ z) ∥
∈join≃ {x = x} = elim-prop e _
  where
  e : Elim-prop (λ z → (x ∈ join z) ≃ ∥ (∃ λ y → x ∈ y × y ∈ z) ∥)
  e .[]ʳ =
    x ∈ join []                   ↔⟨⟩
    x ∈ []                        ↝⟨ ∈[]≃ ⟩
    ⊥                             ↔⟨ inverse $ Trunc.∥∥↔ ⊥-propositional ⟩
    ∥ ⊥ ∥                         ↔⟨ Trunc.∥∥-cong (inverse (×-right-zero {ℓ₁ = lzero} F.∘
                                                             ∃-cong (λ _ → ×-right-zero))) ⟩
    ∥ (∃ λ y → x ∈ y × ⊥) ∥       ↝⟨ Trunc.∥∥-cong (∃-cong λ _ → ∃-cong λ _ → inverse ∈[]≃) ⟩□
    ∥ (∃ λ y → x ∈ y × y ∈ []) ∥  □
  e .∷ʳ {y = z} u hyp =
    x ∈ join (u ∷ z)                                     ↔⟨⟩
    x ∈ u ∪ join z                                       ↝⟨ ∈∪≃ ⟩
    x ∈ u ∥⊎∥ x ∈ join z                                 ↝⟨ F.id Trunc.∥⊎∥-cong hyp ⟩
    x ∈ u ∥⊎∥ ∥ (∃ λ y → x ∈ y × y ∈ z) ∥                ↔⟨ inverse Trunc.truncate-right-∥⊎∥ ⟩
    x ∈ u ∥⊎∥ (∃ λ y → x ∈ y × y ∈ z)                    ↔⟨ ∃-intro _ _ Trunc.∥⊎∥-cong F.id ⟩
    (∃ λ y → x ∈ y × y ≡ u) ∥⊎∥ (∃ λ y → x ∈ y × y ∈ z)  ↔⟨ Trunc.∥∥-cong $ inverse $
                                                            ∃-⊎-distrib-left F.∘
                                                            (∃-cong λ _ → ∃-⊎-distrib-left) ⟩
    ∥ (∃ λ y → x ∈ y × (y ≡ u ⊎ y ∈ z)) ∥                ↔⟨ inverse $
                                                            Trunc.flatten′
                                                              (λ F → ∃ λ y → x ∈ y × F (y ≡ u ⊎ y ∈ z))
                                                              (λ f → Σ-map id (Σ-map id f))
                                                              (λ (y , p , q) → Trunc.∥∥-map (λ q → y , p , q) q) ⟩
    ∥ (∃ λ y → x ∈ y × (y ≡ u ∥⊎∥ y ∈ z)) ∥              ↝⟨ (Trunc.∥∥-cong $ ∃-cong λ _ → ∃-cong λ _ → inverse ∈∷≃) ⟩□
    ∥ (∃ λ y → x ∈ y × y ∈ u ∷ z) ∥                      □
  e .is-propositionʳ _ =
    Eq.left-closure ext 0 ∈-propositional

-- If truncated equality is decidable, then membership is also
-- decidable.

member? :
  ((x y : A) → Dec ∥ x ≡ y ∥) →
  (x : A) (y : Finite-subset-of A) → Dec (x ∈ y)
member? equal? x = elim-prop e
  where
  e : Elim-prop _
  e .[]ʳ          = no λ ()
  e .∷ʳ {y = z} y = case equal? x y of λ where
    (yes ∥x≡y∥) _ → yes (∥≡∥→∈∷ ∥x≡y∥)
    (no ¬∥x≡y∥)   →
      P.[ (λ x∈z → yes (∈→∈∷ x∈z))
        , (λ x∉z → no (
             x ∈ y ∷ z        ↔⟨ ∈∷≃ ⟩
             x ≡ y ∥⊎∥ x ∈ z  ↝⟨ Trunc.∥∥-map P.[ ¬∥x≡y∥ ∘ ∣_∣ , x∉z ] ⟩
             ∥ ⊥ ∥            ↔⟨ Trunc.not-inhabited⇒∥∥↔⊥ id ⟩□
             ⊥                □))
        ]
  e .is-propositionʳ y =
    Dec-closure-propositional ext ∈-propositional

-- A variant that uses Dec-Erased instead of Dec.

member?ᴱ :
  ((x y : A) → Dec-Erased ∥ x ≡ y ∥) →
  (x : A) (y : Finite-subset-of A) → Dec-Erased (x ∈ y)
member?ᴱ equal? x = elim-prop e
  where
  e : Elim-prop _
  e .[]ʳ          = no [ (λ ()) ]
  e .∷ʳ {y = z} y = case equal? x y of λ where
    (yes [ ∥x≡y∥ ]) _ → yes [ ∥≡∥→∈∷ ∥x≡y∥ ]
    (no [ ¬∥x≡y∥ ])   →
      P.[ (λ ([ x∈z ]) → yes [ ∈→∈∷ x∈z ])
        , (λ ([ x∉z ]) → no [
             x ∈ y ∷ z        ↔⟨ ∈∷≃ ⟩
             x ≡ y ∥⊎∥ x ∈ z  ↝⟨ Trunc.∥∥-map P.[ ¬∥x≡y∥ ∘ ∣_∣ , x∉z ] ⟩
             ∥ ⊥ ∥            ↔⟨ Trunc.not-inhabited⇒∥∥↔⊥ id ⟩□
             ⊥                □ ])
        ]
  e .is-propositionʳ y =
    EC.Is-proposition-Dec-Erased ext ∈-propositional

-- If x is a member of y, then x ∷ y is equal to y.

∈→∷≡ : x ∈ y → x ∷ y ≡ y
∈→∷≡ {x = x} = elim-prop e _
  where
  e : Elim-prop (λ y → x ∈ y → x ∷ y ≡ y)
  e .∷ʳ {y = y} z hyp =
    x ∈ z ∷ y            ↔⟨ ∈∷≃ ⟩
    x ≡ z ∥⊎∥ x ∈ y      ↝⟨ id Trunc.∥⊎∥-cong hyp ⟩
    x ≡ z ∥⊎∥ x ∷ y ≡ y  ↝⟨ Trunc.rec is-set
                              P.[ (λ x≡z →
      x ∷ z ∷ y                    ≡⟨ cong (λ x → x ∷ _) x≡z ⟩
      z ∷ z ∷ y                    ≡⟨ drop ⟩∎
      z ∷ y                        ∎)
                                , (λ x∷y≡y →
      x ∷ z ∷ y                    ≡⟨ swap ⟩
      z ∷ x ∷ y                    ≡⟨ cong (_ ∷_) x∷y≡y ⟩∎
      z ∷ y                        ∎)
                                ] ⟩□
    x ∷ z ∷ y ≡ z ∷ y    □

  e .is-propositionʳ _ =
    Π-closure ext 1 λ _ →
    is-set

------------------------------------------------------------------------
-- Subsets of subsets

-- Subsets.

infix 4 _⊆_

_⊆_ : {A : Type a} → Finite-subset-of A → Finite-subset-of A → Type a
x ⊆ y = ∀ z → z ∈ x → z ∈ y

-- _⊆_ is pointwise propositional.

⊆-propositional : Is-proposition (x ⊆ y)
⊆-propositional =
  Π-closure ext 1 λ _ →
  Π-closure ext 1 λ _ →
  ∈-propositional

-- The subset property can be expressed using _∪_ and _≡_.

⊆≃∪≡ : ∀ x → (x ⊆ y) ≃ (x ∪ y ≡ y)
⊆≃∪≡ {y = y} x =
  _↠_.from
    (Eq.≃↠⇔
       (Π-closure ext 1 λ _ →
        Π-closure ext 1 λ _ →
        ∈-propositional)
       is-set)
    (record
       { to   = elim-prop e x
       ; from = λ p z →
           z ∈ x      ↝⟨ ∈→∈∪ˡ ⟩
           z ∈ x ∪ y  ↝⟨ ≡⇒↝ _ (cong (z ∈_) p) ⟩□
           z ∈ y      □
       })
  where
  e : Elim-prop (λ x → x ⊆ y → x ∪ y ≡ y)
  e .[]ʳ _ =
    [] ∪ y  ≡⟨⟩
    y       ∎

  e .∷ʳ {y = z} x hyp x∷z⊆y =
    x ∷ z ∪ y  ≡⟨ cong (x ∷_) (hyp (λ _ → x∷z⊆y _ ∘ ∈→∈∷)) ⟩
    x ∷ y      ≡⟨ ∈→∷≡ (x∷z⊆y x (≡→∈∷ (refl _))) ⟩∎
    y          ∎

  e .is-propositionʳ _ =
    Π-closure ext 1 λ _ →
    is-set

-- Extensionality.

extensionality :
  (x ≡ y) ≃ (∀ z → z ∈ x ⇔ z ∈ y)
extensionality {x = x} {y = y} =
  _↠_.from
    (Eq.≃↠⇔
       is-set
       (Π-closure ext 1 λ _ →
        ⇔-closure ext 1
          ∈-propositional
          ∈-propositional))
    (record
       { to   = λ x≡y z → ≡⇒↝ _ (cong (z ∈_) x≡y)
       ; from =
           (∀ z → z ∈ x ⇔ z ∈ y)  ↝⟨ (λ p → _⇔_.to ∘ p , _⇔_.from ∘ p) ⟩
           x ⊆ y × y ⊆ x          ↔⟨ ⊆≃∪≡ x ×-cong ⊆≃∪≡ y ⟩
           x ∪ y ≡ y × y ∪ x ≡ x  ↝⟨ (λ (p , q) → trans (sym q) (trans (comm y) p)) ⟩□
           x ≡ y                  □
       })

-- Another way to characterise equality.

≡≃⊆×⊇ : (x ≡ y) ≃ (x ⊆ y × y ⊆ x)
≡≃⊆×⊇ {x = x} {y = y} =
  x ≡ y                  ↝⟨ extensionality ⟩
  (∀ z → z ∈ x ⇔ z ∈ y)  ↝⟨ Eq.⇔→≃
                              (Π-closure ext 1 λ _ →
                               ⇔-closure ext 1
                                 ∈-propositional
                                 ∈-propositional)
                              (×-closure 1 ⊆-propositional ⊆-propositional)
                              (λ hyp → _⇔_.to ∘ hyp , _⇔_.from ∘ hyp)
                              (λ (x⊆y , y⊆x) z → record { to = x⊆y z ; from = y⊆x z }) ⟩□
  x ⊆ y × y ⊆ x          □

-- _⊆_ is a partial order.

⊆-refl : x ⊆ x
⊆-refl _ = id

⊆-trans : x ⊆ y → y ⊆ z → x ⊆ z
⊆-trans x⊆y y⊆z _ = y⊆z _ ∘ x⊆y _

⊆-antisymmetric : x ⊆ y → y ⊆ x → x ≡ y
⊆-antisymmetric = curry (_≃_.from ≡≃⊆×⊇)

-- If truncated equality is decidable, then _⊆_ is also decidable.

subset? :
  ((x y : A) → Dec ∥ x ≡ y ∥) →
  (x y : Finite-subset-of A) → Dec (x ⊆ y)
subset? equal? x y = elim-prop r x
  where
  r : Elim-prop (λ x → Dec (x ⊆ y))
  r .[]ʳ = yes λ z →
    z ∈ []  ↔⟨ ∈[]≃ ⟩
    ⊥       ↝⟨ ⊥-elim ⟩□
    z ∈ y   □

  r .∷ʳ {y = x} z =
    Dec (x ⊆ y)                          ↝⟨ member? equal? z y ,_ ⟩
    Dec (z ∈ y) × Dec (x ⊆ y)            ↝⟨ uncurry
                                              P.[ (λ u∈y → Dec-map (
        x ⊆ y                                        ↝⟨ record
                                                          { to = λ x⊆y u →
                                                                   P.[ (λ z≡u → subst (_∈ y) (sym z≡u) u∈y)
                                                                     , x⊆y u
                                                                     ]
                                                          ; from = λ hyp u → hyp u ∘ inj₂
                                                          } ⟩
        (∀ u → u ≡ z ⊎ u ∈ x → u ∈ y)                ↔⟨ (∀-cong ext λ _ → inverse $
                                                         Trunc.universal-property ∈-propositional) ⟩
        (∀ u → u ≡ z ∥⊎∥ u ∈ x → u ∈ y)              ↝⟨ (∀-cong _ λ _ → →-cong₁ _ (inverse ∈∷≃)) ⟩
        (∀ u → u ∈ z ∷ x → u ∈ y)                    ↔⟨⟩
        z ∷ x ⊆ y                                    □))
                                                , (λ u∉y _ → no (
        z ∷ x ⊆ y                                    ↝⟨ (λ u∷x⊆y → u∷x⊆y z (≡→∈∷ (refl _))) ⟩
        z ∈ y                                        ↝⟨ u∉y ⟩□
        ⊥                                            □))
                                                ] ⟩□
    Dec (z ∷ x ⊆ y)                      □

  r .is-propositionʳ _ =
    Dec-closure-propositional ext ⊆-propositional

-- A variant of subset? that uses Dec-Erased.

subset?ᴱ :
  ((x y : A) → Dec-Erased ∥ x ≡ y ∥) →
  (x y : Finite-subset-of A) → Dec-Erased (x ⊆ y)
subset?ᴱ equal? x y = elim-prop r x
  where
  r : Elim-prop (λ x → Dec-Erased (x ⊆ y))
  r .[]ʳ = yes [ (λ z →
    z ∈ []  ↔⟨ ∈[]≃ ⟩
    ⊥       ↝⟨ ⊥-elim ⟩□
    z ∈ y   □ )]

  r .∷ʳ {y = x} z =
    Dec-Erased (x ⊆ y)                       ↝⟨ member?ᴱ equal? z y ,_ ⟩
    Dec-Erased (z ∈ y) × Dec-Erased (x ⊆ y)  ↝⟨ uncurry
                                                P.[ (λ ([ u∈y ]) → EC.Dec-Erased-map (
        x ⊆ y                                          ↝⟨ record
                                                            { to = λ x⊆y u →
                                                                     P.[ (λ z≡u → subst (_∈ y) (sym z≡u) u∈y)
                                                                       , x⊆y u
                                                                       ]
                                                            ; from = λ hyp u → hyp u ∘ inj₂
                                                            } ⟩
        (∀ u → u ≡ z ⊎ u ∈ x → u ∈ y)                  ↔⟨ (∀-cong ext λ _ → inverse $
                                                           Trunc.universal-property ∈-propositional) ⟩
        (∀ u → u ≡ z ∥⊎∥ u ∈ x → u ∈ y)                ↝⟨ (∀-cong _ λ _ → →-cong₁ _ (inverse ∈∷≃)) ⟩
        (∀ u → u ∈ z ∷ x → u ∈ y)                      ↔⟨⟩
        z ∷ x ⊆ y                                      □))
                                                  , (λ ([ u∉y ]) _ → no [
        z ∷ x ⊆ y                                      ↝⟨ (λ u∷x⊆y → u∷x⊆y z (≡→∈∷ (refl _))) ⟩
        z ∈ y                                          ↝⟨ u∉y ⟩□
        ⊥                                              □ ])
                                                  ] ⟩□
    Dec-Erased (z ∷ x ⊆ y)                   □

  r .is-propositionʳ _ =
    EC.Is-proposition-Dec-Erased ext ⊆-propositional

-- If truncated equality is decidable, then _≡_ is also decidable.

equal? :
  ((x y : A) → Dec ∥ x ≡ y ∥) →
  (x y : Finite-subset-of A) → Dec (x ≡ y)
equal? eq? x y =             $⟨ subset? eq? x y , subset? eq? y x ⟩
  Dec (x ⊆ y) × Dec (y ⊆ x)  ↝⟨ uncurry Dec-× ⟩
  Dec (x ⊆ y × y ⊆ x)        ↝⟨ Dec-map (from-equivalence $ inverse ≡≃⊆×⊇) ⟩□
  Dec (x ≡ y)                □

-- A variant of equal? that uses Dec-Erased.

equal?ᴱ :
  ((x y : A) → Dec-Erased ∥ x ≡ y ∥) →
  (x y : Finite-subset-of A) → Dec-Erased (x ≡ y)
equal?ᴱ eq? x y =                              $⟨ subset?ᴱ eq? x y , subset?ᴱ eq? y x ⟩
  Dec-Erased (x ⊆ y) × Dec-Erased (y ⊆ x)      ↝⟨ EC.Dec-Erased↔Dec-Erased _ ×-cong EC.Dec-Erased↔Dec-Erased _ ⟩
  Dec (Erased (x ⊆ y)) × Dec (Erased (y ⊆ x))  ↝⟨ uncurry Dec-× ⟩
  Dec (Erased (x ⊆ y) × Erased (y ⊆ x))        ↝⟨ Dec-map (from-isomorphism $ inverse EC.Erased-Σ↔Σ) ⟩
  Dec (Erased (x ⊆ y × y ⊆ x))                 ↝⟨ _⇔_.from $ EC.Dec-Erased↔Dec-Erased _ ⟩
  Dec-Erased (x ⊆ y × y ⊆ x)                   ↝⟨ EC.Dec-Erased-map (from-equivalence $ inverse ≡≃⊆×⊇) ⟩□
  Dec-Erased (x ≡ y)                           □

------------------------------------------------------------------------
-- The functions map-Maybe, filter, minus and delete

private

  -- A function used to define map-Maybe.

  map-Maybe-cons : Maybe B → Finite-subset-of B → Finite-subset-of B
  map-Maybe-cons nothing  y = y
  map-Maybe-cons (just x) y = x ∷ y

-- A combination of map and filter.

map-Maybe : (A → Maybe B) → Finite-subset-of A → Finite-subset-of B
map-Maybe f = rec r
  where
  r : Rec _ _
  r .[]ʳ         = []
  r .∷ʳ x _ y    = map-Maybe-cons (f x) y
  r .is-setʳ     = is-set
  r .dropʳ x _ y = lemma (f x)
    where
    lemma :
      ∀ m → map-Maybe-cons m (map-Maybe-cons m y) ≡ map-Maybe-cons m y
    lemma nothing  = refl _
    lemma (just _) = drop

  r .swapʳ x y _ z = lemma (f x) (f y)
    where
    lemma :
      ∀ m₁ m₂ →
      map-Maybe-cons m₁ (map-Maybe-cons m₂ z) ≡
      map-Maybe-cons m₂ (map-Maybe-cons m₁ z)
    lemma (just _) (just _) = swap
    lemma _        nothing  = refl _
    lemma nothing  _        = refl _

-- A lemma characterising map-Maybe.

∈map-Maybe≃ :
  (x ∈ map-Maybe f y) ≃ ∥ (∃ λ z → z ∈ y × f z ≡ just x) ∥
∈map-Maybe≃ {x = x} {f = f} = elim-prop e _
  where
  e : Elim-prop (λ y → (x ∈ map-Maybe f y) ≃
                       ∥ (∃ λ z → z ∈ y × f z ≡ just x) ∥)
  e .[]ʳ =
    x ∈ map-Maybe f []                   ↝⟨ ∈[]≃ ⟩
    ⊥                                    ↔⟨ inverse $ Trunc.∥∥↔ ⊥-propositional ⟩
    ∥ ⊥ ∥                                ↔⟨ Trunc.∥∥-cong (inverse (×-right-zero {ℓ₁ = lzero} F.∘
                                                                    ∃-cong (λ _ → ×-left-zero))) ⟩
    ∥ (∃ λ z → ⊥ × f z ≡ just x) ∥       ↝⟨ Trunc.∥∥-cong (∃-cong λ _ → inverse ∈[]≃ ×-cong F.id) ⟩□
    ∥ (∃ λ z → z ∈ [] × f z ≡ just x) ∥  □

  e .∷ʳ {y = y} z hyp =
    (x ∈ map-Maybe f (z ∷ y))                                          ↝⟨ lemma _ _ ⟩
    f z ≡ just x ∥⊎∥ (x ∈ map-Maybe f y)                               ↝⟨ from-isomorphism (inverse Trunc.truncate-right-∥⊎∥) F.∘
                                                                          (F.id Trunc.∥⊎∥-cong hyp) ⟩
    f z ≡ just x ∥⊎∥ (∃ λ u → u ∈ y × f u ≡ just x)                    ↔⟨ inverse $
                                                                          drop-⊤-left-Σ (_⇔_.to contractible⇔↔⊤ $ singleton-contractible _) F.∘
                                                                          Σ-assoc
                                                                            Trunc.∥⊎∥-cong
                                                                          F.id ⟩
    (∃ λ u → u ≡ z × f u ≡ just x) ∥⊎∥ (∃ λ u → u ∈ y × f u ≡ just x)  ↔⟨ Trunc.∥∥-cong $ inverse ∃-⊎-distrib-left ⟩
    ∥ (∃ λ u → u ≡ z × f u ≡ just x ⊎ u ∈ y × f u ≡ just x) ∥          ↔⟨ Trunc.∥∥-cong (∃-cong λ _ → inverse ∃-⊎-distrib-right) ⟩
    ∥ (∃ λ u → (u ≡ z ⊎ u ∈ y) × f u ≡ just x) ∥                       ↔⟨ inverse $
                                                                          Trunc.flatten′
                                                                            (λ F → (∃ λ u → F (u ≡ z ⊎ u ∈ y) × f u ≡ just x))
                                                                            (λ f → Σ-map id (Σ-map f id))
                                                                            (λ (u , p , q) → Trunc.∥∥-map (λ p → u , p , q) p) ⟩
    ∥ (∃ λ u → (u ≡ z ∥⊎∥ u ∈ y) × f u ≡ just x) ∥                     ↝⟨ Trunc.∥∥-cong (∃-cong λ _ → ×-cong₁ λ _ → inverse ∈∷≃) ⟩□
    ∥ (∃ λ u → u ∈ z ∷ y × f u ≡ just x) ∥                             □
    where
    lemma : ∀ m y → (x ∈ map-Maybe-cons m y) ≃ (m ≡ just x ∥⊎∥ x ∈ y)
    lemma nothing y =
      x ∈ map-Maybe-cons nothing y  ↔⟨⟩
      x ∈ y                         ↔⟨ inverse $ Trunc.drop-⊥-left-∥⊎∥ ∈-propositional ⊎.inj₁≢inj₂ ⟩□
      (nothing ≡ just x ∥⊎∥ x ∈ y)  □
    lemma (just z) y =
      x ∈ map-Maybe-cons (just z) y  ↔⟨⟩
      x ∈ z ∷ y                      ↝⟨ ∈∷≃ ⟩
      x ≡ z ∥⊎∥ x ∈ y                ↔⟨ (Bijection.≡↔inj₂≡inj₂ F.∘ ≡-comm) Trunc.∥⊎∥-cong F.id ⟩□
      just z ≡ just x ∥⊎∥ x ∈ y      □

  e .is-propositionʳ y =
    Eq.left-closure ext 0 ∈-propositional

-- The function map-Maybe f commutes with map-Maybe g if f commutes
-- with g in a certain way.

map-Maybe-comm :
  {A : Type a} {f g : A → Maybe A} →
  (∀ x → f =<< g x ≡ g =<< f x) →
  ∀ x → map-Maybe f (map-Maybe g x) ≡ map-Maybe g (map-Maybe f x)
map-Maybe-comm {A = A} {f = f} {g = g}
               hyp x = _≃_.from extensionality λ y →
  y ∈ map-Maybe f (map-Maybe g x)           ↝⟨ lemma₂ ⟩
  ∥ (∃ λ u → u ∈ x × f =<< g u ≡ just y) ∥  ↝⟨ Trunc.∥∥-cong (∃-cong λ _ → ∃-cong λ _ → ≡⇒↝ _ $ cong (_≡ _) $ hyp _) ⟩
  ∥ (∃ λ u → u ∈ x × g =<< f u ≡ just y) ∥  ↝⟨ inverse lemma₂ ⟩
  y ∈ map-Maybe g (map-Maybe f x)           □
  where
  lemma₁ :
    ∀ (f {g} : A → Maybe A) {x z} →
    (∃ λ y → f x ≡ just y × g y ≡ just z) ⇔ (g =<< f x ≡ just z)
  lemma₁ f {g = g} {x = x} {z = z} = record
    { to = λ (y , f≡ , g≡) →
        g =<< f x                    ≡⟨⟩
        Maybe.maybe g nothing (f x)  ≡⟨ cong (Maybe.maybe g nothing) f≡ ⟩
        g y                          ≡⟨ g≡ ⟩∎
        just z                       ∎
    ; from = from (f x)
    }
    where
    from :
      (fx : Maybe A) →
      g =<< fx ≡ just z →
      ∃ λ y → fx ≡ just y × g y ≡ just z
    from nothing  = ⊥-elim ∘ ⊎.inj₁≢inj₂
    from (just y) = (y ,_) ∘ (refl _ ,_)

  lemma₂ :
    {f g : A → Maybe A} →
    y ∈ map-Maybe f (map-Maybe g x) ⇔
    ∥ (∃ λ u → u ∈ x × f =<< g u ≡ just y) ∥
  lemma₂ {y = y} {f = f} {g = g} =
    y ∈ map-Maybe f (map-Maybe g x)                                  ↔⟨ Trunc.∥∥-cong (∃-cong λ _ → ∈map-Maybe≃ ×-cong F.id) F.∘ ∈map-Maybe≃ ⟩
    ∥ (∃ λ z → ∥ (∃ λ u → u ∈ x × g u ≡ just z) ∥ × f z ≡ just y) ∥  ↔⟨ Trunc.flatten′
                                                                          (λ F → ∃ λ z → F (∃ λ u → u ∈ x × _) × _)
                                                                          (λ f → Σ-map id (Σ-map f id))
                                                                          (λ (z , p , q) → Trunc.∥∥-map (λ p → z , p , q) p) ⟩
    ∥ (∃ λ z → (∃ λ u → u ∈ x × g u ≡ just z) × f z ≡ just y) ∥      ↔⟨ Trunc.∥∥-cong (∃-cong λ _ → inverse $ Σ-assoc F.∘ ∃-cong λ _ → Σ-assoc) ⟩
    ∥ (∃ λ z → ∃ λ u → u ∈ x × g u ≡ just z × f z ≡ just y) ∥        ↔⟨ Trunc.∥∥-cong ((∃-cong λ _ → ∃-comm) F.∘ ∃-comm) ⟩
    ∥ (∃ λ u → u ∈ x × ∃ λ z → g u ≡ just z × f z ≡ just y) ∥        ↝⟨ Trunc.∥∥-cong (∃-cong λ _ → ∃-cong λ _ → lemma₁ g) ⟩□
    ∥ (∃ λ u → u ∈ x × f =<< g u ≡ just y) ∥                         □

-- The function map-Maybe commutes with union.

map-Maybe-∪ :
  ∀ x → map-Maybe f (x ∪ y) ≡ map-Maybe f x ∪ map-Maybe f y
map-Maybe-∪ {f = f} {y = y} x = _≃_.from extensionality λ z →
  z ∈ map-Maybe f (x ∪ y)                                    ↔⟨ (Trunc.∥∥-cong (∃-cong λ _ → ∈∪≃ ×-cong F.id)) F.∘ ∈map-Maybe≃ ⟩

  ∥ (∃ λ u → (u ∈ x ∥⊎∥ u ∈ y) × f u ≡ just z) ∥             ↔⟨ Trunc.flatten′
                                                                  (λ F → ∃ λ u → F (u ∈ x ⊎ u ∈ y) × _)
                                                                  (λ f → Σ-map id (Σ-map f id))
                                                                  (λ (u , p , q) → Trunc.∥∥-map (λ p → u , p , q) p) ⟩

  ∥ (∃ λ u → (u ∈ x ⊎ u ∈ y) × f u ≡ just z) ∥               ↔⟨ Trunc.∥∥-cong (∃-cong λ _ → ∃-⊎-distrib-right) ⟩

  ∥ (∃ λ u → u ∈ x × f u ≡ just z ⊎ u ∈ y × f u ≡ just z) ∥  ↔⟨ Trunc.∥∥-cong ∃-⊎-distrib-left ⟩

  (∃ λ u → u ∈ x × f u ≡ just z) ∥⊎∥
  (∃ λ u → u ∈ y × f u ≡ just z)                             ↔⟨ inverse $
                                                                Trunc.flatten′ (λ F → F _ ⊎ F _) (λ f → ⊎-map f f)
                                                                  P.[ Trunc.∥∥-map inj₁ , Trunc.∥∥-map inj₂ ] ⟩
  ∥ (∃ λ u → u ∈ x × f u ≡ just z) ∥ ∥⊎∥
  ∥ (∃ λ u → u ∈ y × f u ≡ just z) ∥                         ↔⟨ inverse $ (∈map-Maybe≃ Trunc.∥⊎∥-cong ∈map-Maybe≃) F.∘ ∈∪≃ ⟩□

  z ∈ map-Maybe f x ∪ map-Maybe f y                          □

-- One can express map using map-Maybe.

map≡map-Maybe-just :
  (x : Finite-subset-of A) →
  map f x ≡ map-Maybe (just ∘ f) x
map≡map-Maybe-just {f = f} = elim-prop e
  where
  e : Elim-prop _
  e .[]ʳ               = refl _
  e .∷ʳ x              = cong (f x ∷_)
  e .is-propositionʳ _ = is-set

-- A lemma characterising map.

∈map≃ : (x ∈ map f y) ≃ ∥ (∃ λ z → z ∈ y × f z ≡ x) ∥
∈map≃ {x = x} {f = f} {y = y} =
  x ∈ map f y                                ↝⟨ ≡⇒↝ _ $ cong (_ ∈_) $ map≡map-Maybe-just y ⟩
  x ∈ map-Maybe (just ∘ f) y                 ↝⟨ ∈map-Maybe≃ ⟩
  ∥ (∃ λ z → z ∈ y × just (f z) ≡ just x) ∥  ↔⟨ Trunc.∥∥-cong (∃-cong λ _ → ∃-cong λ _ → inverse Bijection.≡↔inj₂≡inj₂) ⟩□
  ∥ (∃ λ z → z ∈ y × f z ≡ x) ∥              □

-- Some consequences of the characterisation of map.

∈→∈map :
  {f : A → B} →
  x ∈ y → f x ∈ map f y
∈→∈map {x = x} {y = y} {f = f} =
  x ∈ y                            ↝⟨ (λ x∈y → ∣ x , x∈y , refl _ ∣) ⟩
  ∥ (∃ λ z → z ∈ y × f z ≡ f x) ∥  ↔⟨ inverse ∈map≃ ⟩□
  f x ∈ map f y                    □

Injective→∈map≃ :
  {f : A → B} →
  Injective f →
  (f x ∈ map f y) ≃ (x ∈ y)
Injective→∈map≃ {x = x} {y = y} {f = f} inj =
  f x ∈ map f y                    ↝⟨ ∈map≃ ⟩
  ∥ (∃ λ z → z ∈ y × f z ≡ f x) ∥  ↝⟨ (Trunc.∥∥-cong-⇔ $ ∃-cong λ _ → ∃-cong λ _ →
                                       record { to = inj; from = cong f }) ⟩
  ∥ (∃ λ z → z ∈ y × z ≡ x) ∥      ↔⟨ Trunc.∥∥-cong $ inverse $ ∃-intro _ _ ⟩
  ∥ x ∈ y ∥                        ↔⟨ Trunc.∥∥↔ ∈-propositional ⟩□
  x ∈ y                            □

-- The function map commutes with union.

map-∪ : ∀ x → map f (x ∪ y) ≡ map f x ∪ map f y
map-∪ {f = f} {y = y} x =
  map f (x ∪ y)                                    ≡⟨ map≡map-Maybe-just (x ∪ y) ⟩
  map-Maybe (just ∘ f) (x ∪ y)                     ≡⟨ map-Maybe-∪ x ⟩
  map-Maybe (just ∘ f) x ∪ map-Maybe (just ∘ f) y  ≡⟨ sym $ cong₂ _∪_ (map≡map-Maybe-just x) (map≡map-Maybe-just y) ⟩∎
  map f x ∪ map f y                                ∎

-- A filter function.

filter : (A → Bool) → Finite-subset-of A → Finite-subset-of A
filter p = map-Maybe (λ x → if p x then just x else nothing)

-- A lemma characterising filter.

∈filter≃ :
  ∀ p → (x ∈ filter p y) ≃ (T (p x) × x ∈ y)
∈filter≃ {x = x} {y = y} p =
  x ∈ map-Maybe (λ x → if p x then just x else nothing) y         ↝⟨ ∈map-Maybe≃ ⟩
  ∥ (∃ λ z → z ∈ y × if p z then just z else nothing ≡ just x) ∥  ↝⟨ (Trunc.∥∥-cong $ ∃-cong λ _ → ∃-cong λ _ → lemma _ (refl _)) ⟩
  ∥ (∃ λ z → z ∈ y × T (p z) × z ≡ x) ∥                           ↔⟨ (Trunc.∥∥-cong $ ∃-cong λ _ →
                                                                      (×-cong₁ λ z≡x → ≡⇒↝ _ $ cong (λ z → z ∈ y × T (p z)) z≡x) F.∘
                                                                      Σ-assoc) ⟩
  ∥ (∃ λ z → (x ∈ y × T (p x)) × z ≡ x) ∥                         ↔⟨ inverse Σ-assoc F.∘
                                                                     (×-cong₁ λ _ →
                                                                        ×-comm F.∘
                                                                        Trunc.∥∥↔ (×-closure 1 ∈-propositional (T-propositional (p x)))) F.∘
                                                                     inverse Trunc.∥∥×∥∥↔∥×∥ F.∘
                                                                     Trunc.∥∥-cong ∃-comm ⟩
  T (p x) × x ∈ y × ∥ (∃ λ z → z ≡ x) ∥                           ↔⟨ (∃-cong λ _ → drop-⊤-right λ _ →
                                                                      _⇔_.to contractible⇔↔⊤ (singleton-contractible _) F.∘
                                                                      Trunc.∥∥↔ (mono₁ 0 $ singleton-contractible _)) ⟩□
  T (p x) × x ∈ y                                                 □
  where
  lemma :
    ∀ b → p z ≡ b →
    (if b then just z else nothing ≡ just x) ≃
    (T b × z ≡ x)
  lemma {z = z} true eq =
    just z ≡ just x  ↔⟨ inverse Bijection.≡↔inj₂≡inj₂ ⟩
    z ≡ x            ↔⟨ inverse ×-left-identity ⟩□
    ⊤ × z ≡ x        □
  lemma {z = z} false eq =
    nothing ≡ just x  ↔⟨ Bijection.≡↔⊎ ⟩
    ⊥                 ↔⟨ inverse ×-left-zero ⟩□
    ⊥ × z ≡ x         □

-- The result of filtering is a subset of the original subset.

filter⊆ : ∀ p → filter p x ⊆ x
filter⊆ {x = x} p z =
  z ∈ filter p x   ↔⟨ ∈filter≃ p ⟩
  T (p z) × z ∈ x  ↝⟨ proj₂ ⟩□
  z ∈ x            □

-- Filtering commutes with itself.

filter-comm :
  ∀ (p q : A → Bool) x →
  filter p (filter q x) ≡ filter q (filter p x)
filter-comm p q x = _≃_.from extensionality λ y →
  y ∈ filter p (filter q x)    ↔⟨ from-isomorphism Σ-assoc F.∘ (F.id ×-cong ∈filter≃ q) F.∘ ∈filter≃ p ⟩
  (T (p y) × T (q y)) × y ∈ x  ↔⟨ ×-comm ×-cong F.id ⟩
  (T (q y) × T (p y)) × y ∈ x  ↔⟨ inverse $ from-isomorphism Σ-assoc F.∘ (F.id ×-cong ∈filter≃ p) F.∘ ∈filter≃ q ⟩□
  y ∈ filter q (filter p x)    □

-- Filtering commutes with union.

filter-∪ :
  ∀ p x → filter p (x ∪ y) ≡ filter p x ∪ filter p y
filter-∪ _ = map-Maybe-∪

-- If erased truncated equality is decidable, then one subset can be
-- removed from another.

minus :
  ((x y : A) → Dec-Erased ∥ x ≡ y ∥) →
  Finite-subset-of A → Finite-subset-of A → Finite-subset-of A
minus _≟_ x y =
  filter (λ z → if member?ᴱ _≟_ z y then false else true) x

-- A lemma characterising minus.

∈minus≃ : (x ∈ minus _≟_ y z) ≃ (x ∈ y × x ∉ z)
∈minus≃ {x = x} {_≟_ = _≟_} {y = y} {z = z} =
  x ∈ minus _≟_ y z                                     ↝⟨ ∈filter≃ (λ _ → if member?ᴱ _ _ z then _ else _) ⟩
  T (if member?ᴱ _≟_ x z then false else true) × x ∈ y  ↔⟨ lemma (member?ᴱ _≟_ x z) ×-cong F.id ⟩
  x ∉ z × x ∈ y                                         ↔⟨ ×-comm ⟩□
  x ∈ y × x ∉ z                                         □
  where
  lemma :
    (d : Dec-Erased A) →
    T (if d then false else true) ↔ ¬ A
  lemma {A = A} d@(yes a) =
    T (if d then false else true)  ↔⟨⟩
    ⊥                              ↝⟨ Bijection.⊥↔uninhabited (_$ a) ⟩
    ¬ EC.Erased A                  ↝⟨ EC.¬-Erased↔¬ ext ⟩□
    ¬ A                            □
  lemma {A = A} d@(no ¬a) =
    T (if d then false else true) ↔⟨⟩
    ⊤                             ↝⟨ inverse $
                                     _⇔_.to contractible⇔↔⊤ $
                                     propositional⇒inhabited⇒contractible
                                       (¬-propositional ext)
                                       (EC.Stable-¬ ¬a) ⟩□
    ¬ A                           □

-- The result of minus is a subset of the original subset.

minus⊆ : ∀ y → minus _≟_ x y ⊆ x
minus⊆ y =
  filter⊆ (λ _ → if member?ᴱ _ _ y then _ else _)

-- Minus commutes with itself (in a certain sense).

minus-comm :
  ∀ x y z →
  minus _≟_ (minus _≟_ x y) z ≡ minus _≟_ (minus _≟_ x z) y
minus-comm x y z =
  filter-comm
    (λ _ → if member?ᴱ _ _ z then _ else _)
    (λ _ → if member?ᴱ _ _ y then _ else _)
    x

-- Minus commutes with union (in a certain sense).

minus-∪ :
  ∀ x z →
  minus _≟_ (x ∪ y) z ≡ minus _≟_ x z ∪ minus _≟_ y z
minus-∪ x z = filter-∪ (λ _ → if member?ᴱ _ _ z then _ else _) x

-- A lemma relating minus, _⊆_ and _∪_.

minus⊆≃ :
  {_≟_ : (x y : A) → Dec ∥ x ≡ y ∥} →
  ∀ y →
  (minus (λ x y → Dec→Dec-Erased (x ≟ y)) x y ⊆ z) ≃
  (x ⊆ y ∪ z)
minus⊆≃ {x = x} {z = z} {_≟_ = _≟_} y =
  _↠_.from (Eq.≃↠⇔ ⊆-propositional ⊆-propositional) $ record
    { to = λ x-y⊆z u →
        u ∈ x                         ↝⟨ (λ u∈x →
                                            case member? _≟_ u y of
                                              P.[ Trunc.∣inj₁∣ , Trunc.∣inj₂∣ ∘ (u∈x ,_) ]) ⟩
        u ∈ y ∥⊎∥ (u ∈ x × u ∉ y)     ↔⟨ F.id Trunc.∥⊎∥-cong inverse ∈minus≃ ⟩
        u ∈ y ∥⊎∥ u ∈ minus _≟′_ x y  ↝⟨ id Trunc.∥⊎∥-cong x-y⊆z u ⟩
        u ∈ y ∥⊎∥ u ∈ z               ↔⟨ inverse ∈∪≃ ⟩□
        u ∈ y ∪ z                     □
    ; from = λ x⊆y∪z u →
        u ∈ minus _≟′_ x y         ↔⟨ ∈minus≃ ⟩
        u ∈ x × u ∉ y              ↝⟨ Σ-map (x⊆y∪z _) id ⟩
        u ∈ y ∪ z × u ∉ y          ↔⟨ ∈∪≃ ×-cong F.id ⟩
        (u ∈ y ∥⊎∥ u ∈ z) × u ∉ y  ↔⟨ (×-cong₁ λ u∉y → Trunc.drop-⊥-left-∥⊎∥ ∈-propositional u∉y) ⟩
        u ∈ z × u ∉ y              ↝⟨ proj₁ ⟩□
        u ∈ z                      □
    }
  where
  _≟′_ = λ x y → Dec→Dec-Erased (x ≟ y)

-- If erased truncated equality is decidable, then elements can be
-- removed from a subset.

delete :
  ((x y : A) → Dec-Erased ∥ x ≡ y ∥) →
  A → Finite-subset-of A → Finite-subset-of A
delete _≟_ x y = minus _≟_ y (singleton x)

-- A lemma characterising delete.

∈delete≃ : ∀ _≟_ → (x ∈ delete _≟_ y z) ≃ (x ≢ y × x ∈ z)
∈delete≃ {x = x} {y = y} {z = z} _≟_ =
  x ∈ delete _≟_ y z       ↝⟨ ∈minus≃ {_≟_ = _≟_} ⟩
  x ∈ z × x ∉ singleton y  ↝⟨ F.id ×-cong →-cong₁ ext ∈singleton≃ ⟩
  x ∈ z × ¬ ∥ x ≡ y ∥      ↔⟨ F.id ×-cong Trunc.¬∥∥↔¬ ⟩
  x ∈ z × x ≢ y            ↔⟨ ×-comm ⟩□
  x ≢ y × x ∈ z            □

-- A deleted element is no longer a member of the set.

∉delete : ∀ _≟_ y → x ∉ delete _≟_ x y
∉delete {x = x} _≟_ y =
  x ∈ delete _≟_ x y  ↔⟨ ∈delete≃ _≟_ ⟩
  x ≢ x × x ∈ y       ↝⟨ (_$ refl _) ∘ proj₁ ⟩□
  ⊥                   □

-- Deletion commutes with itself (in a certain sense).

delete-comm :
  ∀ _≟_ z →
  delete _≟_ x (delete _≟_ y z) ≡ delete _≟_ y (delete _≟_ x z)
delete-comm _≟_ z =
  minus-comm {_≟_ = _≟_} z (singleton _) (singleton _)

-- Deletion commutes with union.

delete-∪ :
  ∀ _≟_ y →
  delete _≟_ x (y ∪ z) ≡ delete _≟_ x y ∪ delete _≟_ x z
delete-∪ _≟_ y = minus-∪ {_≟_ = _≟_} y (singleton _)

-- A lemma relating delete, _⊆_ and _∷_.

delete⊆≃ :
  (_≟_ : (x y : A) → Dec ∥ x ≡ y ∥) →
  (delete (λ x y → Dec→Dec-Erased (x ≟ y)) x y ⊆ z) ≃ (y ⊆ x ∷ z)
delete⊆≃ _≟_ = minus⊆≃ {_≟_ = _≟_} (singleton _)

------------------------------------------------------------------------
-- Some preservation lemmas for _⊆_

-- Various operations preserve _⊆_.

∷-cong-⊆ : y ⊆ z → x ∷ y ⊆ x ∷ z
∷-cong-⊆ {y = y} {z = z} {x = x} y⊆z u =
  u ∈ x ∷ y        ↔⟨ ∈∷≃ ⟩
  u ≡ x ∥⊎∥ u ∈ y  ↝⟨ id Trunc.∥⊎∥-cong y⊆z _ ⟩
  u ≡ x ∥⊎∥ u ∈ z  ↔⟨ inverse ∈∷≃ ⟩□
  u ∈ x ∷ z        □

∪-cong-⊆ : x₁ ⊆ x₂ → y₁ ⊆ y₂ → x₁ ∪ y₁ ⊆ x₂ ∪ y₂
∪-cong-⊆ {x₁ = x₁} {x₂ = x₂} {y₁ = y₁} {y₂ = y₂} x₁⊆x₂ y₁⊆y₂ z =
  z ∈ x₁ ∪ y₁        ↔⟨ ∈∪≃ ⟩
  z ∈ x₁ ∥⊎∥ z ∈ y₁  ↝⟨ x₁⊆x₂ _ Trunc.∥⊎∥-cong y₁⊆y₂ _ ⟩
  z ∈ x₂ ∥⊎∥ z ∈ y₂  ↔⟨ inverse ∈∪≃ ⟩□
  z ∈ x₂ ∪ y₂        □

filter-cong-⊆ :
  (∀ z → T (p z) → T (q z)) →
  x ⊆ y → filter p x ⊆ filter q y
filter-cong-⊆ {p = p} {q = q} {x = x} {y = y} p⇒q x⊆y z =
  z ∈ filter p x   ↔⟨ ∈filter≃ p ⟩
  T (p z) × z ∈ x  ↝⟨ Σ-map (p⇒q _) (x⊆y _) ⟩
  T (q z) × z ∈ y  ↔⟨ inverse $ ∈filter≃ q ⟩□
  z ∈ filter q y   □

minus-cong-⊆ : x₁ ⊆ x₂ → y₂ ⊆ y₁ → minus _≟_ x₁ y₁ ⊆ minus _≟_ x₂ y₂
minus-cong-⊆ {x₁ = x₁} {x₂ = x₂} {y₂ = y₂} {y₁ = y₁} {_≟_ = _≟_}
             x₁⊆x₂ y₂⊆y₁ z =
  z ∈ minus _≟_ x₁ y₁  ↔⟨ ∈minus≃ ⟩
  z ∈ x₁ × z ∉ y₁      ↝⟨ Σ-map (x₁⊆x₂ _) (_∘ y₂⊆y₁ _) ⟩
  z ∈ x₂ × z ∉ y₂      ↔⟨ inverse ∈minus≃ ⟩□
  z ∈ minus _≟_ x₂ y₂  □

delete-cong-⊆ : ∀ _≟_ → y ⊆ z → delete _≟_ x y ⊆ delete _≟_ x z
delete-cong-⊆ _≟_ y⊆z =
  minus-cong-⊆ {_≟_ = _≟_} y⊆z (⊆-refl {x = singleton _})

------------------------------------------------------------------------
-- Size

private

  -- This definition is used to define ∣_∣≡ and ∣∣≡-propositional
  -- below.
  --
  -- This definition is not taken from "Finite Sets in Homotopy Type
  -- Theory", but it is based on the size function in that paper.

  Size : {A : Type a} → Finite-subset-of A → ℕ → Proposition a
  Size {a = a} {A = A} = rec r
    where

    mutual

      -- The size of x ∷ y is equal to the size of y if x is a member
      -- of y, and otherwise it is equal to the successor of the size
      -- of y.

      Cons′ :
        A → Finite-subset-of A →
        (ℕ → Proposition a) → (ℕ → Type a)
      Cons′ x y ∣y∣≡ n =
        x ∈ y × proj₁ (∣y∣≡ n)
          ⊎
        Cons″ x y ∣y∣≡ n

      Cons″ :
        A → Finite-subset-of A →
        (ℕ → Proposition a) → (ℕ → Type a)
      Cons″ x y ∣y∣≡ zero    = ⊥
      Cons″ x y ∣y∣≡ (suc n) = x ∉ y × proj₁ (∣y∣≡ n)

    Cons′-propositional :
      ∀ Hyp n → Is-proposition (Cons′ x y Hyp n)
    Cons′-propositional Hyp zero =
      ⊎-closure-propositional
        (λ _ ())
        (×-closure 1 ∈-propositional (proj₂ (Hyp 0)))
        ⊥-propositional
    Cons′-propositional Hyp (suc n) =
      ⊎-closure-propositional
        (λ (x∈y , _) (x∉y , _) → x∉y x∈y)
        (×-closure 1 ∈-propositional (proj₂ (Hyp (suc n))))
        (×-closure 1 (¬-propositional ext) (proj₂ (Hyp n)))

    Cons :
      A → Finite-subset-of A →
      (ℕ → Proposition a) → (ℕ → Proposition a)
    Cons x y Hyp n =
        Cons′ x y Hyp n
      , Cons′-propositional _ _

    drop-lemma :
      Cons′ x (x ∷ y) (Cons x y H) n ≃ Cons′ x y H n
    drop-lemma {x = x} {y = y} {H = H} {n = n} =
      Cons′ x (x ∷ y) (Cons x y H) n   ↔⟨⟩
      x ∈ x ∷ y × Cons′ x y H n ⊎ C n  ↔⟨ drop-⊥-right (C↔⊥ n) ⟩
      x ∈ x ∷ y × Cons′ x y H n        ↔⟨ drop-⊤-left-× (λ _ → x∈x∷y↔⊤) ⟩
      Cons′ x y H n                    □
      where
      C = Cons″ x (x ∷ y) (Cons x y H)

      x∈x∷y↔⊤ : x ∈ x ∷ y ↔ ⊤
      x∈x∷y↔⊤ =
        x ∈ x ∷ y        ↔⟨ ∈∷≃ ⟩
        x ≡ x ∥⊎∥ x ∈ y  ↝⟨ Trunc.inhabited⇒∥∥↔⊤ ∣ inj₁ (refl _) ∣ ⟩□
        ⊤                □

      C↔⊥ : ∀ n → C n ↔ ⊥
      C↔⊥ zero    = ⊥↔⊥
      C↔⊥ (suc n) =
        x ∉ x ∷ y × Cons′ x y H n  ↝⟨ →-cong ext x∈x∷y↔⊤ F.id ×-cong F.id ⟩
        ¬ ⊤ × Cons′ x y H n        ↝⟨ inverse (Bijection.⊥↔uninhabited (_$ _)) ×-cong F.id ⟩
        ⊥₀ × Cons′ x y H n         ↝⟨ ×-left-zero ⟩□
        ⊥                          □

    swap-lemma′ :
      ∀ n →
      x ∈ y ∷ z × Cons′ y z H n ⊎ Cons″ x (y ∷ z) (Cons y z H) n →
      y ∈ x ∷ z × Cons′ x z H n ⊎ Cons″ y (x ∷ z) (Cons x z H) n
    swap-lemma′ {x = x} {y = y} {z = z} {H = H} = λ where
      n (inj₁ (x∈y∷z , inj₁ (y∈z , p))) →
        inj₁ ( ∈→∈∷ y∈z
             , inj₁
                 ( (                 $⟨ x∈y∷z ⟩
                    x ∈ y ∷ z        ↔⟨ ∈∷≃ ⟩
                    x ≡ y ∥⊎∥ x ∈ z  ↝⟨ Trunc.∥∥-map P.[ (flip (subst (_∈ z)) y∈z ∘ sym) , id ] ⟩
                    ∥ x ∈ z ∥        ↔⟨ Trunc.∥∥↔ ∈-propositional ⟩□
                    x ∈ z            □)
                 , p
                 )
             )

      (suc n) (inj₁ (x∈y∷z , inj₂ (y∉z , p))) →
        Trunc.rec (Cons′-propositional (Cons x z H) _)
          P.[ (λ x≡y →
                inj₁ ( ≡→∈∷ (sym x≡y)
                     , inj₂ ( (x ∈ z  ↝⟨ subst (_∈ z) x≡y ⟩
                               y ∈ z  ↝⟨ y∉z ⟩□
                               ⊥      □)
                            , p
                            )
                     ))
            , (λ x∈z →
                 inj₂ ( (y ∈ x ∷ z        ↔⟨ ∈∷≃ ⟩
                         y ≡ x ∥⊎∥ y ∈ z  ↝⟨ Trunc.∥∥-map P.[ flip (subst (_∈ z)) x∈z ∘ sym , id ] ⟩
                         ∥ y ∈ z ∥        ↝⟨ Trunc.∥∥-map y∉z ⟩
                         ∥ ⊥ ∥            ↔⟨ Trunc.∥∥↔ ⊥-propositional ⟩□
                         ⊥                □)
                      , inj₁ (x∈z , p)
                      ))
            ]
          (_≃_.to ∈∷≃ x∈y∷z)

      (suc n) (inj₂ (x∉y∷z , inj₁ (y∈z , p))) →
        inj₁ ( ∈→∈∷ y∈z
             , inj₂ ( (x ∈ z      ↝⟨ ∈→∈∷ ⟩
                       x ∈ y ∷ z  ↝⟨ x∉y∷z ⟩□
                       ⊥          □)
                    , p
                    )
             )

      (suc (suc n)) (inj₂ (x∉y∷z , inj₂ (y∉z , p))) →
        inj₂ ( (y ∈ x ∷ z            ↔⟨ ∈∷≃ ⟩
                y ≡ x ∥⊎∥ y ∈ z      ↝⟨ ≡→∈∷ ∘ sym Trunc.∥⊎∥-cong id ⟩
                x ∈ y ∷ z ∥⊎∥ y ∈ z  ↝⟨ Trunc.∥∥-map P.[ x∉y∷z , y∉z ] ⟩
                ∥ ⊥ ∥                ↔⟨ Trunc.∥∥↔ ⊥-propositional ⟩□
                ⊥                    □)
             , inj₂ ( (x ∈ z      ↝⟨ ∈→∈∷ ⟩
                       x ∈ y ∷ z  ↝⟨ x∉y∷z ⟩□
                       ⊥          □)
                    , p
                    )
             )

    swap-lemma :
      Cons′ x (y ∷ z) (Cons y z H) n ≃
      Cons′ y (x ∷ z) (Cons x z H) n
    swap-lemma {x = x} {y = y} {z = z} {H = H} {n = n} =
      _↠_.from
        (Eq.≃↠⇔
           (Cons′-propositional _ _)
           (Cons′-propositional _ _))
        (record { to = swap-lemma′ _; from = swap-lemma′ _ })

    r : Rec A (ℕ → Proposition a)
    r .[]ʳ n = ↑ _ (n ≡ 0) , ↑-closure 1 ℕ-set

    r .∷ʳ = Cons

    r .dropʳ x y Hyp = ⟨ext⟩ λ _ →
      _↔_.to (ignore-propositional-component
             (H-level-propositional ext 1)) $
      Univ.≃⇒≡ univ drop-lemma

    r .swapʳ x y z Hyp = ⟨ext⟩ λ _ →
      _↔_.to (ignore-propositional-component
             (H-level-propositional ext 1)) $
      Univ.≃⇒≡ univ swap-lemma

    r .is-setʳ =
      Π-closure ext 2 λ _ →
      Univ.∃-H-level-H-level-1+ ext univ 1

-- Size.

infix 4 ∣_∣≡_

∣_∣≡_ : {A : Type a} → Finite-subset-of A → ℕ → Type a
∣ x ∣≡ n = proj₁ (Size x n)

-- The size predicate is propositional.

∣∣≡-propositional :
  (x : Finite-subset-of A) → Is-proposition (∣ x ∣≡ n)
∣∣≡-propositional x = proj₂ (Size x _)

-- Unit tests documenting the computational behaviour of ∣_∣≡_.

_ : (∣ [] {A = A} ∣≡ n) ≡ ↑ _ (n ≡ 0)
_ = refl _

_ : ∀ {A : Type a} {x : A} {y} →
    (∣ x ∷ y ∣≡ zero) ≡ (x ∈ y × ∣ y ∣≡ zero ⊎ ⊥)
_ = refl _

_ : (∣ x ∷ y ∣≡ suc n) ≡ (x ∈ y × ∣ y ∣≡ suc n ⊎ x ∉ y × ∣ y ∣≡ n)
_ = refl _

-- The size predicate is functional.

∣∣≡-functional :
  (x : Finite-subset-of A) → ∣ x ∣≡ m → ∣ x ∣≡ n → m ≡ n
∣∣≡-functional x = elim-prop e x _ _
  where
  e : Elim-prop (λ x → ∀ m n → ∣ x ∣≡ m → ∣ x ∣≡ n → m ≡ n)
  e .[]ʳ m n (lift m≡0) (lift n≡0) =
    m  ≡⟨ m≡0 ⟩
    0  ≡⟨ sym n≡0 ⟩∎
    n  ∎

  e .∷ʳ {y = y} x hyp = λ where
    m n (inj₁ (x∈y , ∣y∣≡m)) (inj₁ (x∈y′ , ∣y∣≡n)) →
      hyp m n ∣y∣≡m ∣y∣≡n

    (suc m) (suc n) (inj₂ (x∉y , ∣y∣≡m)) (inj₂ (x∉y′ , ∣y∣≡n)) →
      cong suc (hyp m n ∣y∣≡m ∣y∣≡n)

    _ (suc _) (inj₁ (x∈y , _)) (inj₂ (x∉y , _)) → ⊥-elim (x∉y x∈y)
    (suc _) _ (inj₂ (x∉y , _)) (inj₁ (x∈y , _)) → ⊥-elim (x∉y x∈y)

  e .is-propositionʳ _ =
    Π-closure ext 1 λ _ →
    Π-closure ext 1 λ _ →
    Π-closure ext 1 λ _ →
    Π-closure ext 1 λ _ →
    ℕ-set

-- If truncated equality is decidable, then one can compute the size
-- of a finite subset.

size :
  ((x y : A) → Dec ∥ x ≡ y ∥) →
  (x : Finite-subset-of A) → ∃ λ n → ∣ x ∣≡ n
size equal? = elim-prop e
  where
  e : Elim-prop _
  e .[]ʳ = 0 , lift (refl _)

  e .∷ʳ {y = y} x (n , ∣y∣≡n) =
    case member? equal? x y of λ x∈?y →
        if x∈?y then n else suc n
      , lemma ∣y∣≡n x∈?y
    where
    lemma :
      ∣ y ∣≡ n →
      (x∈?y : Dec (x ∈ y)) →
      ∣ x ∷ y ∣≡ if x∈?y then n else suc n
    lemma ∣y∣≡n (yes x∈y) = inj₁ (x∈y , ∣y∣≡n)
    lemma ∣y∣≡n (no  x∉y) = inj₂ (x∉y , ∣y∣≡n)

  e .is-propositionʳ x (m , ∣x∣≡m) (n , ∣x∣≡n) =
    Σ-≡,≡→≡ (m  ≡⟨ ∣∣≡-functional x ∣x∣≡m ∣x∣≡n ⟩∎
             n  ∎)
            (∣∣≡-propositional x _ _)

-- A variant of size that uses Erased.

sizeᴱ :
  ((x y : A) → Dec-Erased ∥ x ≡ y ∥) →
  (x : Finite-subset-of A) → ∃ λ n → Erased (∣ x ∣≡ n)
sizeᴱ equal? = elim-prop e
  where
  e : Elim-prop _
  e .[]ʳ = 0 , [ lift (refl _) ]

  e .∷ʳ {y = y} x (n , [ ∣y∣≡n ]) =
    case member?ᴱ equal? x y of λ x∈?y →
        if x∈?y then n else suc n
      , [ lemma ∣y∣≡n x∈?y ]
    where
    @0 lemma :
      ∣ y ∣≡ n →
      (x∈?y : Dec-Erased (x ∈ y)) →
      ∣ x ∷ y ∣≡ if x∈?y then n else suc n
    lemma ∣y∣≡n (yes [ x∈y ]) = inj₁ (x∈y , ∣y∣≡n)
    lemma ∣y∣≡n (no  [ x∉y ]) = inj₂ (x∉y , ∣y∣≡n)

  e .is-propositionʳ x (m , [ ∣x∣≡m ]) (n , [ ∣x∣≡n ]) =
    Σ-≡,≡→≡ (m  ≡⟨ EC.Very-stable→Stable 1
                     (EC.Decidable-equality→Very-stable-≡ Nat._≟_)
                     _ _
                     [ ∣∣≡-functional x ∣x∣≡m ∣x∣≡n ] ⟩∎
             n  ∎)
            (EC.H-level-Erased 1 (∣∣≡-propositional x) _ _)

------------------------------------------------------------------------
-- Finite types

-- A type is finite if there is some finite subset of the type for
-- which every element of the type is a member of the subset.

is-finite : Type a → Type a
is-finite A = ∃ λ (s : Finite-subset-of A) → ∀ x → x ∈ s

-- The is-finite predicate is propositional.

is-finite-propositional : Is-proposition (is-finite A)
is-finite-propositional (x , p) (y , q) =
                         $⟨ (λ z → record { to = λ _ → q z; from = λ _ → p z }) ⟩
  (∀ z → z ∈ x ⇔ z ∈ y)  ↔⟨ inverse extensionality ⟩
  x ≡ y                  ↝⟨ ignore-propositional-component (Π-closure ext 1 (λ _ → ∈-propositional)) ⟩□
  (x , p) ≡ (y , q)      □

------------------------------------------------------------------------
-- Lists can be converted to finite subsets

-- Converts lists to finite subsets.

from-List : List A → Finite-subset-of A
from-List = L.foldr _∷_ []

-- Membership in the resulting set is equivalent to truncated
-- membership in the list.

∥∈∥≃∈-from-List : ∥ x BE.∈ ys ∥ ≃ (x ∈ from-List ys)
∥∈∥≃∈-from-List {x = x} {ys = ys} = _↠_.from
  (Eq.≃↠⇔
     Trunc.truncation-is-proposition
     ∈-propositional)
  (record { to = to _; from = from _ })
  where
  to : ∀ ys → ∥ x BE.∈ ys ∥ → x ∈ from-List ys
  to []       = Trunc.rec ∈-propositional (λ ())
  to (y ∷ ys) = Trunc.rec ∈-propositional
                  P.[ ≡→∈∷ , ∈→∈∷ ∘ to ys ∘ ∣_∣ ]

  from : ∀ ys → x ∈ from-List ys → ∥ x BE.∈ ys ∥
  from [] ()
  from (y ∷ ys) =
    Trunc.rec
      Trunc.truncation-is-proposition
      P.[ ∣_∣ ∘ inj₁ , Trunc.∥∥-map inj₂ ∘ from ys ] ∘
    _≃_.to ∈∷≃

------------------------------------------------------------------------
-- Some definitions related to the definitions in Bag-equivalence

-- Finite subsets can be expressed as lists quotiented by set
-- equivalence.

≃List/∼ : Finite-subset-of A ≃ List A / _∼[ set ]_
≃List/∼ = from-bijection (record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  })
  where
  cons : A → List A / _∼[ set ]_ → List A / _∼[ set ]_
  cons x = (x ∷_) Q./-map λ _ _ → refl _ BE.∷-cong_

  to : Finite-subset-of A → List A / _∼[ set ]_
  to = rec r
    where
    r : Rec _ _
    r .[]ʳ       = Q.[ [] ]
    r .∷ʳ x _ y  = cons x y
    r .is-setʳ   = Q./-is-set
    r .dropʳ x _ = Q.elim-prop λ where
      .Q.[]ʳ xs → Q.[]-respects-relation λ z →
        z BE.∈ x ∷ x ∷ xs      ↝⟨ record { to = P.[ inj₁ , id ]; from = inj₂ } ⟩□
        z BE.∈ x ∷ xs          □
      .Q.is-propositionʳ _ → Q./-is-set

    r .swapʳ x y _ = Q.elim-prop λ where
      .Q.[]ʳ xs → Q.[]-respects-relation λ z →
        z BE.∈ x ∷ y ∷ xs  ↔⟨ BE.swap-first-two z ⟩□
        z BE.∈ y ∷ x ∷ xs  □
      .Q.is-propositionʳ _ → Q./-is-set

  from : List A / _∼[ set ]_ → Finite-subset-of A
  from {A = A} = Q.rec λ where
    .Q.[]ʳ → from-List

    .Q.[]-respects-relationʳ {x = xs} {y = ys} xs∼ys →
      _≃_.from extensionality λ z →
        z ∈ from-List xs  ↔⟨ inverse ∥∈∥≃∈-from-List ⟩
        ∥ z BE.∈ xs ∥     ↔⟨ Trunc.∥∥-cong-⇔ {k = bijection} (xs∼ys z) ⟩
        ∥ z BE.∈ ys ∥     ↔⟨ ∥∈∥≃∈-from-List ⟩□
        z ∈ from-List ys  □

    .Q.is-setʳ → is-set

  to∘from : ∀ x → to (from x) ≡ x
  to∘from = Q.elim-prop λ where
      .Q.[]ʳ               → lemma
      .Q.is-propositionʳ _ → Q./-is-set
    where
    lemma : ∀ xs → to (from-List xs) ≡ Q.[ xs ]
    lemma []       = refl _
    lemma (x ∷ xs) =
      to (from-List (x ∷ xs))                              ≡⟨⟩
      ((x ∷_) Q./-map _) (to (from-List xs))               ≡⟨ cong ((x ∷_) Q./-map _) (lemma xs) ⟩
      ((x ∷_) Q./-map λ _ _ → refl _ BE.∷-cong_) Q.[ xs ]  ≡⟨⟩
      Q.[ x ∷ xs ]                                         ∎

  from∘to : ∀ x → from (to x) ≡ x
  from∘to = elim-prop e
    where
    e : Elim-prop _
    e .[]ʳ = refl _

    e .∷ʳ {y = y} x hyp =
      from (to (x ∷ y))     ≡⟨⟩
      from (cons x (to y))  ≡⟨ Q.elim-prop
                                 {P = λ y → from (cons x y) ≡ x ∷ from y}
                                 (λ where
                                    .Q.[]ʳ _             → refl _
                                    .Q.is-propositionʳ _ → is-set)
                                 (to y) ⟩
      x ∷ from (to y)       ≡⟨ cong (x ∷_) hyp ⟩∎
      x ∷ y                 ∎

    e .is-propositionʳ _ = is-set

-- A truncated variant of the proof-relevant membership relation from
-- Bag-equivalence can be expressed in terms of _∈_.

∥∈∥≃∈ : ∥ x BE.∈ ys ∥ ≃ (x ∈ _≃_.from ≃List/∼ Q.[ ys ])
∥∈∥≃∈ = ∥∈∥≃∈-from-List

------------------------------------------------------------------------
-- Fresh numbers

-- One can always find a natural number that is distinct from those in
-- a given finite set of natural numbers.

fresh :
  (ns : Finite-subset-of ℕ) →
  ∃ λ (n : ℕ) → n ∉ ns
fresh ns =
  Σ-map id
    (λ {m} →
       Erased (∀ n → n ∈ ns → n < m)  ↝⟨ EC.map (_$ m) ⟩
       Erased (m ∈ ns → m < m)        ↝⟨ EC.map (∀-cong _ λ _ → Nat.+≮ 0) ⟩
       Erased (m ∉ ns)                ↝⟨ EC.Stable-¬ ⟩□
       m ∉ ns                         □)
    (elim e ns)
  where
  OK : @0 Finite-subset-of ℕ → @0 ℕ → Type
  OK ms m = Erased (∀ n → n ∈ ms → n < m)

  prop : Is-proposition (OK ms m)
  prop =
    EC.H-level-Erased 1 (
    Π-closure ext 1 λ _ →
    Π-closure ext 1 λ _ →
    ≤-propositional)

  ∷-max-suc :
    ∀ {ms n m} →
    OK ms n →
    OK (m ∷ ms) (Nat.max (suc m) n)
  ∷-max-suc {ms = ms} {n = n} {m = m} [ ub ] =
    [ (λ o →
         o ∈ m ∷ ms                   ↔⟨ ∈∷≃ ⟩
         o ≡ m ∥⊎∥ o ∈ ms             ↝⟨ Nat.≤-refl′ ∘ cong suc ∘ id Trunc.∥⊎∥-cong ub o ⟩
         o Nat.< suc m ∥⊎∥ o Nat.< n  ↝⟨ Trunc.rec ≤-propositional
                                           P.[ flip Nat.≤-trans (Nat.ˡ≤max _ n)
                                             , flip Nat.≤-trans (Nat.ʳ≤max (suc m) _)
                                             ] ⟩□
         o Nat.< Nat.max (suc m) n    □)
    ]

  e : Elim (λ ms → ∃ λ m → OK ms m)
  e .[]ʳ =
    0 , [ (λ _ ()) ]

  e .∷ʳ m (n , ub) =
    Nat.max (suc m) n , ∷-max-suc ub

  e .dropʳ {y = ns} m (n , ub) =
    _↔_.to (ignore-propositional-component prop)
      (proj₁ (subst (λ ms → ∃ λ m → OK ms m)
                    (drop {x = m} {y = ns})
                    ( Nat.max (suc m) (Nat.max (suc m) n)
                    , ∷-max-suc (∷-max-suc ub)
                    ))                                     ≡⟨ cong proj₁ $
                                                              push-subst-pair-× {y≡z = drop {x = m} {y = ns}} _
                                                                (λ (ms , m) → OK ms m)
                                                                {p = _ , ∷-max-suc (∷-max-suc ub)} ⟩

       Nat.max (suc m) (Nat.max (suc m) n)                 ≡⟨ Nat.max-assoc (suc m) {n = suc m} {o = n} ⟩

       Nat.max (Nat.max (suc m) (suc m)) n                 ≡⟨ cong (λ m → Nat.max m n) $ Nat.max-idempotent (suc m) ⟩∎

       Nat.max (suc m) n                                   ∎)

  e .swapʳ {z = ns} m n (o , ub) =
    _↔_.to (ignore-propositional-component prop)
      (proj₁ (subst (λ xs → ∃ λ m → OK xs m)
                    (swap {x = m} {y = n} {z = ns})
                    ( Nat.max (suc m) (Nat.max (suc n) o)
                    , ∷-max-suc (∷-max-suc ub)
                    ))                                     ≡⟨ cong proj₁ $
                                                              push-subst-pair-× {y≡z = swap {x = m} {y = n} {z = ns}} _
                                                                (λ (ms , m) → OK ms m)
                                                                {p = _ , ∷-max-suc (∷-max-suc ub)} ⟩

       Nat.max (suc m) (Nat.max (suc n) o)                 ≡⟨ Nat.max-assoc (suc m) {n = suc n} {o = o} ⟩

       Nat.max (Nat.max (suc m) (suc n)) o                 ≡⟨ cong (λ m → Nat.max m o) $ Nat.max-comm (suc m) (suc n) ⟩

       Nat.max (Nat.max (suc n) (suc m)) o                 ≡⟨ sym $ Nat.max-assoc (suc n) {n = suc m} {o = o} ⟩∎

       Nat.max (suc n) (Nat.max (suc m) o)                 ∎)

  e .is-setʳ _ =
    Σ-closure 2 ℕ-set λ _ →
    mono₁ 1 prop

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality