-- We define ZigZag-complete relations and prove that quasi equivalence relations -- give rise to equivalences on the set quotients. {-# OPTIONS --cubical --no-import-sorts --safe #-} module Cubical.Relation.ZigZag.Base where open import Cubical.Core.Everything open import Cubical.Foundations.Prelude open import Cubical.Foundations.Function open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.HLevels open import Cubical.Data.Sigma open import Cubical.HITs.SetQuotients open import Cubical.HITs.PropositionalTruncation as Trunc open import Cubical.Relation.Binary.Base open BinaryRelation open isEquivRel private variable ℓ ℓ' : Level isZigZagComplete : {A B : Type ℓ} (R : A → B → Type ℓ') → Type (ℓ-max ℓ ℓ') isZigZagComplete R = ∀ {a b a' b'} → R a b → R a' b → R a' b' → R a b' ZigZagRel : (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ')) ZigZagRel A B ℓ' = Σ[ R ∈ (A → B → Type ℓ') ] (isZigZagComplete R) record isQuasiEquivRel {A B : Type ℓ} (R : A → B → Type ℓ') : Type (ℓ-max ℓ ℓ') where field zigzag : isZigZagComplete R fwd : (a : A) → ∃[ b ∈ B ] R a b bwd : (b : B) → ∃[ a ∈ A ] R a b open isQuasiEquivRel QuasiEquivRel : (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ')) QuasiEquivRel A B ℓ' = Σ[ R ∈ PropRel A B ℓ' ] isQuasiEquivRel (R .fst) invQER : {A B : Type ℓ} {ℓ' : Level} → QuasiEquivRel A B ℓ' → QuasiEquivRel B A ℓ' invQER (R , qer) .fst = invPropRel R invQER (R , qer) .snd .zigzag aRb aRb' a'Rb' = qer .zigzag a'Rb' aRb' aRb invQER (R , qer) .snd .fwd = qer .bwd invQER (R , qer) .snd .bwd = qer .fwd QER→EquivRel : {A B : Type ℓ} → QuasiEquivRel A B ℓ' → EquivPropRel A (ℓ-max ℓ ℓ') QER→EquivRel (R , sim) .fst = compPropRel R (invPropRel R) QER→EquivRel (R , sim) .snd .reflexive a = Trunc.map (λ {(b , r) → b , r , r}) (sim .fwd a) QER→EquivRel (R , sim) .snd .symmetric _ _ = Trunc.map (λ {(b , r₀ , r₁) → b , r₁ , r₀}) QER→EquivRel (R , sim) .snd .transitive _ _ _ = Trunc.map2 (λ {(b , r₀ , r₁) (b' , r₀' , r₁') → b , r₀ , sim .zigzag r₁' r₀' r₁}) -- The following result is due to Carlo Angiuli module QER→Equiv {A B : Type ℓ} (R : QuasiEquivRel A B ℓ') where Rᴸ = QER→EquivRel R .fst .fst Rᴿ = QER→EquivRel (invQER R) .fst .fst private sim = R .snd private f : (a : A) → ∃[ b ∈ B ] R .fst .fst a b → B / Rᴿ f a = Trunc.rec→Set squash/ ([_] ∘ fst) (λ {(b , r) (b' , r') → eq/ b b' ∣ a , r , r' ∣}) fPath : (a₀ : A) (s₀ : ∃[ b ∈ B ] R .fst .fst a₀ b) (a₁ : A) (s₁ : ∃[ b ∈ B ] R .fst .fst a₁ b) → Rᴸ a₀ a₁ → f a₀ s₀ ≡ f a₁ s₁ fPath a₀ = Trunc.elim (λ _ → isPropΠ3 λ _ _ _ → squash/ _ _) (λ {(b₀ , r₀) a₁ → Trunc.elim (λ _ → isPropΠ λ _ → squash/ _ _) (λ {(b₁ , r₁) → Trunc.elim (λ _ → squash/ _ _) (λ {(b' , r₀' , r₁') → eq/ b₀ b₁ ∣ a₀ , r₀ , sim .zigzag r₀' r₁' r₁ ∣})})}) φ : A / Rᴸ → B / Rᴿ φ [ a ] = f a (sim .fwd a) φ (eq/ a₀ a₁ r i) = fPath a₀ (sim .fwd a₀) a₁ (sim .fwd a₁) r i φ (squash/ _ _ p q j i) = squash/ _ _ (cong φ p) (cong φ q) j i relToFwd≡ : ∀ {a b} → R .fst .fst a b → φ [ a ] ≡ [ b ] relToFwd≡ {a} {b} r = Trunc.elim {P = λ s → f a s ≡ [ b ]} (λ _ → squash/ _ _) (λ {(b' , r') → eq/ b' b ∣ a , r' , r ∣}) (sim .fwd a) fwd≡ToRel : ∀ {a b} → φ [ a ] ≡ [ b ] → R .fst .fst a b fwd≡ToRel {a} {b} = Trunc.elim {P = λ s → f a s ≡ [ b ] → R .fst .fst a b} (λ _ → isPropΠ λ _ → R .fst .snd _ _) (λ {(b' , r') p → Trunc.rec (R .fst .snd _ _) (λ {(a' , s' , s) → R .snd .zigzag r' s' s}) (effective (QER→EquivRel (invQER R) .fst .snd) (QER→EquivRel (invQER R) .snd) b' b p)}) (sim .fwd a) private g : (b : B) → ∃[ a ∈ A ] R .fst .fst a b → A / Rᴸ g b = Trunc.rec→Set squash/ ([_] ∘ fst) (λ {(a , r) (a' , r') → eq/ a a' ∣ b , r , r' ∣}) gPath : (b₀ : B) (s₀ : ∃[ a ∈ A ] R .fst .fst a b₀) (b₁ : B) (s₁ : ∃[ a ∈ A ] R .fst .fst a b₁) → Rᴿ b₀ b₁ → g b₀ s₀ ≡ g b₁ s₁ gPath b₀ = Trunc.elim (λ _ → isPropΠ3 λ _ _ _ → squash/ _ _) (λ {(a₀ , r₀) b₁ → Trunc.elim (λ _ → isPropΠ λ _ → squash/ _ _) (λ {(a₁ , r₁) → Trunc.elim (λ _ → squash/ _ _) (λ {(a' , r₀' , r₁') → eq/ a₀ a₁ ∣ b₀ , r₀ , sim .zigzag r₁ r₁' r₀' ∣})})}) ψ : B / Rᴿ → A / Rᴸ ψ [ b ] = g b (sim .bwd b) ψ (eq/ b₀ b₁ r i) = gPath b₀ (sim .bwd b₀) b₁ (sim .bwd b₁) r i ψ (squash/ _ _ p q j i) = squash/ _ _ (cong ψ p) (cong ψ q) j i relToBwd≡ : ∀ {a b} → R .fst .fst a b → ψ [ b ] ≡ [ a ] relToBwd≡ {a} {b} r = Trunc.elim {P = λ s → g b s ≡ [ a ]} (λ _ → squash/ _ _) (λ {(a' , r') → eq/ a' a ∣ b , r' , r ∣}) (sim .bwd b) private η : ∀ qb → φ (ψ qb) ≡ qb η = elimProp (λ _ → squash/ _ _) (λ b → Trunc.elim {P = λ s → φ (g b s) ≡ [ b ]} (λ _ → squash/ _ _) (λ {(a , r) → relToFwd≡ r}) (sim .bwd b)) ε : ∀ qa → ψ (φ qa) ≡ qa ε = elimProp (λ _ → squash/ _ _) (λ a → Trunc.elim {P = λ s → ψ (f a s) ≡ [ a ]} (λ _ → squash/ _ _) (λ {(b , r) → relToBwd≡ r}) (sim .fwd a)) bwd≡ToRel : ∀ {a b} → ψ [ b ] ≡ [ a ] → R .fst .fst a b bwd≡ToRel {a} {b} p = fwd≡ToRel (cong φ (sym p) ∙ η [ b ]) Thm : (A / Rᴸ) ≃ (B / Rᴿ) Thm = isoToEquiv (iso φ ψ η ε)