```------------------------------------------------------------------------
-- Atoms
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Atom where

open import Bag-equivalence
open import Equality.Propositional
open import Interval using (ext)
open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J as Bijection using (_↔_)
open import Equality.Decidable-UIP equality-with-J
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import Injection equality-with-J using (Injective)
import Nat equality-with-J as Nat
open import Univalence-axiom equality-with-J

-- Atoms.

record Atoms : Set₁ where
field
-- The type of atoms.

Name : Set

-- The type must be countably infinite.

countably-infinite : Name ↔ ℕ

-- Atoms have decidable equality.

_≟_ : Decidable-equality Name
_≟_ = Bijection.decidable-equality-respects
(inverse countably-infinite) Nat._≟_

-- Membership test.

member : (x : Name) (xs : List Name) → Dec (x ∈ xs)
member x []       = no (λ ())
member x (y ∷ xs) with x ≟ y
... | yes x≡y = yes (inj₁ x≡y)
... | no  x≢y with member x xs
...   | yes x∈xs = yes (inj₂ x∈xs)
...   | no  x∉xs = no [ x≢y , x∉xs ]

-- Conversions.

name : ℕ → Name
name = _↔_.from countably-infinite

code : Name → ℕ
code = _↔_.to countably-infinite

-- The name function is injective.

name-injective : Injective name
name-injective = _↔_.injective (inverse countably-infinite)

-- Distinct natural numbers are mapped to distinct names.

distinct-codes→distinct-names : ∀ {m n} → m ≢ n → name m ≢ name n
distinct-codes→distinct-names {m} {n} m≢n =
name m ≡ name n  ↝⟨ name-injective ⟩
m ≡ n            ↝⟨ m≢n ⟩□
⊥                □

-- Name is a set.

Name-set : Is-set Name
Name-set = decidable⇒set _≟_

-- One implementation of atoms, using natural numbers.

ℕ-atoms : Atoms
Atoms.Name               ℕ-atoms = ℕ
Atoms.countably-infinite ℕ-atoms = Bijection.id

-- Two sets of atoms, one for constants and one for variables.

record χ-atoms : Set₁ where
field
const-atoms var-atoms : Atoms

module C = Atoms const-atoms renaming (Name to Const)
module V = Atoms var-atoms   renaming (Name to Var)

open C public using (Const)
open V public using (Var)

-- One implementation of χ-atoms, using natural numbers.

χ-ℕ-atoms : χ-atoms
χ-atoms.const-atoms χ-ℕ-atoms = ℕ-atoms
χ-atoms.var-atoms   χ-ℕ-atoms = ℕ-atoms

-- The type of atoms is isomorphic to the unit type (assuming
-- univalence).

Atoms↔⊤ :
Univalence (# 0) →
Atoms ↔ ⊤
Atoms↔⊤ univ =
Atoms                          ↝⟨ eq ⟩
(∃ λ (Name : Set) → Name ↔ ℕ)  ↝⟨ ∃-cong (λ _ → Eq.↔↔≃′ ext ℕ-set) ⟩
(∃ λ (Name : Set) → Name ≃ ℕ)  ↝⟨ singleton-with-≃-↔-⊤ ext univ ⟩□
⊤                              □
where
open Atoms

eq : Atoms ↔ ∃ λ (Name : Set) → Name ↔ ℕ
eq = record
{ surjection = record
{ logical-equivalence = record
{ to   = λ a → Name a , countably-infinite a
; from = uncurry λ N c →
record { Name = N; countably-infinite = c }
}
; right-inverse-of = λ _ → refl
}
; left-inverse-of = λ _ → refl
}

-- The χ-atoms type is isomorphic to the unit type (assuming
-- univalence).

χ-atoms↔⊤ :
Univalence (# 0) →
χ-atoms ↔ ⊤
χ-atoms↔⊤ univ =
χ-atoms        ↝⟨ eq ⟩
Atoms × Atoms  ↝⟨ Atoms↔⊤ univ ×-cong Atoms↔⊤ univ ⟩
⊤ × ⊤          ↝⟨ ×-right-identity ⟩□
⊤              □
where
open χ-atoms

eq : χ-atoms ↔ Atoms × Atoms
eq = record
{ surjection = record
{ logical-equivalence = record
{ to   = λ a → const-atoms a , var-atoms a
; from = uncurry λ c v →
record { const-atoms = c; var-atoms = v }
}
; right-inverse-of = λ _ → refl
}
; left-inverse-of = λ _ → refl
}

-- If a property holds for one choice of atoms, then it holds for any
-- other choice of atoms (assuming univalence).

invariant :
∀ {p} →
Univalence (# 0) →
(P : χ-atoms → Set p) →
∀ a₁ a₂ → P a₁ → P a₂
invariant univ P a₁ a₂ =
subst P (_⇔_.to propositional⇔irrelevant
(mono₁ 0 \$ _⇔_.from contractible⇔↔⊤ \$
χ-atoms↔⊤ univ)
a₁ a₂)

-- If a property holds for χ-ℕ-atoms, then it holds for any choice of
-- atoms (assuming univalence).

one-can-restrict-attention-to-χ-ℕ-atoms :
∀ {p} →
Univalence (# 0) →
(P : χ-atoms → Set p) →
P χ-ℕ-atoms → ∀ a → P a
one-can-restrict-attention-to-χ-ℕ-atoms univ P p a =
invariant univ P χ-ℕ-atoms a p
```