```{-# OPTIONS --without-K #-}

open import library.Basics hiding (Type ; Σ)
open import library.types.Sigma
open import library.types.Bool

open import Sec2preliminaries
open import Sec4collapsibility

module Sec6collImplDecEq where

-- Lemma 6.1
coll-family-dec : {X : Type} → (x₁ x₂ : X) → ((x : X) → coll ((x₁ == x) + (x₂ == x))) → (x₁ == x₂) + ¬(x₁ == x₂)
coll-family-dec {X} x₁ x₂ coll-fam = solution where
f₋ : (x : X) → (x₁ == x) + (x₂ == x) → (x₁ == x) + (x₂ == x)
f₋ x = fst (coll-fam x)

E₋ : X → Type
E₋ x = fix (f₋ x)

E : Type
E = Σ X λ x → (E₋ x)

E-fst-determines-eq : (e₁ e₂ : E) → (fst e₁ == fst e₂) → e₁ == e₂
E-fst-determines-eq e₁ e₂ p = second-comp-triv (λ x → fixed-point (f₋ x) (snd (coll-fam x))) _ _ p

r : Bool → E
r true = x₁ , to-fix (f₋ x₁) (snd (coll-fam x₁)) (inl idp)
r false = x₂ , to-fix (f₋ x₂) (snd (coll-fam x₂)) (inr idp)

about-r : (r true == r false) ↔ (x₁ == x₂)
about-r = (λ p → ap fst p) , (λ p → E-fst-determines-eq _ _ p)

s : E → Bool
s (_ , inl _ , _) = true
s (_ , inr _ , _) = false

s-section-of-r : (e : E) → r(s e) == e
s-section-of-r (x , inl p , q) = E-fst-determines-eq _ _ p
s-section-of-r (x , inr p , q) = E-fst-determines-eq _ _ p

about-s : (e₁ e₂ : E) → (s e₁ == s e₂) ↔ (e₁ == e₂)
about-s e₁ e₂ = one , two where
one : (s e₁ == s e₂) → (e₁ == e₂)
one p =
e₁       =⟨ ! (s-section-of-r e₁) ⟩
r(s(e₁)) =⟨ ap r p ⟩
r(s(e₂)) =⟨ s-section-of-r e₂ ⟩
e₂       ∎
two : (e₁ == e₂) → (s e₁ == s e₂)
two p = ap s p

combine : (s (r true) == s (r false)) ↔ (x₁ == x₂)
combine = (about-s _ _) ◎ about-r

check-bool : (s (r true) == s (r false)) + ¬(s (r true) == s (r false))
check-bool = Bool-has-dec-eq _ _

solution : (x₁ == x₂) + ¬(x₁ == x₂)
solution with check-bool
solution | inl p = inl (fst combine p)
solution | inr np = inr (λ p → np (snd combine p))

-- Theorem 6.2
all-coll→dec-eq : ((X : Type) → coll X) → (X : Type) → has-dec-eq X
all-coll→dec-eq all-coll X x₁ x₂ = coll-family-dec x₁ x₂ (λ x → all-coll _)
```