Fix compilation with agda/agda#7581

agda · Nov 13, 2024 · 3694581 · 3694581
1 parent 5449cc2
commit 3694581
Show file tree

Hide file tree

Showing 8 changed files with 16 additions and 17 deletions.
diff --git a/Cubical/Categories/Constructions/Slice/Base.agda b/Cubical/Categories/Constructions/Slice/Base.agda
@@ -46,7 +46,7 @@ open SliceHom public
 -- can probably replace these by showing that SliceOb is isomorphic to Sigma and
 -- that paths are isomorphic to Sigma? But sounds like that would need a lot of transp
 
-SliceOb-≡-intro : ∀ {a b} {f g}
+SliceOb-≡-intro : ∀ {a b} {f : C [ a , c ]} {g : C [ b , c ]}
                  → (p : a ≡ b)
                  → PathP (λ i → C [ p i , c ]) f g
                  → sliceob {a} f ≡ sliceob {b} g

diff --git a/Cubical/Categories/DistLatticeSheaf/ComparisonLemma.agda b/Cubical/Categories/DistLatticeSheaf/ComparisonLemma.agda
@@ -399,7 +399,7 @@ module _ (L : DistLattice ℓ) (C : Category ℓ' ℓ'') (limitC : Limits {ℓ}
                          (NatTransCone _ _ _ F (idTrans _) x)
                    ⋆⟨ C ⟩ limOfArrows (FLimCone (α ∘ˡ i) _) (GLimCone (α ∘ˡ i) _)
                                       (↓nt (α ∘ˡ i) x)
-         goal x = sym (limArrowUnique _ _ _ _ (isConeMorComp x))
+         goal x = sym (limArrowUnique {C = C} _ _ _ _ (isConeMorComp x))
                 ∙ limArrowCompLimOfArrows _ _ _ _ _
 
      nIso (η winv) (F , isSheafF) = isIsoΣPropCat _ _ _

diff --git a/Cubical/Categories/Instances/CommAlgebras.agda b/Cubical/Categories/Instances/CommAlgebras.agda
@@ -675,10 +675,9 @@ module PreSheafFromUniversalProp (C : Category ℓ ℓ') (P : ob C → Type ℓ)
     assocDiagPath : Forgetful ∘F (universalPShf ∘F D) ≡ 𝓖 ∘F D
     assocDiagPath = F-assoc
 
-    conePathPCR : PathP (λ i → Cone (assocDiagPath i) (F-ob (Forgetful ∘F universalPShf) c))
+    conePathPCR : PathP (λ i → Cone (assocDiagPath i) (F-ob 𝓖 c))
                    (F-cone Forgetful (F-cone universalPShf cc)) (F-cone 𝓖 cc)
-    conePathPCR = conePathPDiag -- why does everything have to be explicit?
-            (λ v _ → (Forgetful ∘F universalPShf) .F-hom {x = c} {y = D .F-ob v} (cc .coneOut v))
+    conePathPCR = conePathPDiag (λ v _ → 𝓖 .F-hom (cc .coneOut v))
 
 
    toLimCone : isLimCone _ _ (F-cone 𝓖 cc)

diff --git a/Cubical/Categories/Limits/RightKan.agda b/Cubical/Categories/Limits/RightKan.agda
@@ -106,9 +106,9 @@ module _ {ℓC ℓC' ℓM ℓM' ℓA ℓA' : Level}
   path v = (F-hom Ran f) ⋆⟨ A ⟩ (F-hom Ran g) ⋆⟨ A ⟩ (limOut (limitA (z ↓Diag) (T* z)) v)
          ≡⟨ ⋆Assoc A _ _ _ ⟩
            (F-hom Ran f) ⋆⟨ A ⟩ ((F-hom Ran g) ⋆⟨ A ⟩ (limOut (limitA (z ↓Diag) (T* z)) v))
-         ≡⟨ cong (seq' A (F-hom Ran f)) (limArrowCommutes _ _ _ _) ⟩
+         ≡⟨ cong (seq' A (F-hom Ran f)) (limArrowCommutes (limitA _ _) _ _ _) ⟩
            (F-hom Ran f) ⋆⟨ A ⟩ limOut (limitA (y ↓Diag) (T* y)) (j g .F-ob v)
-         ≡⟨ limArrowCommutes _ _ _ _ ⟩
+         ≡⟨ limArrowCommutes (limitA _ _) _ _ _ ⟩
            limOut (limitA (x ↓Diag) (T* x)) (j f .F-ob (j g .F-ob v))
          ≡⟨ RanConeTrans f g v ⟩
            coneOut (RanCone (f ⋆⟨ C ⟩ g)) v ∎
@@ -121,7 +121,7 @@ module _ {ℓC ℓC' ℓM ℓM' ℓA ℓA' : Level}
      Ran .F-hom (K .F-hom f) ⋆⟨ A ⟩ coneOut (RanCone (id C)) (v , id C)
    ≡⟨ cong (λ g → Ran .F-hom (K .F-hom f) ⋆⟨ A ⟩ g) (sym (RanConeRefl (v , id C))) ⟩
      Ran .F-hom (K .F-hom f) ⋆⟨ A ⟩ limOut (limitA ((K .F-ob v) ↓Diag) (T* (K .F-ob v))) (v , id C)
-   ≡⟨ limArrowCommutes _ _ _ _ ⟩
+   ≡⟨ limArrowCommutes (limitA _ _) _ _ _ ⟩
      coneOut (RanCone (K .F-hom f)) (v , id C)
    ≡⟨ cong (λ g → limOut (limitA ((K .F-ob u) ↓Diag) (T* (K .F-ob u))) (v , g))
                          (⋆IdR C (K .F-hom f) ∙ sym (⋆IdL C (K .F-hom f))) ⟩
@@ -169,15 +169,15 @@ module _ {ℓC ℓC' ℓM ℓM' ℓA ℓA' : Level}
          (S .F-hom f ⋆⟨ A ⟩ N-ob σ y) ⋆⟨ A ⟩ limOut (limitA (y ↓Diag) (T* y)) (u , g)
        ≡⟨ ⋆Assoc A _ _ _ ⟩
          S .F-hom f ⋆⟨ A ⟩ (N-ob σ y ⋆⟨ A ⟩ limOut (limitA (y ↓Diag) (T* y)) (u , g))
-       ≡⟨ cong (seq' A (S .F-hom f)) (limArrowCommutes _ _ _ _) ⟩
+       ≡⟨ cong (seq' A (S .F-hom f)) (limArrowCommutes (limitA _ _) _ _ _) ⟩
          S .F-hom f ⋆⟨ A ⟩ (S .F-hom g ⋆⟨ A ⟩ α .N-ob u)
        ≡⟨ sym (⋆Assoc A _ _ _) ⟩
          (S .F-hom f ⋆⟨ A ⟩ S .F-hom g) ⋆⟨ A ⟩ α .N-ob u
        ≡⟨ cong (λ h → h ⋆⟨ A ⟩ α .N-ob u) (sym (S .F-seq _ _)) ⟩
          S .F-hom (f ⋆⟨ C ⟩ g) ⋆⟨ A ⟩ α .N-ob u
-       ≡⟨ sym (limArrowCommutes _ _ _ _) ⟩
+       ≡⟨ sym (limArrowCommutes (limitA _ _) _ _ _) ⟩
          N-ob σ x ⋆⟨ A ⟩ limOut (limitA (x ↓Diag) (T* x)) (u , f ⋆⟨ C ⟩ g)
-       ≡⟨ cong (seq' A (N-ob σ x)) (sym (limArrowCommutes _ _ _ _)) ⟩
+       ≡⟨ cong (seq' A (N-ob σ x)) (sym (limArrowCommutes (limitA _ _) _ _ _)) ⟩
          N-ob σ x ⋆⟨ A ⟩ (Ran .F-hom f ⋆⟨ A ⟩ limOut (limitA (y ↓Diag) (T* y)) (u , g))
        ≡⟨ sym (⋆Assoc A _ _ _) ⟩
          (N-ob σ x ⋆⟨ A ⟩ Ran .F-hom f) ⋆⟨ A ⟩ limOut (limitA (y ↓Diag) (T* y)) (u , g) ∎
@@ -200,7 +200,7 @@ module _ {ℓC ℓC' ℓM ℓM' ℓA ℓA' : Level}
          S .F-hom (id C ⋆⟨ C ⟩ id C) ⋆⟨ A ⟩ α .N-ob u
        ≡⟨ refl ⟩
          NatTransCone S α (F-ob K u) .coneOut (u , id C ⋆⟨ C ⟩ id C)
-       ≡⟨ sym (limArrowCommutes _ _ _ _) ⟩
+       ≡⟨ sym (limArrowCommutes (limitA _ _) _ _ _) ⟩
          limArrow (limitA ((K .F-ob u) ↓Diag) (T* (K .F-ob u))) _ (NatTransCone S α (F-ob K u))
            ⋆⟨ A ⟩ limOut (limitA ((K .F-ob u) ↓Diag) (T* (K .F-ob u))) (u , id C ⋆⟨ C ⟩ id C) ∎
 

diff --git a/Cubical/Categories/Presheaf/Properties.agda b/Cubical/Categories/Presheaf/Properties.agda
@@ -329,7 +329,7 @@ module _ {ℓS : Level} (C : Category ℓ ℓ') (F : Functor (C ^op) (SET ℓS))
                   refl≡comm : PathP (λ i → (F ⟪ f ⟫) (eq i) ≡ (eq' i)) refl comm
                   refl≡comm = isOfHLevel→isOfHLevelDep 1 (λ (v , w) → snd (F ⟅ d ⟆) ((F ⟪ f ⟫) w) v) refl comm λ i → (eq' i , eq i)
 
-                  X'≡subst : PathP (λ i → fst (P ⟅ c , eq i ⟆)) X' (subst _ eq X')
+                  X'≡subst : PathP (λ i → fst (P ⟅ c , eq i ⟆)) X' (subst (λ v → fst (P ⟅ c , v ⟆)) eq X')
                   X'≡subst = transport-filler (λ i → fst (P ⟅ c , eq i ⟆)) X'
 
               -- bottom left of the commuting diagram
@@ -355,7 +355,7 @@ module _ {ℓS : Level} (C : Category ℓ ℓ') (F : Functor (C ^op) (SET ℓS))
             right i = (α ⟦ c , eq i ⟧) (X'≡subst i)
               where
                 -- this is exactly the same as the one from before, can refactor?
-                X'≡subst : PathP (λ i → fst (P ⟅ c , eq i ⟆)) X' (subst _ eq X')
+                X'≡subst : PathP (λ i → fst (P ⟅ c , eq i ⟆)) X' (subst (λ v → fst (P ⟅ c , v ⟆)) eq X')
                 X'≡subst = transport-filler _ _
 
             -- extracted out type since need to use in in 'left' body as well

diff --git a/Cubical/Categories/RezkCompletion/Construction.agda b/Cubical/Categories/RezkCompletion/Construction.agda
@@ -51,7 +51,7 @@ module RezkByYoneda (C : Category ℓ ℓ) where
   ToYonedaImage = ToEssentialImage _
 
   isWeakEquivalenceToYonedaImage : isWeakEquivalence ToYonedaImage
-  isWeakEquivalenceToYonedaImage .fullfaith = isFullyFaithfulToEssentialImage _ isFullyFaithfulYO
+  isWeakEquivalenceToYonedaImage .fullfaith = isFullyFaithfulToEssentialImage YO isFullyFaithfulYO
   isWeakEquivalenceToYonedaImage .esssurj   = isEssentiallySurjToEssentialImage YO
 
   isRezkCompletionToYonedaImage : isRezkCompletion ToYonedaImage

diff --git a/Cubical/Tactics/CategorySolver/Solver.agda b/Cubical/Tactics/CategorySolver/Solver.agda
@@ -51,7 +51,7 @@ module Eval (𝓒 : Category ℓ ℓ') where
   solve : ∀ {A B} → (e₁ e₂ : W𝓒 [ A , B ])
         → eval e₁ ≡ eval e₂
         → ⟦ e₁ ⟧c ≡ ⟦ e₂ ⟧c
-  solve {A}{B} e₁ e₂ p = cong ⟦_⟧c (isFaithfulPseudoYoneda _ _ _ _ lem) where
+  solve {A}{B} e₁ e₂ p = cong ⟦_⟧c (isFaithfulPseudoYoneda {C = W𝓒} _ _ _ _ lem) where
     lem : 𝓘 ⟪ e₁ ⟫ ≡ 𝓘 ⟪ e₂ ⟫
     lem = transport
             (λ i → Yo-YoSem-agree (~ i) ⟪ e₁ ⟫ ≡ Yo-YoSem-agree (~ i) ⟪ e₂ ⟫)

diff --git a/Cubical/Tactics/FunctorSolver/Solver.agda b/Cubical/Tactics/FunctorSolver/Solver.agda
@@ -55,7 +55,7 @@ module Eval (𝓒 : Category ℓc ℓc') (𝓓 : Category ℓd ℓd')  (𝓕 : F
         → (p : Path _ (YoSem.semH ⟪ e ⟫) (YoSem.semH ⟪ e' ⟫))
         → Path _ (TautoSem.semH ⟪ e ⟫) (TautoSem.semH ⟪ e' ⟫)
   solve {A}{B} e e' p =
-    cong (TautoSem.semH .F-hom) (isFaithfulPseudoYoneda _ _ _ _ lem) where
+    cong (TautoSem.semH .F-hom) (isFaithfulPseudoYoneda {C = Free𝓓} _ _ _ _ lem) where
     lem : Path _ (PsYo ⟪ e ⟫) (PsYo ⟪ e' ⟫)
     lem = transport
           (λ i → Path _