Bij

Bag.agda

{-# OPTIONS --safe --backtracking-instance-search #-}
module Bag where

open import Prelude
open import Data.Nat.Base
open import Data.Fin.Computational.Base
open import Data.Fin.Computational.Instances.Finite
open import Structures.FinSet
open import Bij

open FinSet

private variable
  ℓ : Level
  A : 𝒰
  
-- free symmetric monoid

Bag : 𝒰 ℓ → 𝒰 ℓ
Bag {ℓ} A = Σ[ b ꞉ Bij {ℓ} ] (El b → A)

mapb : {A B : 𝒰 ℓ} → (A → B) → Bag A → Bag B
mapb f (b , mem) = b , f ∘ mem

emptyb : Bag A
emptyb = size 0 , λ ()

pureb : A → Bag A
pureb x = size 1 , λ _ → x

Bij.agda

{-# OPTIONS --safe --backtracking-instance-search #-}
module Bij where

open import Prelude
open import Data.Nat.Base
open import Data.Fin.Computational.Base
open import Data.Fin.Computational.Instances.Finite
open import Structures.FinSet

open FinSet

private variable
  ℓ : Level
  A : 𝒰

{-
-- using a groupoid quotient gives a termination error

data Bij : 𝒰 where
  obj      : ℕ → Bij
  hom      : ∀ {m n} → (α : Fin m ≃ Fin n) → obj m ＝ obj n
--  id-coh   : (n : ℕ) → hom {m = n} reflₑ ＝ reflₚ
  comp-coh : ∀ {m n o}
           → (α : Fin m ≃ Fin n)
           → (β : Fin n ≃ Fin o)
           → (hom (α ∙ₑ β)) ＝ (hom α ∙ₚ hom β)
  trunc    : is-groupoid Bij
-}

mutual
  data Bij {ℓ : Level} : 𝒰 ℓ where
    size : ℕ → Bij
    @0 un : (p q : Bij) → El p ≃ El q → p ＝ q

  El : Bij {ℓ} → 𝒰 ℓ 
  El {ℓ} (size n)     = Lift ℓ (Fin n)
  El     (un _ _ e i) = ua e i

@0 is-embedding-El : is-embedding (El {ℓ})
is-embedding-El u (b₁ , e₁) (b₂ , e₂) =
  Σ-path (un b₁ b₂ (=→≃ (e₁ ∙ e₂ ⁻¹))) $
  subst-path-left _ _ ∙
    (⌜ ua (=→≃ (e₁ ∙ e₂ ⁻¹)) ⌝ ⁻¹ ∙ e₁  ~⟨ ap! (ua-η _) ⟩
     ⌜ (e₁ ∙ e₂ ⁻¹) ⁻¹ ⌝ ∙ e₁           ~⟨ ap! (sym-∙ _ _) ⟩
     (e₂ ⁻¹ ⁻¹ ∙ e₁ ⁻¹) ∙ e₁            ~⟨ ∙-cancel-r _ _ ⟩
     e₂                                 ∎)

elimBij : ∀ {ℓ} {P : Bij {ℓ} → 𝒰 ℓ}
        → (ps : (n : ℕ) → P (size n))
        → (@0 pu : ∀ {p q} → (Pp : P p) → (Pq : P q)
                 → (e : El p ≃ El q)
                 → ＜ Pp ／ (λ j → P (un p q e j)) ＼ Pq ＞)
        → (b : Bij) → P b
elimBij     ps pu (size n)     = ps n
elimBij {P} ps pu (un p q e i) = pu {p} {q} (elimBij {P = P} ps pu p) (elimBij {P = P} ps pu q) e i

bishop-finite-El : (b : Bij {ℓ}) → is-bishop-finite (El b)
bishop-finite-El =
  elimBij (λ n → manifest-bishop-finite→is-bishop-finite)
          (λ bfp bfq e → to-pathᴾ (hlevel 1 _ bfq))

@0 bishop-finite-fib-El : is-bishop-finite A → fibre El A
bishop-finite-fib-El {A} bf =
  ∥-∥₁.elim (λ _ → is-embedding-El A)
            (λ ee → size (cardinality bf) , ua (lift≃id ∙ ee ⁻¹))
            (enumeration₁ bf)

@0 fib-el≅bish : fibre El A ≅ is-bishop-finite A
fib-el≅bish {A} = to , iso bishop-finite-fib-El ri li
  where
  to : fibre El A → is-bishop-finite A
  to (b , e) = subst is-bishop-finite e (bishop-finite-El b)
  ri : bishop-finite-fib-El is-right-inverse-of to
  ri x = hlevel 1 (to (bishop-finite-fib-El x)) x
  li : bishop-finite-fib-El is-left-inverse-of to
  li x = is-embedding-El A (bishop-finite-fib-El (to x)) x

bij→finset : Bij → FinSet ℓ
bij→finset b = fin-set (El b) (bishop-finite-El b)

@0 finset→bij : FinSet ℓ → Bij
finset→bij fs = fst (bishop-finite-fib-El (fs .has-bishop-finite))

@0 finset→bij→finset : finset→bij {ℓ} is-right-inverse-of bij→finset
finset→bij→finset fs with (bishop-finite-fib-El (fs .has-bishop-finite))
... | b , e = fs-path e

@0 bij→finset→bij : finset→bij {ℓ} is-left-inverse-of bij→finset
bij→finset→bij b = un (finset→bij (bij→finset b)) b (aux b)
  where
  aux : ∀ b → El (finset→bij (bij→finset b)) ≃ El b
  aux b with (bishop-finite-fib-El ((bij→finset b) .has-bishop-finite))
  ... | x , p = =→≃ p 

@0 bij≅finset : Bij ≅ FinSet ℓ
bij≅finset {ℓ} = bij→finset , iso finset→bij finset→bij→finset bij→finset→bij
  
@0 bij-is-groupoid : is-groupoid (Bij {ℓ})
bij-is-groupoid = ≅→is-of-hlevel 3 bij≅finset FinSet-is-groupoid

is-set-el : (b : Bij {ℓ}) → (n : HLevel)
          → is-of-hlevel (2 + n) (El b)
is-set-el b n = hlevel (2 + n) ⦃ x = H-Level-hedberg ⦃ di = is-bishop-finite→is-discrete ⦃ bf = bishop-finite-El b ⦄ ⦄ ⦄

-- operations

card : Bij {ℓ} → ℕ
card b = bishop-finite-El b .cardinality

enum : (b : Bij {ℓ}) → ∥ El b ≃ Fin (card b) ∥₁
enum b = bishop-finite-El b .enumeration₁

bsuc : Bij {ℓ} → Bij {ℓ}
bsuc = size ∘ suc ∘ card

bplus : Bij {ℓ} → Bij {ℓ} → Bij {ℓ}
bplus b₁ b₂ = size (card b₁ + card b₂)