aly.agda

open import Data.Set.Coequaliser
open import 1Lab.Prelude
open import Data.Bool
open import Data.Fin.Base
open import Data.Vec.Base

module wip.aly where

data Tri : Type where
  zero one two : Tri

Tri-is-set : is-set Tri
Tri-is-set = retract→is-hlevel 2
  (lookup (zero ∷ one ∷ two ∷ []))
  (λ { zero → 0
     ; one  → 1
     ; two  → 2 })
  (λ { zero → refl
     ; one  → refl
     ; two  → refl
     })
  Fin-is-set

abstract instance
  H-Level-Tri : H-Level Tri 2
  H-Level-Tri = hlevel-instance Tri-is-set

data rel : Tri → Tri → Type where
  evens  : rel zero two
  reflᵣ  : ∀ {x} → rel x x
  symᵣ   : ∀ {x y} → rel x y → rel y x
  squash : ∀ x y → is-prop (rel x y)

Two : Type
Two = Tri / rel

sign : Tri → Bool
sign zero = false
sign one  = true
sign two  = false

embed : Bool → Tri
embed true  = one
embed false = zero

f : Tri → Tri
f x = embed (sign x)

f-idempotent : ∀ x → f (f x) ≡ f x
f-idempotent zero = refl
f-idempotent one  = refl
f-idempotent two  = refl

lemma : ∀ {x y} → (f x ≡ f y) ≃ rel x y
lemma = prop-ext (Tri-is-set _ _) (squash _ _) (to _ _) (fro _ _) where
  to : ∀ x y → f x ≡ f y → rel x y
  to zero zero p = reflᵣ
  to zero two  p = evens
  to one  one  p = reflᵣ
  to two  zero p = symᵣ evens
  to two  two  p = reflᵣ
  to zero one  p = absurd $ transport (ap (λ { zero → ⊤ ; _ → ⊥ }) p) tt
  to two  one  p = absurd $ transport (ap (λ { zero → ⊤ ; _ → ⊥ }) p) tt
  to one  two  p = absurd $ transport (ap (λ { one → ⊤ ; _ → ⊥ }) p) tt
  to one  zero p = absurd $ transport (ap (λ { one → ⊤ ; _ → ⊥ }) p) tt

  fro : ∀ x y → rel x y → f x ≡ f y
  fro .zero .two evens = refl
  fro x .x reflᵣ       = refl
  fro x y (symᵣ r)     = sym (fro _ _ r)
  fro x y (squash .x .y p q i) =
    Tri-is-set (f x) (f y) (fro x y p) (fro x y q) i

open is-iso

eqv : Two ≃ (Σ Tri λ x → f x ≡ x)
eqv = Iso→Equiv λ where
  .fst → Coeq-rec hlevel! (λ x → f x , f-idempotent x) λ {
    (_ , _ , r) → Σ-prop-path! (Equiv.from lemma r) }
  .snd .inv  (x , _) → Coeq.inc x
  .snd .rinv (x , p) → Σ-prop-path! p
  .snd .linv → Coeq-elim-prop (λ _ → hlevel 1) λ x →
    glue (_ , _ , Equiv.to lemma (f-idempotent x))

no-go :
  ∀ {ℓa ℓr} {A : Type ℓa}
  → is-set A
  → (R : Congruence A ℓr)
  → (g : Congruence.quotient R → A)
  → is-left-inverse g Coeq.inc
  → ∀ {x y : A} → (x ≡ y) ≃ Congruence.relation R x y
no-go a-set R g linv = thm _ _ where
  emb : is-embedding {B = Congruence.quotient R} Coeq.inc
  emb = injective→is-embedding squash Coeq.inc λ {x} {y} p →
    x         ≡˘⟨ linv x ⟩
    g (inc x) ≡⟨ ap g p ⟩
    g (inc y) ≡⟨ linv y ⟩
    y         ∎

  thm : ∀ x y → (x ≡ y) ≃ Congruence.relation R x y
  thm x y =
    x ≡ y                     ≃⟨ _ , embedding→cancellable emb ⟩
    inc x ≡ inc y             ≃⟨ (_ , effective R) e⁻¹ ⟩
    Congruence.relation R x y ≃∎