Variant of Andrej's code to try to understand choice and 'type like'.

SetoidChoice.agda

{-# OPTIONS --safe --without-K #-}
-- Characterizations of setoids that satisfy the axiom of choice.
--
-- We define four properties of a setoid A:
--
-- (1) A satisfies the axiom of choice
-- (2) A is projective
-- (3) A is isomorphic to a type
-- (4) A has canonical elements
--
-- We show that (1) ⇔ (2)
--
-- We show that (2) ⇒ (3) when the carrier of A is an h-set.
-- We show that (3) ⇒ (4) ⇒ (1).
--
-- As a corrolary we conclude that the setoid of natural numbers satisfies choice.
-- (This is known as countable choice.)
--
-- Author: Andrej Bauer
-- January 6, 2022

-- This version has been edited by Jacques Carette, January 10--12.
-- It is not meant to be 'better', but rather an experiment with writing things
-- somewhat differently. And it's still a WIP.
-- also adds (2) ⇔ (4), so that we have 1, 2, 4 all equivalent and (3) being the
-- odd one out.

open import Level
open import Relation.Binary using (Setoid)
import Data.Integer as ℤ
open import Data.Product renaming (proj₁ to fst; proj₂ to snd)
open import Data.Product.Properties -- using (Σ-≡,≡↔≡)
open import Data.Unit using (⊤; tt)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; setoid)
open import Relation.Nullary using (¬_)
open import Function.Equality using (_⟶_; Π; _⟨$⟩_; cong; _∘_)
import Function.Inverse as FI
import Function.Equivalence as FE
open import Function.Bundles using (module Inverse)
import  Relation.Binary.Reasoning.Setoid as SetoidR

module SetoidChoice where

  -- ===== Preliminaries =====

  -- variables to cut down on declaration noise
  private
    variable
      c ℓ c₁ ℓ₁ c₂ ℓ₂ r c' ℓ' : Level
      A : Setoid c₁ ℓ₁
      B : Setoid c₂ ℓ₂

  -- Setoid Utilities
  ∣_∣ : Setoid c ℓ → Set c
  ∣_∣ = Setoid.Carrier

  [_][_≈_] : (C : Setoid c ℓ) → (x y : ∣ C ∣) → Set ℓ
  [_][_≈_] = Setoid._≈_

  SetoidLift : ∀ {c ℓ} c' ℓ' → Setoid c ℓ → Setoid (c ⊔ c') (ℓ ⊔ ℓ')
  SetoidLift c' ℓ' A =
    record { Carrier = Lift c' ∣ A ∣
           ; _≈_ = λ x y → Lift ℓ' (lower x ≈ lower y)
           ; isEquivalence = record { refl = lift refl
                                    ; sym = λ ξ → lift (Setoid.sym A (lower ξ))
                                    ; trans = λ ζ ξ → lift (Setoid.trans A (lower ζ) (lower ξ))
                                    }
           }
    where
      open Setoid A

  -- the definition of h-sets

  is-set : Set ℓ → Set ℓ
  is-set A = ∀ {x y : A} {p q : x ≡ y} → p ≡ q

  _≅_ : (A : Setoid c₁ ℓ₁) (B : Setoid c₂ ℓ₂) → Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂)
  _≅_ = FI.Inverse

  -- A binary relation on setoids A and B is a relation which respects equivalence
  -- (does this exist in the standard library).

  record SetoidRelation k (A : Setoid c₁ ℓ₁) (B : Setoid c₂ ℓ₂) : Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂ ⊔ suc k) where
    private
      module A = Setoid A
      module B = Setoid B
    field
      _∼_ : ∣ A ∣ → ∣ B ∣ → Set k
      resp-∼ : ∀ {x₁ x₂ y₁ y₂} → x₁ A.≈ x₂ → y₁ B.≈ y₂ → x₁ ∼ y₁ → x₂ ∼ y₂

  module _ {A : Setoid c ℓ} {B : Setoid c' ℓ'} where
    private
      module A = Setoid A
      module B = Setoid B

    -- a witness of a point (in B) that is related to a given one in A
    record RelTo  (R : SetoidRelation r A B) (a : ∣ A ∣ ) : Set (c ⊔ c' ⊔ ℓ ⊔ ℓ' ⊔ r) where
      constructor relat
      open SetoidRelation R
      field
        pt : ∣ B ∣
        relTo : a ∼ pt

    open SetoidRelation

    -- Given a setoid function f : A ⟶ B, the points b that are related to f ⟨$⟩ a, as a relation from A to B
    f-rel : A ⟶ B → SetoidRelation ℓ' A B
    f-rel f ._∼_      a     b                                 = f ⟨$⟩ a B.≈ b
    f-rel f .resp-∼ {a₁} {a₂} {b₁} {b₂} a₁≈a₂ b₁≈b₂  fa₁≈b₁ = begin
      f ⟨$⟩ a₂ ≈⟨ cong f (Setoid.sym A a₁≈a₂) ⟩
      f ⟨$⟩ a₁ ≈⟨ fa₁≈b₁ ⟩
      b₁      ≈⟨ b₁≈b₂ ⟩
      b₂ ∎
      where open SetoidR B

    -- same as above, but f runs in the opposite direction
    f⁻¹-rel : B ⟶ A → SetoidRelation ℓ A B
    f⁻¹-rel f ._∼_      a     b                                 = f ⟨$⟩ b A.≈ a
    f⁻¹-rel f .resp-∼ {a₁} {a₂} {b₁} {b₂} a₁≈a₂ b₁≈b₂  fa₁≈b₁ = begin
      f ⟨$⟩ b₂ ≈⟨ cong f (Setoid.sym B b₁≈b₂) ⟩
      f ⟨$⟩ b₁ ≈⟨ fa₁≈b₁ ⟩
      a₁      ≈⟨ a₁≈a₂ ⟩
      a₂ ∎
      where open SetoidR A

  -- A SetoidRelation induces a Setoid
  record relWitness {k} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} (R : SetoidRelation k A B) : Set (c₁ ⊔ c₂ ⊔ k ) where
    constructor relW
    open SetoidRelation R
    field
      a∈A : ∣ A ∣
      b∈B : ∣ B ∣
      related : a∈A ∼ b∈B

  open relWitness

  RelSetoid : ∀ {k} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} → SetoidRelation k A B → Setoid (c₁ ⊔ c₂ ⊔ k) (ℓ₁ ⊔ ℓ₂)
  RelSetoid             R .Setoid.Carrier = relWitness R
  RelSetoid {A = A} {B} R .Setoid._≈_     w₁ w₂ = [ A ][ w₁ .a∈A ≈ w₂ .a∈A ] × [ B ][ w₁ .b∈B ≈ w₂ .b∈B ]
  RelSetoid {A = A} {B} R .Setoid.isEquivalence   = record { refl = Setoid.refl A , Setoid.refl B
                                                           ; sym = map (Setoid.sym A) (Setoid.sym B)
                                                           ; trans = zip (Setoid.trans A) (Setoid.trans B) }

  -- The definition of surjective setoid morphism

  surjective : {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} → A ⟶ B → Set (c₁ ⊔ c₂ ⊔ ℓ₂)
  surjective {B = B} f = ∀ y → ∃ λ x → f ⟨$⟩ x ≈ y where open Setoid B

  -- The definition of a split setoid morphism
  record split {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} (f : A ⟶ B) : Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
    constructor splits
    open Setoid B
    field
      f⁻¹ : B ⟶ A
      right-inv : ∀ y → f ⟨$⟩ (f⁻¹ ⟨$⟩ y) ≈ y

  open split

  -- A choice morphism, for a given total SetoidRelation.
  record Choice⇒ (A : Setoid c ℓ) (B : Setoid c' ℓ') (R : SetoidRelation r A B) (tot : ∀ x → RelTo R x) : Set (c ⊔ ℓ ⊔ c' ⊔ ℓ' ⊔ r) where
    constructor chooser
    open SetoidRelation R
    field
      choose : A ⟶ B
      coherent-choice : (x : ∣ A ∣ ) → x ∼ (choose ⟨$⟩ x)

  -- A is type-like if it is isomorphic to a setoid whose equivalence is propositional equality _≡_

  record type-like (A : Setoid c ℓ) t : Set (suc c ⊔ ℓ ⊔ suc t) where
    field
      type-like-to : Set t
      type-like-≅ : A ≅ setoid type-like-to


  module _ (A : Setoid c ℓ) where
    open Setoid A
    private
      _○_ = trans
      ⟺ = sym

    -- ===== Notions of “A satisfies choice” =====

    -- A satisfies choice if every total relation has a choice morphism

    satisfies-choice : ∀ c' ℓ' r → Set (c ⊔ ℓ ⊔ suc c' ⊔ suc ℓ' ⊔ suc r)
    satisfies-choice c' ℓ' r = ∀ (B : Setoid c' ℓ') (R : SetoidRelation r A B) → (tot : ∀ x → RelTo R x) → Choice⇒ A B R tot

    -- A is projective if every surjection onto A is split

    projective : ∀ c' ℓ' → Set (c ⊔ ℓ ⊔ suc c' ⊔ suc ℓ')
    projective c' ℓ' = ∀ (B : Setoid c' ℓ') (f : B ⟶ A) → surjective f → split f

    -- A has “canonical elements” if a function chooses (canonical) representatives from each equivalence class

    record canonical-elements : Set (c ⊔ ℓ) where
      constructor canon-elts
      field
        canon : Carrier → Carrier
        canon-≈ : ∀ x → canon x ≈ x
        canon-≡ : ∀ {x y} → x ≈ y → canon x ≡ canon y

    -- ===== Theorems ====

    -- A is projective iff it satisfies choice

    satisfies-choice⇒projective : ∀ c' ℓ' → satisfies-choice c' ℓ' ℓ -> projective c' ℓ'
    satisfies-choice⇒projective c' ℓ' ac B f s = splits (choose sc) (coherent-choice sc)
      where
        open Choice⇒
        rt : ∀ b → RelTo (f⁻¹-rel f) b
        rt b = let (a , fa≈b) = s b in relat a fa≈b
        sc = ac _ (f⁻¹-rel f) rt

    projective⇒satisfies-choice : ∀ c' ℓ' → projective (c ⊔ ℓ ⊔ c') (ℓ ⊔ ℓ') → satisfies-choice c' ℓ' ℓ
    projective⇒satisfies-choice c' ℓ' p B R r =
                                chooser u λ x → R.resp-∼ (right-inv uθ x) (Setoid.refl B) (related (f⁻¹ uθ ⟨$⟩ x))
        where
        module R = SetoidRelation R
        C = RelSetoid R
        uθ = p C
               (record { _⟨$⟩_ = a∈A ; cong = fst })
               λ x → relW x (RelTo.pt (r x)) (RelTo.relTo (r x)) , refl

        u : A ⟶ B
        u = record { _⟨$⟩_ = λ x → b∈B (f⁻¹ uθ ⟨$⟩ x)
                   ; cong = λ ξ → snd (cong (f⁻¹ uθ) ξ)
                   }

    -- If A is projective then it is type-like.
    -- Note that here we need the assumption that the carrier of A is a set.

    projective⇒type-like : is-set ∣ A ∣ → projective c c → type-like A c
    projective⇒type-like σ p =
      record { type-like-to = Σ Carrier (λ x → f ⟨$⟩ x ≡ x )
             ; type-like-≅ = record
               { to = record { _⟨$⟩_ = λ x → (f ⟨$⟩ x , cong f (right-inv fθ x))
                             ; cong = λ ξ → Σ-≡,≡↔≡ .Inverse.f (cong f ξ , σ) }
               ; from = record { _⟨$⟩_ = fst
                               ; cong = λ i≡j → reflexive (≡.cong fst i≡j) }
               ; inverse-of = record { left-inverse-of = right-inv fθ
                                     ; right-inverse-of = λ eq → Σ-≡,≡↔≡ .Inverse.f (snd eq , σ) }
               }
             }
      where
        fθ = p (setoid Carrier)
               (record { _⟨$⟩_ = λ x → x ; cong = λ { ≡.refl → refl } })
               (λ y → y , refl)

        f : A ⟶ setoid Carrier
        f = f⁻¹ fθ

    -- If A is type-like then it has canonical elements

    type-like⇒canonical-elements : type-like A c → canonical-elements
    type-like⇒canonical-elements
       record { type-like-≅ = record { to = f ; from = g ; inverse-of = record {left-inverse-of = ξ ; right-inverse-of = τ } } }
       = canon-elts (g ∘ f ⟨$⟩_) ξ λ ξ → ≡.cong (g ⟨$⟩_) (cong f ξ)

    -- If A has canonical elements then it satisfies choice

    canonical-elements⇒satisfies-choice : canonical-elements → satisfies-choice c' ℓ' r
    canonical-elements⇒satisfies-choice ce B R r
      =  chooser u λ x →  R.resp-∼ (canon-≈ x) (Setoid.reflexive B ≡.refl) (RelTo.relTo (r (canon x)))
      where
        open canonical-elements ce
        module R = SetoidRelation R
        u : A ⟶ B
        u = record { _⟨$⟩_ = λ x → RelTo.pt (r (canon x))
                   ; cong = λ { ξ → Setoid.reflexive B (≡.cong (λ x → RelTo.pt (r x)) (canon-≡ ξ)) }}

    -- choice implies canonical elements
    satisfies-choice⇒canonical-elements : satisfies-choice c c ℓ → canonical-elements
    satisfies-choice⇒canonical-elements sc =
      canon-elts (choose ⟨$⟩_) (λ x → sym (coherent-choice x)) (cong choose)
      where
        open SetoidR A
        D : Setoid c c
        D = setoid ∣ A ∣
        R : SetoidRelation ℓ A D
        R = record
          { _∼_ = _≈_
          ; resp-∼ = λ x₁≈x₂ y₁≈₁y₂ y₁≈x₁ → trans (sym x₁≈x₂) (trans y₁≈x₁ (reflexive y₁≈₁y₂))
          }
        tot : ∀ x → RelTo R x
        tot x = relat x refl
        choice : Choice⇒ A D R tot
        choice = sc D R tot
        open Choice⇒ choice

    canon-Setoid : canonical-elements → Setoid _ _
    canon-Setoid ce = record
      { Carrier = Σ (Carrier × Carrier) λ {(x , y) → canon x ≡ y}
      ; _≈_ = λ x y → snd (fst x) ≡ snd (fst y) -- the canonical elements are identical
      ; isEquivalence = record { refl = ≡.refl ; sym = ≡.sym ; trans = ≡.trans }
      }
      where open canonical-elements ce

    canon-≅ : (ce : canonical-elements) → A ≅ canon-Setoid ce
    canon-≅ ce = record
      { to = record { _⟨$⟩_ = λ x → ((x , canon x) , ≡.refl) ; cong = canon-≡ }
      ; from = record { _⟨$⟩_ = λ { ((x , _), _) → x}  -- the from map 'cheats'.
      ; cong = λ { {(( x₁ , y₁) , eq₁)} {((x₂ , y₂) , eq₂)} eq₃ →
          trans (sym (canon-≈ x₁)) (trans (reflexive eq₁) (trans (reflexive eq₃) (sym (trans (sym (canon-≈ x₂)) (reflexive eq₂)))))} }
      ; inverse-of = record
        { left-inverse-of = λ _ → refl
        ; right-inverse-of = λ { ((x , y) , eq) → eq}
        }
      }
      where
        open canonical-elements ce

  -- here's an example of not-a-set that still have canonical elements
  ℤ-Groupoid : Setoid 0ℓ 0ℓ
  ℤ-Groupoid = record
    { Carrier = ⊤
    ; _≈_ = λ _ _ → ℤ.ℤ
    ; isEquivalence = record { refl = ℤ.+0 ; sym = λ a → ℤ.- a ; trans = ℤ._+_ }
    }

  ℤG-canonical-elements : canonical-elements ℤ-Groupoid
  ℤG-canonical-elements = canon-elts (λ x → x) (λ _ → ℤ.+0) (λ _ → ≡.refl)

  cong-equiv : (eq : A ≅ B) → (x y : ∣ A ∣ ) → Setoid._≈_ A x y FE.⇔ Setoid._≈_ B (FI.Inverse.to eq ⟨$⟩ x) (FI.Inverse.to eq ⟨$⟩ y)
  cong-equiv {A = A} {B} eq x y = record
    { to = record { _⟨$⟩_ = cong to ; cong = λ { ≡.refl → ≡.refl } }
    ; from = record
      { _⟨$⟩_ = λ fx≈fy → let open Setoid A in
        trans (sym (left-inverse-of x)) (trans (cong from fx≈fy) (left-inverse-of y))
      ; cong = λ { ≡.refl → ≡.refl }
      }
    }
    where
      open FI.Inverse eq

  cong-on-Set : {x y : ∣ A ∣ } (is : is-set ∣ A ∣ ) (f : ∣ A ∣ → ∣ B ∣ ) (p q : x ≡ y) → ≡.cong f p ≡ ≡.cong f q
  cong-on-Set {A = A} {x = x} {y} is f p q = begin
    ≡.cong f p ≡⟨ ≡.cong (≡.cong f) (is {x} {y} {p} {q}) ⟩
    ≡.cong f q ∎
    where open ≡.≡-Reasoning

  ≅-pres-Set : (eq : A ≅ B) → is-set ∣ B ∣ → {x y : ∣ A ∣ } → (p q : x ≡ y) → p ≡ q
  ≅-pres-Set eq is {x} {y} p q = begin
    p                  ≡⟨ ≡.sym (≡.cong-id p) ⟩
    ≡.cong (λ x → x) p ≡⟨ {!!} ⟩
    q ∎
    where
      open ≡.≡-Reasoning
      open FI.Inverse eq

  ℤG-¬Set : ¬ (type-like ℤ-Groupoid r)
  ℤG-¬Set tl = {!!}
    where
      open type-like tl
      open FI.Inverse type-like-≅

  -- Corrolary: ℕ satisfies choice
  open import Data.Nat

  ℕ-choice : satisfies-choice (setoid ℕ) c ℓ r
  ℕ-choice =
    canonical-elements⇒satisfies-choice
      (setoid ℕ)
      (type-like⇒canonical-elements (setoid ℕ)
         (record { type-like-to = ℕ
                 ; type-like-≅ = FI.id }))