From 9b7d5f27c12ad31e634f264a31395f52ad365a72 Mon Sep 17 00:00:00 2001 From: Ulf Norell Date: Wed, 13 Nov 2024 14:54:49 +0100 Subject: [PATCH] Fix compilation with agda/agda#7581 --- Cubical/Categories/Constructions/Slice/Base.agda | 2 +- .../DistLatticeSheaf/ComparisonLemma.agda | 2 +- Cubical/Categories/Instances/CommAlgebras.agda | 5 ++--- Cubical/Categories/Limits/RightKan.agda | 14 +++++++------- Cubical/Categories/Presheaf/Properties.agda | 4 ++-- .../Categories/RezkCompletion/Construction.agda | 2 +- Cubical/Tactics/CategorySolver/Solver.agda | 2 +- Cubical/Tactics/FunctorSolver/Solver.agda | 2 +- 8 files changed, 16 insertions(+), 17 deletions(-) diff --git a/Cubical/Categories/Constructions/Slice/Base.agda b/Cubical/Categories/Constructions/Slice/Base.agda index c11652b7cf..f04453e4e7 100644 --- 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 index 3eaf2dfd27..74af31a6f9 100644 --- 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 index ef5a1cde61..dfd5d1f9de 100644 --- 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 index 08ef4b92b7..f45eafd6d4 100644 --- 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 index 1f79eb4c42..101866c4d7 100644 --- 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 index 029948031f..26f420355e 100644 --- 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 index 0748789418..fa1ebf6a7e 100644 --- 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 index aee48d7fe7..219ac60ef4 100644 --- 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 _