From 279b29b28f077429d19aeac487f5de4958c4be33 Mon Sep 17 00:00:00 2001 From: hejohns Date: Mon, 29 May 2023 15:16:04 -0400 Subject: [PATCH 1/5] init construction of rezk completion by higher inductive types, as in HOTT book --- .../RezkCompletion/Constructionn.agda | 93 +++++++++++++++++++ 1 file changed, 93 insertions(+) create mode 100644 Cubical/Categories/RezkCompletion/Constructionn.agda diff --git a/Cubical/Categories/RezkCompletion/Constructionn.agda b/Cubical/Categories/RezkCompletion/Constructionn.agda new file mode 100644 index 00000000..96e9ecdc --- /dev/null +++ b/Cubical/Categories/RezkCompletion/Constructionn.agda @@ -0,0 +1,93 @@ +{- + +The Construction of Rezk Completion + +-} +{-# OPTIONS --safe --lossy-unification #-} + +module Cubical.Categories.RezkCompletion.Constructionn where + +open import Cubical.Foundations.Prelude + +open import Cubical.Categories.Category +open import Cubical.Categories.Functor +open import Cubical.Categories.Equivalence.WeakEquivalence +open import Cubical.Categories.Constructions.EssentialImage +open import Cubical.Categories.Presheaf.Base +open import Cubical.Categories.Yoneda + +open import Cubical.Categories.RezkCompletion.Base + +private + variable + ℓ ℓ' : Level + +open isWeakEquivalence + + +-- There are two different ways to construct the Rezk completion, +-- one is using the essential image of the Yoneda embbeding, +-- another one is using a higher inductive type +-- (c.f. HoTT Book Chaper 9.9). + +-- Yoneda embbeding can give a very simple and quick construction. +-- Unfortunately, this construction increases the universe level. + +-- The HIT construction, on the other hand, keeps the universe level, +-- but its proof is a bit long and tedious, still easy though. + + +{- The Construction by Yoneda Embedding -} + +module RezkByYoneda (C : Category ℓ ℓ) where + + YonedaImage : Category (ℓ-suc ℓ) ℓ + YonedaImage = EssentialImage (YO {C = C}) + + isUnivalentYonedaImage : isUnivalent YonedaImage + isUnivalentYonedaImage = isUnivalentEssentialImage _ isUnivalentPresheafCategory + + ToYonedaImage : Functor C YonedaImage + ToYonedaImage = ToEssentialImage _ + + isWeakEquivalenceToYonedaImage : isWeakEquivalence ToYonedaImage + isWeakEquivalenceToYonedaImage .fullfaith = isFullyFaithfulToEssentialImage _ isFullyFaithfulYO + isWeakEquivalenceToYonedaImage .esssurj = isEssentiallySurjToEssentialImage YO + + isRezkCompletionToYonedaImage : isRezkCompletion ToYonedaImage + isRezkCompletionToYonedaImage = makeIsRezkCompletion isUnivalentYonedaImage isWeakEquivalenceToYonedaImage + + +{- The Construction by Higher Inductive Type -} + +module RezkByHIT (C : Category ℓ ℓ') where + open import Cubical.Categories.Category + open Cubical.Categories.Category.Category + open import Cubical.Categories.Isomorphism + -- TODO: Write the HIT construction of Rezk completion here. + data Ĉ₀ : Type (ℓ-max ℓ ℓ') where -- TODO: is this the best we can do w/ the levels? + i : (C .ob) → Ĉ₀ + j : {a b : C .ob}(e : CatIso C a b) → i a ≡ i b + jid : {a : C .ob} → j {a} idCatIso ≡ refl + jcomp : {a b c : C .ob}(f : CatIso C a b)(g : CatIso C b c) → j (⋆Iso f g) ≡ j f ∙ j g + 1-truncation : (x y : Ĉ₀)(p q : x ≡ y)(r s : p ≡ q) → r ≡ s + + -- the paragraph directly following the HIT definition, below theorem 9.9.5 of the HOTT book + notethatfor : (a b : C .ob)(p : a ≡ b) → j (pathToIso p) ≡ congS i p + notethatfor a b p = J (λ y → λ eq → j (pathToIso eq) ≡ congS i eq) (j (pathToIso refl) ≡⟨ congS j pathToIso-refl ⟩ j idCatIso ≡⟨ jid ⟩ congS i refl ∎) p -- TODO: I don't really get this proof and why we want this theorem + + open import Cubical.Foundations.Isomorphism + open import Cubical.Categories.Category.Base + open Cubical.Categories.Category.isIso + Ĉ₁ : Ĉ₀ → Ĉ₀ → Type _ + Ĉ₁ (i a) (i b) = (C [ a , b ]) + Ĉ₁ (i a) (j {b} {b'} e i') = isoToPath (iso iso→ iso⁻¹← (λ g → g ⋆⟨ C ⟩ e⁻¹← ⋆⟨ C ⟩ e→ ≡⟨ C .⋆Assoc g e⁻¹← e→ ⟩ g ⋆⟨ C ⟩ (e⁻¹← ⋆⟨ C ⟩ e→) ≡⟨ congS (λ eq → g ⋆⟨ C ⟩ eq) (e .snd .sec) ⟩ g ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR g ⟩ g ∎) (λ f → f ⋆⟨ C ⟩ e→ ⋆⟨ C ⟩ e⁻¹← ≡⟨ C .⋆Assoc f e→ e⁻¹← ⟩ f ⋆⟨ C ⟩ (e→ ⋆⟨ C ⟩ e⁻¹←) ≡⟨ congS (λ eq → f ⋆⟨ C ⟩ eq) (e .snd .ret) ⟩ f ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR f ⟩ f ∎ )) i' + where + e→ = e .fst + e⁻¹← = e .snd .inv + -- let f ∈ C [ a , b ], g ∈ C [ a , b' ] + -- explicit types to manually supply contraints + iso→ : C [ a , b ] → C [ a , b' ] + iso→ f = f ⋆⟨ C ⟩ e→ + iso⁻¹← : C [ a , b' ] → C [ a , b ] + iso⁻¹← g = g ⋆⟨ C ⟩ e⁻¹← From 2821a3b80b5d4341561f50a8de51844c681218c0 Mon Sep 17 00:00:00 2001 From: hejohns Date: Thu, 1 Jun 2023 12:34:07 -0400 Subject: [PATCH 2/5] I'm stuck trying to show two paths are (prop) equal --- .../RezkCompletion/Constructionn.agda | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/Cubical/Categories/RezkCompletion/Constructionn.agda b/Cubical/Categories/RezkCompletion/Constructionn.agda index 96e9ecdc..ec1c0255 100644 --- a/Cubical/Categories/RezkCompletion/Constructionn.agda +++ b/Cubical/Categories/RezkCompletion/Constructionn.agda @@ -73,15 +73,16 @@ module RezkByHIT (C : Category ℓ ℓ') where 1-truncation : (x y : Ĉ₀)(p q : x ≡ y)(r s : p ≡ q) → r ≡ s -- the paragraph directly following the HIT definition, below theorem 9.9.5 of the HOTT book - notethatfor : (a b : C .ob)(p : a ≡ b) → j (pathToIso p) ≡ congS i p - notethatfor a b p = J (λ y → λ eq → j (pathToIso eq) ≡ congS i eq) (j (pathToIso refl) ≡⟨ congS j pathToIso-refl ⟩ j idCatIso ≡⟨ jid ⟩ congS i refl ∎) p -- TODO: I don't really get this proof and why we want this theorem + _ : (a b : C .ob)(p : a ≡ b) → j (pathToIso p) ≡ congS i p + _ = λ a b p → J (λ y → λ eq → j (pathToIso eq) ≡ congS i eq) (j (pathToIso refl) ≡⟨ congS j pathToIso-refl ⟩ j idCatIso ≡⟨ jid ⟩ congS i refl ∎) p -- TODO: I don't really get this proof and why we want this theorem open import Cubical.Foundations.Isomorphism open import Cubical.Categories.Category.Base open Cubical.Categories.Category.isIso + open import Cubical.Foundations.Univalence Ĉ₁ : Ĉ₀ → Ĉ₀ → Type _ Ĉ₁ (i a) (i b) = (C [ a , b ]) - Ĉ₁ (i a) (j {b} {b'} e i') = isoToPath (iso iso→ iso⁻¹← (λ g → g ⋆⟨ C ⟩ e⁻¹← ⋆⟨ C ⟩ e→ ≡⟨ C .⋆Assoc g e⁻¹← e→ ⟩ g ⋆⟨ C ⟩ (e⁻¹← ⋆⟨ C ⟩ e→) ≡⟨ congS (λ eq → g ⋆⟨ C ⟩ eq) (e .snd .sec) ⟩ g ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR g ⟩ g ∎) (λ f → f ⋆⟨ C ⟩ e→ ⋆⟨ C ⟩ e⁻¹← ≡⟨ C .⋆Assoc f e→ e⁻¹← ⟩ f ⋆⟨ C ⟩ (e→ ⋆⟨ C ⟩ e⁻¹←) ≡⟨ congS (λ eq → f ⋆⟨ C ⟩ eq) (e .snd .ret) ⟩ f ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR f ⟩ f ∎ )) i' + Ĉ₁ (i a) (j {b} {b'} e i') = isoToPath (iso iso→ iso⁻¹← (λ g → iso→ (iso⁻¹← g) ≡⟨ refl ⟩ g ⋆⟨ C ⟩ e⁻¹← ⋆⟨ C ⟩ e→ ≡⟨ C .⋆Assoc g e⁻¹← e→ ⟩ g ⋆⟨ C ⟩ (e⁻¹← ⋆⟨ C ⟩ e→) ≡⟨ congS (λ eq → g ⋆⟨ C ⟩ eq) (e .snd .sec) ⟩ g ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR g ⟩ g ∎) (λ f → iso⁻¹← (iso→ f) ≡⟨ refl ⟩ f ⋆⟨ C ⟩ e→ ⋆⟨ C ⟩ e⁻¹← ≡⟨ C .⋆Assoc f e→ e⁻¹← ⟩ f ⋆⟨ C ⟩ (e→ ⋆⟨ C ⟩ e⁻¹←) ≡⟨ congS (λ eq → f ⋆⟨ C ⟩ eq) (e .snd .ret) ⟩ f ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR f ⟩ f ∎ )) i' where e→ = e .fst e⁻¹← = e .snd .inv @@ -91,3 +92,13 @@ module RezkByHIT (C : Category ℓ ℓ') where iso→ f = f ⋆⟨ C ⟩ e→ iso⁻¹← : C [ a , b' ] → C [ a , b ] iso⁻¹← g = g ⋆⟨ C ⟩ e⁻¹← + Ĉ₁ (i a) (jid {b} i' i'') = ((isoToPath (iso iso→ iso⁻¹← (λ g → iso→ (iso⁻¹← g) ≡⟨ refl ⟩ g ⋆⟨ C ⟩ C .id ⋆⟨ C ⟩ C .id ≡⟨ C .⋆Assoc g (C .id) (C .id) ⟩ g ⋆⟨ C ⟩ (C .id ⋆⟨ C ⟩ C .id) ≡⟨ congS (λ eq → g ⋆⟨ C ⟩ eq) (C .⋆IdL (C .id)) ⟩ g ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR g ⟩ g ∎ ) (λ f → iso⁻¹← (iso→ f) ≡⟨ refl ⟩ f ⋆⟨ C ⟩ C .id ⋆⟨ C ⟩ C .id ≡⟨ C .⋆Assoc f (C .id) (C .id) ⟩ f ⋆⟨ C ⟩ (C .id ⋆⟨ C ⟩ C .id) ≡⟨ congS (λ eq → f ⋆⟨ C ⟩ eq) (C .⋆IdL (C .id)) ⟩ f ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR f ⟩ f ∎))) ≡⟨ {!!} ⟩ refl-hom ∎) i' i'' + where + iso→ : C [ a , b ] → C [ a , b ] + iso→ f = f ⋆⟨ C ⟩ (C .id) + iso⁻¹← : C [ a , b ] → C [ a , b ] + iso⁻¹← g = g ⋆⟨ C ⟩ (C .id) + refl-hom : C [ a , b ] ≡ C [ a , b ] + refl-hom = refl + Ĉ₁ (i a) (jcomp {b} {c} {d} f g i' i'') = {!!} + Ĉ₁ (j {a} {a'} e i') (i b) = {!!} From 2e76ef6971a9738d711c78c6922d0c8626b5f566 Mon Sep 17 00:00:00 2001 From: hejohns Date: Thu, 1 Jun 2023 16:03:35 -0400 Subject: [PATCH 3/5] yeah this is stuck. I'll come back when I understand actual HoTT better --- Cubical/Categories/RezkCompletion/Constructionn.agda | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Cubical/Categories/RezkCompletion/Constructionn.agda b/Cubical/Categories/RezkCompletion/Constructionn.agda index ec1c0255..1a531d5d 100644 --- a/Cubical/Categories/RezkCompletion/Constructionn.agda +++ b/Cubical/Categories/RezkCompletion/Constructionn.agda @@ -79,7 +79,6 @@ module RezkByHIT (C : Category ℓ ℓ') where open import Cubical.Foundations.Isomorphism open import Cubical.Categories.Category.Base open Cubical.Categories.Category.isIso - open import Cubical.Foundations.Univalence Ĉ₁ : Ĉ₀ → Ĉ₀ → Type _ Ĉ₁ (i a) (i b) = (C [ a , b ]) Ĉ₁ (i a) (j {b} {b'} e i') = isoToPath (iso iso→ iso⁻¹← (λ g → iso→ (iso⁻¹← g) ≡⟨ refl ⟩ g ⋆⟨ C ⟩ e⁻¹← ⋆⟨ C ⟩ e→ ≡⟨ C .⋆Assoc g e⁻¹← e→ ⟩ g ⋆⟨ C ⟩ (e⁻¹← ⋆⟨ C ⟩ e→) ≡⟨ congS (λ eq → g ⋆⟨ C ⟩ eq) (e .snd .sec) ⟩ g ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR g ⟩ g ∎) (λ f → iso⁻¹← (iso→ f) ≡⟨ refl ⟩ f ⋆⟨ C ⟩ e→ ⋆⟨ C ⟩ e⁻¹← ≡⟨ C .⋆Assoc f e→ e⁻¹← ⟩ f ⋆⟨ C ⟩ (e→ ⋆⟨ C ⟩ e⁻¹←) ≡⟨ congS (λ eq → f ⋆⟨ C ⟩ eq) (e .snd .ret) ⟩ f ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR f ⟩ f ∎ )) i' @@ -92,12 +91,14 @@ module RezkByHIT (C : Category ℓ ℓ') where iso→ f = f ⋆⟨ C ⟩ e→ iso⁻¹← : C [ a , b' ] → C [ a , b ] iso⁻¹← g = g ⋆⟨ C ⟩ e⁻¹← - Ĉ₁ (i a) (jid {b} i' i'') = ((isoToPath (iso iso→ iso⁻¹← (λ g → iso→ (iso⁻¹← g) ≡⟨ refl ⟩ g ⋆⟨ C ⟩ C .id ⋆⟨ C ⟩ C .id ≡⟨ C .⋆Assoc g (C .id) (C .id) ⟩ g ⋆⟨ C ⟩ (C .id ⋆⟨ C ⟩ C .id) ≡⟨ congS (λ eq → g ⋆⟨ C ⟩ eq) (C .⋆IdL (C .id)) ⟩ g ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR g ⟩ g ∎ ) (λ f → iso⁻¹← (iso→ f) ≡⟨ refl ⟩ f ⋆⟨ C ⟩ C .id ⋆⟨ C ⟩ C .id ≡⟨ C .⋆Assoc f (C .id) (C .id) ⟩ f ⋆⟨ C ⟩ (C .id ⋆⟨ C ⟩ C .id) ≡⟨ congS (λ eq → f ⋆⟨ C ⟩ eq) (C .⋆IdL (C .id)) ⟩ f ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR f ⟩ f ∎))) ≡⟨ {!!} ⟩ refl-hom ∎) i' i'' + Ĉ₁ (i a) (jid {b} i' i'') = ( proof⋆id ≡⟨ J (λ y eq → {! !}) {!!} proof⋆id ⟩ refl-hom ∎) i' i'' where iso→ : C [ a , b ] → C [ a , b ] iso→ f = f ⋆⟨ C ⟩ (C .id) iso⁻¹← : C [ a , b ] → C [ a , b ] iso⁻¹← g = g ⋆⟨ C ⟩ (C .id) + proof⋆id : C [ a , b ] ≡ C [ a , b ] + proof⋆id = isoToPath (iso iso→ iso⁻¹← (λ g → iso→ (iso⁻¹← g) ≡⟨ refl ⟩ g ⋆⟨ C ⟩ C .id ⋆⟨ C ⟩ C .id ≡⟨ C .⋆Assoc g (C .id) (C .id) ⟩ g ⋆⟨ C ⟩ (C .id ⋆⟨ C ⟩ C .id) ≡⟨ congS (λ eq → g ⋆⟨ C ⟩ eq) (C .⋆IdL (C .id)) ⟩ g ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR g ⟩ g ∎ ) (λ f → iso⁻¹← (iso→ f) ≡⟨ refl ⟩ f ⋆⟨ C ⟩ C .id ⋆⟨ C ⟩ C .id ≡⟨ C .⋆Assoc f (C .id) (C .id) ⟩ f ⋆⟨ C ⟩ (C .id ⋆⟨ C ⟩ C .id) ≡⟨ congS (λ eq → f ⋆⟨ C ⟩ eq) (C .⋆IdL (C .id)) ⟩ f ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR f ⟩ f ∎)) refl-hom : C [ a , b ] ≡ C [ a , b ] refl-hom = refl Ĉ₁ (i a) (jcomp {b} {c} {d} f g i' i'') = {!!} From 343d6dc25a04bfb55000040744c2a0a97b90e685 Mon Sep 17 00:00:00 2001 From: hejohns Date: Mon, 5 Jun 2023 16:38:36 -0400 Subject: [PATCH 4/5] resolved the isoToPath issue (see prev commit). From eric's suggestion Friday evening --- .../Categories/RezkCompletion/Constructionn.agda | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/Cubical/Categories/RezkCompletion/Constructionn.agda b/Cubical/Categories/RezkCompletion/Constructionn.agda index 1a531d5d..0bd44c07 100644 --- a/Cubical/Categories/RezkCompletion/Constructionn.agda +++ b/Cubical/Categories/RezkCompletion/Constructionn.agda @@ -79,9 +79,12 @@ module RezkByHIT (C : Category ℓ ℓ') where open import Cubical.Foundations.Isomorphism open import Cubical.Categories.Category.Base open Cubical.Categories.Category.isIso + open import Cubical.Foundations.Univalence + open import Cubical.Foundations.Equiv Ĉ₁ : Ĉ₀ → Ĉ₀ → Type _ Ĉ₁ (i a) (i b) = (C [ a , b ]) - Ĉ₁ (i a) (j {b} {b'} e i') = isoToPath (iso iso→ iso⁻¹← (λ g → iso→ (iso⁻¹← g) ≡⟨ refl ⟩ g ⋆⟨ C ⟩ e⁻¹← ⋆⟨ C ⟩ e→ ≡⟨ C .⋆Assoc g e⁻¹← e→ ⟩ g ⋆⟨ C ⟩ (e⁻¹← ⋆⟨ C ⟩ e→) ≡⟨ congS (λ eq → g ⋆⟨ C ⟩ eq) (e .snd .sec) ⟩ g ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR g ⟩ g ∎) (λ f → iso⁻¹← (iso→ f) ≡⟨ refl ⟩ f ⋆⟨ C ⟩ e→ ⋆⟨ C ⟩ e⁻¹← ≡⟨ C .⋆Assoc f e→ e⁻¹← ⟩ f ⋆⟨ C ⟩ (e→ ⋆⟨ C ⟩ e⁻¹←) ≡⟨ congS (λ eq → f ⋆⟨ C ⟩ eq) (e .snd .ret) ⟩ f ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR f ⟩ f ∎ )) i' + Ĉ₁ (i a) (j {b} {b'} e i') = ua (isoToEquiv (iso iso→ iso⁻¹← (λ g → iso→ (iso⁻¹← g) ≡⟨ refl ⟩ g ⋆⟨ C ⟩ e⁻¹← ⋆⟨ C ⟩ e→ ≡⟨ C .⋆Assoc g e⁻¹← e→ ⟩ g ⋆⟨ C ⟩ (e⁻¹← ⋆⟨ C ⟩ e→) ≡⟨ congS (λ eq → g ⋆⟨ C ⟩ eq) (e .snd .sec) ⟩ g ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR g ⟩ g ∎) (λ f → iso⁻¹← (iso→ f) ≡⟨ refl ⟩ f ⋆⟨ C ⟩ e→ ⋆⟨ C ⟩ e⁻¹← ≡⟨ C .⋆Assoc f e→ e⁻¹← ⟩ f ⋆⟨ C ⟩ (e→ ⋆⟨ C ⟩ e⁻¹←) ≡⟨ congS (λ eq → f ⋆⟨ C ⟩ eq) (e .snd .ret) ⟩ f ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR f ⟩ f ∎ ))) i' + -- isoToPath (iso iso→ iso⁻¹← (λ g → iso→ (iso⁻¹← g) ≡⟨ refl ⟩ g ⋆⟨ C ⟩ e⁻¹← ⋆⟨ C ⟩ e→ ≡⟨ C .⋆Assoc g e⁻¹← e→ ⟩ g ⋆⟨ C ⟩ (e⁻¹← ⋆⟨ C ⟩ e→) ≡⟨ congS (λ eq → g ⋆⟨ C ⟩ eq) (e .snd .sec) ⟩ g ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR g ⟩ g ∎) (λ f → iso⁻¹← (iso→ f) ≡⟨ refl ⟩ f ⋆⟨ C ⟩ e→ ⋆⟨ C ⟩ e⁻¹← ≡⟨ C .⋆Assoc f e→ e⁻¹← ⟩ f ⋆⟨ C ⟩ (e→ ⋆⟨ C ⟩ e⁻¹←) ≡⟨ congS (λ eq → f ⋆⟨ C ⟩ eq) (e .snd .ret) ⟩ f ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR f ⟩ f ∎ )) i' where e→ = e .fst e⁻¹← = e .snd .inv @@ -91,15 +94,15 @@ module RezkByHIT (C : Category ℓ ℓ') where iso→ f = f ⋆⟨ C ⟩ e→ iso⁻¹← : C [ a , b' ] → C [ a , b ] iso⁻¹← g = g ⋆⟨ C ⟩ e⁻¹← - Ĉ₁ (i a) (jid {b} i' i'') = ( proof⋆id ≡⟨ J (λ y eq → {! !}) {!!} proof⋆id ⟩ refl-hom ∎) i' i'' + Ĉ₁ (i a) (jid {b} i' i'') = ( proof⋆id ≡⟨ congS ua (equivEq (funExt λ f → C .⋆IdR f)) ⟩ ua (idEquiv (C [ a , b ])) ≡⟨ uaIdEquiv ⟩ refl-hom ∎) i' i'' where iso→ : C [ a , b ] → C [ a , b ] iso→ f = f ⋆⟨ C ⟩ (C .id) iso⁻¹← : C [ a , b ] → C [ a , b ] iso⁻¹← g = g ⋆⟨ C ⟩ (C .id) proof⋆id : C [ a , b ] ≡ C [ a , b ] - proof⋆id = isoToPath (iso iso→ iso⁻¹← (λ g → iso→ (iso⁻¹← g) ≡⟨ refl ⟩ g ⋆⟨ C ⟩ C .id ⋆⟨ C ⟩ C .id ≡⟨ C .⋆Assoc g (C .id) (C .id) ⟩ g ⋆⟨ C ⟩ (C .id ⋆⟨ C ⟩ C .id) ≡⟨ congS (λ eq → g ⋆⟨ C ⟩ eq) (C .⋆IdL (C .id)) ⟩ g ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR g ⟩ g ∎ ) (λ f → iso⁻¹← (iso→ f) ≡⟨ refl ⟩ f ⋆⟨ C ⟩ C .id ⋆⟨ C ⟩ C .id ≡⟨ C .⋆Assoc f (C .id) (C .id) ⟩ f ⋆⟨ C ⟩ (C .id ⋆⟨ C ⟩ C .id) ≡⟨ congS (λ eq → f ⋆⟨ C ⟩ eq) (C .⋆IdL (C .id)) ⟩ f ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR f ⟩ f ∎)) + proof⋆id = ua (isoToEquiv (iso iso→ iso⁻¹← (λ g → iso→ (iso⁻¹← g) ≡⟨ refl ⟩ g ⋆⟨ C ⟩ C .id ⋆⟨ C ⟩ C .id ≡⟨ C .⋆Assoc g (C .id) (C .id) ⟩ g ⋆⟨ C ⟩ (C .id ⋆⟨ C ⟩ C .id) ≡⟨ congS (λ eq → g ⋆⟨ C ⟩ eq) (C .⋆IdL (C .id)) ⟩ g ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR g ⟩ g ∎ ) (λ f → iso⁻¹← (iso→ f) ≡⟨ refl ⟩ f ⋆⟨ C ⟩ C .id ⋆⟨ C ⟩ C .id ≡⟨ C .⋆Assoc f (C .id) (C .id) ⟩ f ⋆⟨ C ⟩ (C .id ⋆⟨ C ⟩ C .id) ≡⟨ congS (λ eq → f ⋆⟨ C ⟩ eq) (C .⋆IdL (C .id)) ⟩ f ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR f ⟩ f ∎))) refl-hom : C [ a , b ] ≡ C [ a , b ] refl-hom = refl - Ĉ₁ (i a) (jcomp {b} {c} {d} f g i' i'') = {!!} - Ĉ₁ (j {a} {a'} e i') (i b) = {!!} + --Ĉ₁ (i a) (jcomp {b} {c} {d} f g i' i'') = {!!} + --Ĉ₁ (j {a} {a'} e i') (i b) = {!!} From 619991233477c6962cc88015fd39ab9348dbe555 Mon Sep 17 00:00:00 2001 From: Max New Date: Fri, 16 Feb 2024 09:46:52 -0500 Subject: [PATCH 5/5] define an eliminator for the Rezk completion --- .../RezkCompletion/Constructionn.agda | 137 +++++++++++++----- 1 file changed, 98 insertions(+), 39 deletions(-) diff --git a/Cubical/Categories/RezkCompletion/Constructionn.agda b/Cubical/Categories/RezkCompletion/Constructionn.agda index 0bd44c07..c9431e1e 100644 --- a/Cubical/Categories/RezkCompletion/Constructionn.agda +++ b/Cubical/Categories/RezkCompletion/Constructionn.agda @@ -1,6 +1,6 @@ {- -The Construction of Rezk Completion +The Constructionn (sic) of Rezk Completion -} {-# OPTIONS --safe --lossy-unification #-} @@ -8,8 +8,13 @@ The Construction of Rezk Completion module Cubical.Categories.RezkCompletion.Constructionn where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels + +open import Cubical.Data.Sigma open import Cubical.Categories.Category +open import Cubical.Categories.Isomorphism +open import Cubical.Categories.Instances.Sets open import Cubical.Categories.Functor open import Cubical.Categories.Equivalence.WeakEquivalence open import Cubical.Categories.Constructions.EssentialImage @@ -20,7 +25,7 @@ open import Cubical.Categories.RezkCompletion.Base private variable - ℓ ℓ' : Level + ℓ ℓ' ℓ'' : Level open isWeakEquivalence @@ -61,48 +66,102 @@ module RezkByYoneda (C : Category ℓ ℓ) where {- The Construction by Higher Inductive Type -} module RezkByHIT (C : Category ℓ ℓ') where - open import Cubical.Categories.Category - open Cubical.Categories.Category.Category - open import Cubical.Categories.Isomorphism + module C = Category C -- TODO: Write the HIT construction of Rezk completion here. data Ĉ₀ : Type (ℓ-max ℓ ℓ') where -- TODO: is this the best we can do w/ the levels? - i : (C .ob) → Ĉ₀ - j : {a b : C .ob}(e : CatIso C a b) → i a ≡ i b - jid : {a : C .ob} → j {a} idCatIso ≡ refl - jcomp : {a b c : C .ob}(f : CatIso C a b)(g : CatIso C b c) → j (⋆Iso f g) ≡ j f ∙ j g - 1-truncation : (x y : Ĉ₀)(p q : x ≡ y)(r s : p ≡ q) → r ≡ s - - -- the paragraph directly following the HIT definition, below theorem 9.9.5 of the HOTT book - _ : (a b : C .ob)(p : a ≡ b) → j (pathToIso p) ≡ congS i p - _ = λ a b p → J (λ y → λ eq → j (pathToIso eq) ≡ congS i eq) (j (pathToIso refl) ≡⟨ congS j pathToIso-refl ⟩ j idCatIso ≡⟨ jid ⟩ congS i refl ∎) p -- TODO: I don't really get this proof and why we want this theorem + [_] : (C.ob) → Ĉ₀ + iso// : {a b : C.ob}(e : CatIso C a b) → [ a ] ≡ [ b ] + id// : {a : C.ob} → iso// {a} idCatIso ≡ refl + -- | copied this from HITs.GroupoidQuotients + -- | Equivalent to the original but stated in terms of PathP + -- | instead of path composition + comp// : ∀ {a b c} → (e : CatIso C a b) → (e' : CatIso C b c) + → PathP (λ j → [ a ] ≡ iso// e' j) + (iso// e) + (iso// (⋆Iso e e')) + -- comp// : {a b c : C .ob}(f : CatIso C a b)(g : CatIso C b c) + -- → iso// (⋆Iso f g) ≡ iso// f ∙ iso// g + squash// : isGroupoid Ĉ₀ + + -- -- the paragraph directly following the HIT definition, below theorem 9.9.5 of the HOTT book + -- _ : (a b : C .ob)(p : a ≡ b) → j (pathToIso p) ≡ congS i p + -- _ = λ a b p → J (λ y → λ eq → j (pathToIso eq) ≡ congS i eq) (j (pathToIso refl) ≡⟨ congS j pathToIso-refl ⟩ j idCatIso ≡⟨ jid ⟩ congS i refl ∎) p -- TODO: I don't really get this proof and why we want this theorem open import Cubical.Foundations.Isomorphism open import Cubical.Categories.Category.Base open Cubical.Categories.Category.isIso open import Cubical.Foundations.Univalence open import Cubical.Foundations.Equiv - Ĉ₁ : Ĉ₀ → Ĉ₀ → Type _ - Ĉ₁ (i a) (i b) = (C [ a , b ]) - Ĉ₁ (i a) (j {b} {b'} e i') = ua (isoToEquiv (iso iso→ iso⁻¹← (λ g → iso→ (iso⁻¹← g) ≡⟨ refl ⟩ g ⋆⟨ C ⟩ e⁻¹← ⋆⟨ C ⟩ e→ ≡⟨ C .⋆Assoc g e⁻¹← e→ ⟩ g ⋆⟨ C ⟩ (e⁻¹← ⋆⟨ C ⟩ e→) ≡⟨ congS (λ eq → g ⋆⟨ C ⟩ eq) (e .snd .sec) ⟩ g ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR g ⟩ g ∎) (λ f → iso⁻¹← (iso→ f) ≡⟨ refl ⟩ f ⋆⟨ C ⟩ e→ ⋆⟨ C ⟩ e⁻¹← ≡⟨ C .⋆Assoc f e→ e⁻¹← ⟩ f ⋆⟨ C ⟩ (e→ ⋆⟨ C ⟩ e⁻¹←) ≡⟨ congS (λ eq → f ⋆⟨ C ⟩ eq) (e .snd .ret) ⟩ f ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR f ⟩ f ∎ ))) i' - -- isoToPath (iso iso→ iso⁻¹← (λ g → iso→ (iso⁻¹← g) ≡⟨ refl ⟩ g ⋆⟨ C ⟩ e⁻¹← ⋆⟨ C ⟩ e→ ≡⟨ C .⋆Assoc g e⁻¹← e→ ⟩ g ⋆⟨ C ⟩ (e⁻¹← ⋆⟨ C ⟩ e→) ≡⟨ congS (λ eq → g ⋆⟨ C ⟩ eq) (e .snd .sec) ⟩ g ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR g ⟩ g ∎) (λ f → iso⁻¹← (iso→ f) ≡⟨ refl ⟩ f ⋆⟨ C ⟩ e→ ⋆⟨ C ⟩ e⁻¹← ≡⟨ C .⋆Assoc f e→ e⁻¹← ⟩ f ⋆⟨ C ⟩ (e→ ⋆⟨ C ⟩ e⁻¹←) ≡⟨ congS (λ eq → f ⋆⟨ C ⟩ eq) (e .snd .ret) ⟩ f ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR f ⟩ f ∎ )) i' - where - e→ = e .fst - e⁻¹← = e .snd .inv - -- let f ∈ C [ a , b ], g ∈ C [ a , b' ] - -- explicit types to manually supply contraints - iso→ : C [ a , b ] → C [ a , b' ] - iso→ f = f ⋆⟨ C ⟩ e→ - iso⁻¹← : C [ a , b' ] → C [ a , b ] - iso⁻¹← g = g ⋆⟨ C ⟩ e⁻¹← - Ĉ₁ (i a) (jid {b} i' i'') = ( proof⋆id ≡⟨ congS ua (equivEq (funExt λ f → C .⋆IdR f)) ⟩ ua (idEquiv (C [ a , b ])) ≡⟨ uaIdEquiv ⟩ refl-hom ∎) i' i'' - where - iso→ : C [ a , b ] → C [ a , b ] - iso→ f = f ⋆⟨ C ⟩ (C .id) - iso⁻¹← : C [ a , b ] → C [ a , b ] - iso⁻¹← g = g ⋆⟨ C ⟩ (C .id) - proof⋆id : C [ a , b ] ≡ C [ a , b ] - proof⋆id = ua (isoToEquiv (iso iso→ iso⁻¹← (λ g → iso→ (iso⁻¹← g) ≡⟨ refl ⟩ g ⋆⟨ C ⟩ C .id ⋆⟨ C ⟩ C .id ≡⟨ C .⋆Assoc g (C .id) (C .id) ⟩ g ⋆⟨ C ⟩ (C .id ⋆⟨ C ⟩ C .id) ≡⟨ congS (λ eq → g ⋆⟨ C ⟩ eq) (C .⋆IdL (C .id)) ⟩ g ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR g ⟩ g ∎ ) (λ f → iso⁻¹← (iso→ f) ≡⟨ refl ⟩ f ⋆⟨ C ⟩ C .id ⋆⟨ C ⟩ C .id ≡⟨ C .⋆Assoc f (C .id) (C .id) ⟩ f ⋆⟨ C ⟩ (C .id ⋆⟨ C ⟩ C .id) ≡⟨ congS (λ eq → f ⋆⟨ C ⟩ eq) (C .⋆IdL (C .id)) ⟩ f ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR f ⟩ f ∎))) - refl-hom : C [ a , b ] ≡ C [ a , b ] - refl-hom = refl - --Ĉ₁ (i a) (jcomp {b} {c} {d} f g i' i'') = {!!} - --Ĉ₁ (j {a} {a'} e i') (i b) = {!!} + + elim : {P : Ĉ₀ → Type ℓ''} + → (∀ ĉ → isGroupoid (P ĉ)) + → (f-[_] : ∀ c → P [ c ]) + → (f-iso// : ∀ {a b} (e : CatIso C a b) + → PathP (λ i → P (iso// e i)) (f-[ a ]) (f-[ b ])) + → (f-id// : ∀ {a} → + SquareP (λ i j → P (id// {a} i j)) + ((f-iso// {a} idCatIso)) + refl + (λ j → f-[ a ]) + (cong f-[_] refl)) + → (f-comp// : ∀ {a b c} (e : CatIso C a b)(e' : CatIso C b c) + → SquareP (λ i j → P (comp// e e' i j)) + (f-iso// e) + (f-iso// (⋆Iso e e')) + (λ j → f-[ a ]) + (f-iso// e')) + → ∀ ĉ → P ĉ + elim isGroupoidP f-[_] f-iso// f-id// f-comp// [ c ] = f-[ c ] + elim isGroupoidP f-[_] f-iso// f-id// f-comp// (iso// e i) = f-iso// e i + elim isGroupoidP f-[_] f-iso// f-id// f-comp// (id// i j) = f-id// i j + elim isGroupoidP f-[_] f-iso// f-id// f-comp// (comp// f g i j) = f-comp// f g i j + elim isGroupoidP f-[_] f-iso// f-id// f-comp// (squash// ĉ ĉ' p p' q q' i j k) = + isOfHLevel→isOfHLevelDep 3 isGroupoidP + _ _ _ _ (λ j k → elimm (q j k)) (λ j k → elimm (q' j k)) (squash// ĉ ĉ' p p' q q') i j k where + elimm = elim isGroupoidP f-[_] f-iso// f-id// f-comp// + + ĈHom : Ĉ₀ → Ĉ₀ → hSet ℓ' + ĈHom = elim isGrpdFam ĈHomc + {!!} + {!!} + {!!} where + ĈHomc : C.ob → Ĉ₀ → hSet ℓ' + ĈHomc a = elim (λ _ → isGroupoidHSet) + (λ b → C.Hom[ a , b ] , C.isSetHom) + (λ {b c} e → + -- This follows from univalence of Set: + -- e : b ≅ c + -- C [ a ,-] ⟪ e ⟫ : C [ a , b ] ≅ C [ a , c ] + -- C [ a , b ] ≡ C [ a , c ] + isUnivalent.CatIsoToPath isUnivalentSET + (F-Iso {F = C [ a ,-]} e)) + {!!} + {!!} + + isGrpdFam : (ĉ : Ĉ₀) → isGroupoid (Ĉ₀ → hSet ℓ') + isGrpdFam _ = isGroupoidΠ (λ _ → isGroupoidHSet) + -- Ĉ₁ : Ĉ₀ → Ĉ₀ → Type _ + -- Ĉ₁ (i a) (i b) = (C [ a , b ]) + -- Ĉ₁ (i a) (j {b} {b'} e i') = ua (isoToEquiv (iso iso→ iso⁻¹← (λ g → iso→ (iso⁻¹← g) ≡⟨ refl ⟩ g ⋆⟨ C ⟩ e⁻¹← ⋆⟨ C ⟩ e→ ≡⟨ C .⋆Assoc g e⁻¹← e→ ⟩ g ⋆⟨ C ⟩ (e⁻¹← ⋆⟨ C ⟩ e→) ≡⟨ congS (λ eq → g ⋆⟨ C ⟩ eq) (e .snd .sec) ⟩ g ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR g ⟩ g ∎) (λ f → iso⁻¹← (iso→ f) ≡⟨ refl ⟩ f ⋆⟨ C ⟩ e→ ⋆⟨ C ⟩ e⁻¹← ≡⟨ C .⋆Assoc f e→ e⁻¹← ⟩ f ⋆⟨ C ⟩ (e→ ⋆⟨ C ⟩ e⁻¹←) ≡⟨ congS (λ eq → f ⋆⟨ C ⟩ eq) (e .snd .ret) ⟩ f ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR f ⟩ f ∎ ))) i' + -- -- isoToPath (iso iso→ iso⁻¹← (λ g → iso→ (iso⁻¹← g) ≡⟨ refl ⟩ g ⋆⟨ C ⟩ e⁻¹← ⋆⟨ C ⟩ e→ ≡⟨ C .⋆Assoc g e⁻¹← e→ ⟩ g ⋆⟨ C ⟩ (e⁻¹← ⋆⟨ C ⟩ e→) ≡⟨ congS (λ eq → g ⋆⟨ C ⟩ eq) (e .snd .sec) ⟩ g ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR g ⟩ g ∎) (λ f → iso⁻¹← (iso→ f) ≡⟨ refl ⟩ f ⋆⟨ C ⟩ e→ ⋆⟨ C ⟩ e⁻¹← ≡⟨ C .⋆Assoc f e→ e⁻¹← ⟩ f ⋆⟨ C ⟩ (e→ ⋆⟨ C ⟩ e⁻¹←) ≡⟨ congS (λ eq → f ⋆⟨ C ⟩ eq) (e .snd .ret) ⟩ f ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR f ⟩ f ∎ )) i' + -- where + -- e→ = e .fst + -- e⁻¹← = e .snd .inv + -- -- let f ∈ C [ a , b ], g ∈ C [ a , b' ] + -- -- explicit types to manually supply contraints + -- iso→ : C [ a , b ] → C [ a , b' ] + -- iso→ f = f ⋆⟨ C ⟩ e→ + -- iso⁻¹← : C [ a , b' ] → C [ a , b ] + -- iso⁻¹← g = g ⋆⟨ C ⟩ e⁻¹← + -- Ĉ₁ (i a) (jid {b} i' i'') = ( proof⋆id ≡⟨ congS ua (equivEq (funExt λ f → C .⋆IdR f)) ⟩ ua (idEquiv (C [ a , b ])) ≡⟨ uaIdEquiv ⟩ refl-hom ∎) i' i'' + -- where + -- iso→ : C [ a , b ] → C [ a , b ] + -- iso→ f = f ⋆⟨ C ⟩ (C .id) + -- iso⁻¹← : C [ a , b ] → C [ a , b ] + -- iso⁻¹← g = g ⋆⟨ C ⟩ (C .id) + -- proof⋆id : C [ a , b ] ≡ C [ a , b ] + -- proof⋆id = ua (isoToEquiv (iso iso→ iso⁻¹← (λ g → iso→ (iso⁻¹← g) ≡⟨ refl ⟩ g ⋆⟨ C ⟩ C .id ⋆⟨ C ⟩ C .id ≡⟨ C .⋆Assoc g (C .id) (C .id) ⟩ g ⋆⟨ C ⟩ (C .id ⋆⟨ C ⟩ C .id) ≡⟨ congS (λ eq → g ⋆⟨ C ⟩ eq) (C .⋆IdL (C .id)) ⟩ g ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR g ⟩ g ∎ ) (λ f → iso⁻¹← (iso→ f) ≡⟨ refl ⟩ f ⋆⟨ C ⟩ C .id ⋆⟨ C ⟩ C .id ≡⟨ C .⋆Assoc f (C .id) (C .id) ⟩ f ⋆⟨ C ⟩ (C .id ⋆⟨ C ⟩ C .id) ≡⟨ congS (λ eq → f ⋆⟨ C ⟩ eq) (C .⋆IdL (C .id)) ⟩ f ⋆⟨ C ⟩ C .id ≡⟨ C .⋆IdR f ⟩ f ∎))) + -- refl-hom : C [ a , b ] ≡ C [ a , b ] + -- refl-hom = refl + -- --Ĉ₁ (i a) (jcomp {b} {c} {d} f g i' i'') = {!!} + -- --Ĉ₁ (j {a} {a'} e i') (i b) = {!!}