yeah this is stuck. I'll come back when I understand actual HoTT better

maxsnew · Sep 3, 2023 · 5252cf4 · 5252cf4
1 parent aef464a
commit 5252cf4
Showing 1 changed file with 3 additions and 2 deletions.
diff --git 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'') = {!!}