resolved the isoToPath issue (see prev commit). From eric's suggestio…

…n Friday evening
maxsnew · Sep 3, 2023 · 934f042 · 934f042
1 parent 5252cf4
commit 934f042
Showing 1 changed file with 8 additions and 5 deletions.
diff --git 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) = {!!}