From 8cb8f11c54e9a1a17c7b24d6604a7df2032e8cbb Mon Sep 17 00:00:00 2001 From: Andreas Nuyts Date: Mon, 28 Oct 2024 18:12:16 +0100 Subject: [PATCH 1/2] PROP & SIEVE. --- Cubical/Categories/Instances/Functors.agda | 3 ++ .../Categories/Instances/Propositions.agda | 28 +++++++++++++++ .../Instances/SievesAsFunctors.agda | 34 +++++++++++++++++++ .../NaturalTransformation/Properties.agda | 3 ++ Cubical/Categories/Thin.agda | 12 +++++++ 5 files changed, 80 insertions(+) create mode 100644 Cubical/Categories/Instances/Propositions.agda create mode 100644 Cubical/Categories/Instances/SievesAsFunctors.agda create mode 100644 Cubical/Categories/Thin.agda diff --git a/Cubical/Categories/Instances/Functors.agda b/Cubical/Categories/Instances/Functors.agda index 789994b00e..567f9365d3 100644 --- a/Cubical/Categories/Instances/Functors.agda +++ b/Cubical/Categories/Instances/Functors.agda @@ -23,6 +23,7 @@ open import Cubical.Categories.Functor.Base open import Cubical.Categories.Morphism open import Cubical.Categories.NaturalTransformation.Base open import Cubical.Categories.NaturalTransformation.Properties +open import Cubical.Categories.Thin private variable @@ -138,3 +139,5 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where ≡⟨ D .⋆Assoc _ _ _ ⟩ (β .N-ob e ∘⟨ D ⟩ G .F-hom g) ∘⟨ D ⟩ (α .N-ob d ∘⟨ D ⟩ F .F-hom f) ∎ + isThinFUNCTOR : isThin D → isThin FUNCTOR + isThinFUNCTOR thinD F G = isThin→isPropNatTrans thinD diff --git a/Cubical/Categories/Instances/Propositions.agda b/Cubical/Categories/Instances/Propositions.agda new file mode 100644 index 0000000000..ca598539b3 --- /dev/null +++ b/Cubical/Categories/Instances/Propositions.agda @@ -0,0 +1,28 @@ +{-# OPTIONS --safe #-} + +module Cubical.Categories.Instances.Propositions where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Function + +open import Cubical.Categories.Category +open Category +open import Cubical.Categories.Thin + +private + variable + ℓ : Level + +PROP : ∀ (ℓ : Level) → Category (ℓ-suc ℓ) ℓ +ob (PROP ℓ) = hProp ℓ +Hom[_,_] (PROP ℓ) (P , _) (Q , _) = P → Q +id (PROP ℓ) = idfun _ +_⋆_ (PROP ℓ) f g x = g (f x) +⋆IdL (PROP ℓ) {P , _} {Q , propQ} f = isProp→ propQ _ _ +⋆IdR (PROP ℓ) {P , _} {Q , propQ} f = isProp→ propQ _ _ +⋆Assoc (PROP ℓ) {P , _} {Q , _} {R , _} {S , propS} f g h = isPropΠ (λ _ → propS) _ _ +isSetHom (PROP ℓ) {P , _} {Q , propQ} = isProp→isSet (isProp→ propQ) + +isThinPROP : isThin (PROP ℓ) +isThinPROP (P , propP) (Q , propQ) = isProp→ propQ diff --git a/Cubical/Categories/Instances/SievesAsFunctors.agda b/Cubical/Categories/Instances/SievesAsFunctors.agda new file mode 100644 index 0000000000..ddb0d8c817 --- /dev/null +++ b/Cubical/Categories/Instances/SievesAsFunctors.agda @@ -0,0 +1,34 @@ +{-# OPTIONS --safe #-} + +module Cubical.Categories.Instances.SievesAsFunctors where + +-- There are also sieves in Cubical.Site.Sieve + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels + +open import Cubical.Categories.Category +open Category +open import Cubical.Categories.Instances.Functors +open import Cubical.Categories.Instances.Propositions +open import Cubical.Categories.Constructions.Slice +open import Cubical.Categories.Thin + +private + variable + ℓ ℓ' ℓP : Level + C : Category ℓ ℓ' + +SIEVE : (C : Category ℓ ℓ') → (ℓP : Level) + → Category (ℓ-max (ℓ-max ℓ ℓ') (ℓ-suc ℓP)) (ℓ-max (ℓ-max ℓ ℓ') ℓP) +SIEVE C ℓP = FUNCTOR (C ^op) (PROP ℓP) + +Sieve : (C : Category ℓ ℓ') → (ℓP : Level) → Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-suc ℓP)) +Sieve C ℓP = SIEVE C ℓP .ob + +isThinSIEVE : isThin (SIEVE C ℓP) +isThinSIEVE = isThinFUNCTOR _ _ isThinPROP + +SIEVE_ON : (C : Category ℓ ℓ') → (c : C .ob) → (ℓP : Level) + → Category (ℓ-max (ℓ-max ℓ ℓ') (ℓ-suc ℓP)) (ℓ-max (ℓ-max ℓ ℓ') ℓP) +SIEVE_ON C c ℓP = SIEVE (SliceCat C c) ℓP diff --git a/Cubical/Categories/NaturalTransformation/Properties.agda b/Cubical/Categories/NaturalTransformation/Properties.agda index 5688a9021a..ecac50c60a 100644 --- a/Cubical/Categories/NaturalTransformation/Properties.agda +++ b/Cubical/Categories/NaturalTransformation/Properties.agda @@ -16,6 +16,7 @@ open import Cubical.Categories.Functor.Properties open import Cubical.Categories.Morphism open import Cubical.Categories.Isomorphism open import Cubical.Categories.NaturalTransformation.Base +open import Cubical.Categories.Thin private variable @@ -193,3 +194,5 @@ inv congNatIso^opFiso = _ rightInv congNatIso^opFiso _ = refl leftInv congNatIso^opFiso _ = refl +isThin→isPropNatTrans : ∀ {F G : Functor C D} → isThin D → isProp (NatTrans F G) +isThin→isPropNatTrans thinD μ ν = makeNatTransPath (isPropΠ (λ x → thinD _ _) _ _) diff --git a/Cubical/Categories/Thin.agda b/Cubical/Categories/Thin.agda new file mode 100644 index 0000000000..800fd07d4c --- /dev/null +++ b/Cubical/Categories/Thin.agda @@ -0,0 +1,12 @@ +{-# OPTIONS --safe #-} +module Cubical.Categories.Thin where + +open import Cubical.Foundations.Prelude +open import Cubical.Categories.Category +open Category + +private + variable ℓ ℓ' : Level + +isThin : (C : Category ℓ ℓ') → Type (ℓ-max ℓ ℓ') +isThin C = (x y : C .ob) → isProp (C [ x , y ]) From 42939d579566f26b7d932d49afeb4f5152aea3ee Mon Sep 17 00:00:00 2001 From: Andreas Nuyts Date: Tue, 29 Oct 2024 12:43:38 +0100 Subject: [PATCH 2/2] SieveOn. --- Cubical/Categories/Instances/SievesAsFunctors.agda | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Cubical/Categories/Instances/SievesAsFunctors.agda b/Cubical/Categories/Instances/SievesAsFunctors.agda index ddb0d8c817..a58f392eac 100644 --- a/Cubical/Categories/Instances/SievesAsFunctors.agda +++ b/Cubical/Categories/Instances/SievesAsFunctors.agda @@ -32,3 +32,6 @@ isThinSIEVE = isThinFUNCTOR _ _ isThinPROP SIEVE_ON : (C : Category ℓ ℓ') → (c : C .ob) → (ℓP : Level) → Category (ℓ-max (ℓ-max ℓ ℓ') (ℓ-suc ℓP)) (ℓ-max (ℓ-max ℓ ℓ') ℓP) SIEVE_ON C c ℓP = SIEVE (SliceCat C c) ℓP + +SieveOn : (C : Category ℓ ℓ') → (c : C .ob) → (ℓP : Level) → Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-suc ℓP)) +SieveOn C c ℓP = SIEVE_ON C c ℓP .ob