From 21363dbb78d424a5809302d8a78d2a3d728b80be Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 15 May 2018 16:28:04 +0200 Subject: [PATCH] Move opposite- and span- category to own modules --- doc/implementation.tex | 15 +- src/Cat.agda | 1 + src/Cat/Categories/CwF.agda | 1 + src/Cat/Categories/Fun.agda | 2 +- src/Cat/Categories/Opposite.agda | 96 ++++++++ src/Cat/Categories/Sets.agda | 4 +- src/Cat/Categories/Span.agda | 173 ++++++++++++++ src/Cat/Category.agda | 92 -------- src/Cat/Category/Product.agda | 377 +++++++++---------------------- src/Cat/Category/Yoneda.agda | 4 +- 10 files changed, 389 insertions(+), 376 deletions(-) create mode 100644 src/Cat/Categories/Opposite.agda create mode 100644 src/Cat/Categories/Span.agda diff --git a/doc/implementation.tex b/doc/implementation.tex index d94f033..75f2df7 100644 --- a/doc/implementation.tex +++ b/doc/implementation.tex @@ -10,19 +10,20 @@ Name & Link \\ \hline Categories & \sourcelink{Cat.Category} \\ Functors & \sourcelink{Cat.Category.Functor} \\ -Products & \sourcelink{Cat.Category.Products} \\ -Exponentials & \sourcelink{Cat.Category.Exponentials} \\ +Products & \sourcelink{Cat.Category.Product} \\ +Exponentials & \sourcelink{Cat.Category.Exponential} \\ Cartesian closed categories & \sourcelink{Cat.Category.CartesianClosed} \\ Natural transformations & \sourcelink{Cat.Category.NaturalTransformation} \\ Yoneda embedding & \sourcelink{Cat.Category.Yoneda} \\ -Monads & \sourcelink{Cat.Category.Monads} \\ +Monads & \sourcelink{Cat.Category.Monad} \\ +Kleisli Monads & \sourcelink{Cat.Category.Monad.Kleisli} \\ +Monoidal Monads & \sourcelink{Cat.Category.Monad.Monoidal} \\ +Voevodsky's construction & \sourcelink{Cat.Category.Monad.Voevodsky} \\ %% Categories & \null \\ %% -Opposite category & -\href{\sourcebasepath Cat.Category.html#22744}{\texttt{Cat.Category.Opposite}} \\ +Opposite category & \sourcelink{Cat.Categories.Opposite} \\ Category of sets & \sourcelink{Cat.Categories.Sets} \\ -Span category & -\href{\sourcebasepath Cat.Category.Product.html#2919}{\texttt{Cat.Category.Product.Span}} \\ +Span category & \sourcelink{Cat.Categories.Span} \\ %% \end{tabular} \end{center} diff --git a/src/Cat.agda b/src/Cat.agda index fca9c99..a2d73e8 100644 --- a/src/Cat.agda +++ b/src/Cat.agda @@ -14,6 +14,7 @@ open import Cat.Category.Monad.Monoidal open import Cat.Category.Monad.Kleisli open import Cat.Category.Monad.Voevodsky +open import Cat.Categories.Opposite open import Cat.Categories.Sets open import Cat.Categories.Cat open import Cat.Categories.Rel diff --git a/src/Cat/Categories/CwF.agda b/src/Cat/Categories/CwF.agda index 1a491ec..9c1fc6d 100644 --- a/src/Cat/Categories/CwF.agda +++ b/src/Cat/Categories/CwF.agda @@ -5,6 +5,7 @@ open import Cat.Prelude open import Cat.Category open import Cat.Category.Functor open import Cat.Categories.Fam +open import Cat.Categories.Opposite module _ {ℓa ℓb : Level} where record CwF : Set (lsuc (ℓa ⊔ ℓb)) where diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index eb861e7..bcfb508 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -3,11 +3,11 @@ module Cat.Categories.Fun where open import Cat.Prelude open import Cat.Equivalence - open import Cat.Category open import Cat.Category.Functor import Cat.Category.NaturalTransformation as NaturalTransformation +open import Cat.Categories.Opposite module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where open NaturalTransformation ℂ 𝔻 public hiding (module Properties) diff --git a/src/Cat/Categories/Opposite.agda b/src/Cat/Categories/Opposite.agda new file mode 100644 index 0000000..ef2fa33 --- /dev/null +++ b/src/Cat/Categories/Opposite.agda @@ -0,0 +1,96 @@ +{-# OPTIONS --cubical #-} +module Cat.Categories.Opposite where + +open import Cat.Prelude +open import Cat.Equivalence +open import Cat.Category + +-- | The opposite category +-- +-- The opposite category is the category where the direction of the arrows are +-- flipped. +module _ {ℓa ℓb : Level} where + module _ (ℂ : Category ℓa ℓb) where + private + module _ where + module ℂ = Category ℂ + opRaw : RawCategory ℓa ℓb + RawCategory.Object opRaw = ℂ.Object + RawCategory.Arrow opRaw = flip ℂ.Arrow + RawCategory.identity opRaw = ℂ.identity + RawCategory._<<<_ opRaw = ℂ._>>>_ + + open RawCategory opRaw + + isPreCategory : IsPreCategory opRaw + IsPreCategory.isAssociative isPreCategory = sym ℂ.isAssociative + IsPreCategory.isIdentity isPreCategory = swap ℂ.isIdentity + IsPreCategory.arrowsAreSets isPreCategory = ℂ.arrowsAreSets + + open IsPreCategory isPreCategory + + module _ {A B : ℂ.Object} where + open Σ (toIso _ _ (ℂ.univalent {A} {B})) + renaming (fst to idToIso* ; snd to inv*) + open AreInverses {f = ℂ.idToIso A B} {idToIso*} inv* + + shuffle : A ≊ B → A ℂ.≊ B + shuffle (f , g , inv) = g , f , inv + + shuffle~ : A ℂ.≊ B → A ≊ B + shuffle~ (f , g , inv) = g , f , inv + + lem : (p : A ≡ B) → idToIso A B p ≡ shuffle~ (ℂ.idToIso A B p) + lem p = isoEq refl + + isoToId* : A ≊ B → A ≡ B + isoToId* = idToIso* ∘ shuffle + + inv : AreInverses (idToIso A B) isoToId* + inv = + ( funExt (λ x → begin + (isoToId* ∘ idToIso A B) x + ≡⟨⟩ + (idToIso* ∘ shuffle ∘ idToIso A B) x + ≡⟨ cong (λ φ → φ x) (cong (λ φ → idToIso* ∘ shuffle ∘ φ) (funExt lem)) ⟩ + (idToIso* ∘ shuffle ∘ shuffle~ ∘ ℂ.idToIso A B) x + ≡⟨⟩ + (idToIso* ∘ ℂ.idToIso A B) x + ≡⟨ (λ i → verso-recto i x) ⟩ + x ∎) + , funExt (λ x → begin + (idToIso A B ∘ idToIso* ∘ shuffle) x + ≡⟨ cong (λ φ → φ x) (cong (λ φ → φ ∘ idToIso* ∘ shuffle) (funExt lem)) ⟩ + (shuffle~ ∘ ℂ.idToIso A B ∘ idToIso* ∘ shuffle) x + ≡⟨ cong (λ φ → φ x) (cong (λ φ → shuffle~ ∘ φ ∘ shuffle) recto-verso) ⟩ + (shuffle~ ∘ shuffle) x + ≡⟨⟩ + x ∎) + ) + + isCategory : IsCategory opRaw + IsCategory.isPreCategory isCategory = isPreCategory + IsCategory.univalent isCategory + = univalenceFromIsomorphism (isoToId* , inv) + + opposite : Category ℓa ℓb + Category.raw opposite = opRaw + Category.isCategory opposite = isCategory + + -- As demonstrated here a side-effect of having no-eta-equality on constructors + -- means that we need to pick things apart to show that things are indeed + -- definitionally equal. I.e; a thing that would normally be provable in one + -- line now takes 13!! Admittedly it's a simple proof. + module _ {ℂ : Category ℓa ℓb} where + open Category ℂ + private + -- Since they really are definitionally equal we just need to pick apart + -- the data-type. + rawInv : Category.raw (opposite (opposite ℂ)) ≡ raw + RawCategory.Object (rawInv _) = Object + RawCategory.Arrow (rawInv _) = Arrow + RawCategory.identity (rawInv _) = identity + RawCategory._<<<_ (rawInv _) = _<<<_ + + oppositeIsInvolution : opposite (opposite ℂ) ≡ ℂ + oppositeIsInvolution = Category≡ rawInv diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index e707b55..e25f148 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -3,11 +3,11 @@ module Cat.Categories.Sets where open import Cat.Prelude as P - +open import Cat.Equivalence open import Cat.Category open import Cat.Category.Functor open import Cat.Category.Product -open import Cat.Equivalence +open import Cat.Categories.Opposite _⊙_ : {ℓa ℓb ℓc : Level} {A : Set ℓa} {B : Set ℓb} {C : Set ℓc} → (A ≃ B) → (B ≃ C) → A ≃ C eqA ⊙ eqB = Equivalence.compose eqA eqB diff --git a/src/Cat/Categories/Span.agda b/src/Cat/Categories/Span.agda new file mode 100644 index 0000000..3573266 --- /dev/null +++ b/src/Cat/Categories/Span.agda @@ -0,0 +1,173 @@ +{-# OPTIONS --cubical --caching #-} +module Cat.Categories.Span where + +open import Cat.Prelude as P hiding (_×_ ; fst ; snd) +open import Cat.Equivalence +open import Cat.Category + +module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) + (let module ℂ = Category ℂ) (𝒜 ℬ : ℂ.Object) where + + open P + + private + module _ where + raw : RawCategory _ _ + raw = record + { Object = Σ[ X ∈ ℂ.Object ] ℂ.Arrow X 𝒜 × ℂ.Arrow X ℬ + ; Arrow = λ{ (A , a0 , a1) (B , b0 , b1) + → Σ[ f ∈ ℂ.Arrow A B ] + ℂ [ b0 ∘ f ] ≡ a0 + × ℂ [ b1 ∘ f ] ≡ a1 + } + ; identity = λ{ {X , f , g} → ℂ.identity {X} , ℂ.rightIdentity , ℂ.rightIdentity} + ; _<<<_ = λ { {_ , a0 , a1} {_ , b0 , b1} {_ , c0 , c1} (f , f0 , f1) (g , g0 , g1) + → (f ℂ.<<< g) + , (begin + ℂ [ c0 ∘ ℂ [ f ∘ g ] ] ≡⟨ ℂ.isAssociative ⟩ + ℂ [ ℂ [ c0 ∘ f ] ∘ g ] ≡⟨ cong (λ φ → ℂ [ φ ∘ g ]) f0 ⟩ + ℂ [ b0 ∘ g ] ≡⟨ g0 ⟩ + a0 ∎ + ) + , (begin + ℂ [ c1 ∘ ℂ [ f ∘ g ] ] ≡⟨ ℂ.isAssociative ⟩ + ℂ [ ℂ [ c1 ∘ f ] ∘ g ] ≡⟨ cong (λ φ → ℂ [ φ ∘ g ]) f1 ⟩ + ℂ [ b1 ∘ g ] ≡⟨ g1 ⟩ + a1 ∎ + ) + } + } + + module _ where + open RawCategory raw + + propEqs : ∀ {X' : Object}{Y' : Object} (let X , xa , xb = X') (let Y , ya , yb = Y') + → (xy : ℂ.Arrow X Y) → isProp (ℂ [ ya ∘ xy ] ≡ xa × ℂ [ yb ∘ xy ] ≡ xb) + propEqs xs = propSig (ℂ.arrowsAreSets _ _) (\ _ → ℂ.arrowsAreSets _ _) + + arrowEq : {X Y : Object} {f g : Arrow X Y} → fst f ≡ fst g → f ≡ g + arrowEq {X} {Y} {f} {g} p = λ i → p i , lemPropF propEqs p {snd f} {snd g} i + + isAssociative : IsAssociative + isAssociative {f = f , f0 , f1} {g , g0 , g1} {h , h0 , h1} = arrowEq ℂ.isAssociative + + isIdentity : IsIdentity identity + isIdentity {AA@(A , a0 , a1)} {BB@(B , b0 , b1)} {f , f0 , f1} = arrowEq ℂ.leftIdentity , arrowEq ℂ.rightIdentity + + arrowsAreSets : ArrowsAreSets + arrowsAreSets {X , x0 , x1} {Y , y0 , y1} + = sigPresSet ℂ.arrowsAreSets λ a → propSet (propEqs _) + + isPreCat : IsPreCategory raw + IsPreCategory.isAssociative isPreCat = isAssociative + IsPreCategory.isIdentity isPreCat = isIdentity + IsPreCategory.arrowsAreSets isPreCat = arrowsAreSets + + open IsPreCategory isPreCat + + module _ {𝕏 𝕐 : Object} where + open Σ 𝕏 renaming (fst to X ; snd to x) + open Σ x renaming (fst to xa ; snd to xb) + open Σ 𝕐 renaming (fst to Y ; snd to y) + open Σ y renaming (fst to ya ; snd to yb) + open import Cat.Equivalence using (composeIso) renaming (_≅_ to _≅_) + step0 + : ((X , xa , xb) ≡ (Y , ya , yb)) + ≅ (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya) × (PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb)) + step0 + = (λ p → cong fst p , cong-d (fst ∘ snd) p , cong-d (snd ∘ snd) p) + -- , (λ x → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i)) + , (λ{ (p , q , r) → Σ≡ p λ i → q i , r i}) + , funExt (λ{ p → refl}) + , funExt (λ{ (p , q , r) → refl}) + + step1 + : (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya) × (PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb)) + ≅ Σ (X ℂ.≊ Y) (λ iso + → let p = ℂ.isoToId iso + in + ( PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya) + × PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb + ) + step1 + = symIso + (isoSigFst + {A = (X ℂ.≊ Y)} + {B = (X ≡ Y)} + (ℂ.groupoidObject _ _) + {Q = \ p → (PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya) × (PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb)} + ℂ.isoToId + (symIso (_ , ℂ.asTypeIso {X} {Y}) .snd) + ) + + step2 + : Σ (X ℂ.≊ Y) (λ iso + → let p = ℂ.isoToId iso + in + ( PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya) + × PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb + ) + ≅ ((X , xa , xb) ≊ (Y , ya , yb)) + step2 + = ( λ{ (iso@(f , f~ , inv-f) , p , q) + → ( f , sym (ℂ.domain-twist-sym iso p) , sym (ℂ.domain-twist-sym iso q)) + , ( f~ , sym (ℂ.domain-twist iso p) , sym (ℂ.domain-twist iso q)) + , arrowEq (fst inv-f) + , arrowEq (snd inv-f) + } + ) + , (λ{ (f , f~ , inv-f , inv-f~) → + let + iso : X ℂ.≊ Y + iso = fst f , fst f~ , cong fst inv-f , cong fst inv-f~ + p : X ≡ Y + p = ℂ.isoToId iso + pA : ℂ.Arrow X 𝒜 ≡ ℂ.Arrow Y 𝒜 + pA = cong (λ x → ℂ.Arrow x 𝒜) p + pB : ℂ.Arrow X ℬ ≡ ℂ.Arrow Y ℬ + pB = cong (λ x → ℂ.Arrow x ℬ) p + k0 = begin + coe pB xb ≡⟨ ℂ.coe-dom iso ⟩ + xb ℂ.<<< fst f~ ≡⟨ snd (snd f~) ⟩ + yb ∎ + k1 = begin + coe pA xa ≡⟨ ℂ.coe-dom iso ⟩ + xa ℂ.<<< fst f~ ≡⟨ fst (snd f~) ⟩ + ya ∎ + in iso , coe-lem-inv k1 , coe-lem-inv k0}) + , funExt (λ x → lemSig + (λ x → propSig prop0 (λ _ → prop1)) + _ _ + (Σ≡ refl (ℂ.propIsomorphism _ _ _))) + , funExt (λ{ (f , _) → lemSig propIsomorphism _ _ (Σ≡ refl (propEqs _ _ _))}) + where + prop0 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) 𝒜) xa ya) + prop0 {x} = pathJ (λ y p → ∀ x → isProp (PathP (λ i → ℂ.Arrow (p i) 𝒜) xa x)) (λ x → ℂ.arrowsAreSets _ _) Y (ℂ.isoToId x) ya + prop1 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) ℬ) xb yb) + prop1 {x} = pathJ (λ y p → ∀ x → isProp (PathP (λ i → ℂ.Arrow (p i) ℬ) xb x)) (λ x → ℂ.arrowsAreSets _ _) Y (ℂ.isoToId x) yb + -- One thing to watch out for here is that the isomorphisms going forwards + -- must compose to give idToIso + iso + : ((X , xa , xb) ≡ (Y , ya , yb)) + ≅ ((X , xa , xb) ≊ (Y , ya , yb)) + iso = step0 ⊙ step1 ⊙ step2 + where + infixl 5 _⊙_ + _⊙_ = composeIso + equiv1 + : ((X , xa , xb) ≡ (Y , ya , yb)) + ≃ ((X , xa , xb) ≊ (Y , ya , yb)) + equiv1 = _ , fromIso _ _ (snd iso) + + univalent : Univalent + univalent = univalenceFrom≃ equiv1 + + isCat : IsCategory raw + IsCategory.isPreCategory isCat = isPreCat + IsCategory.univalent isCat = univalent + + span : Category _ _ + span = record + { raw = raw + ; isCategory = isCat + } diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 274f94e..139fba9 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -631,95 +631,3 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where _[_∘_] : {A B C : Object} → (g : Arrow B C) → (f : Arrow A B) → Arrow A C _[_∘_] = _<<<_ - --- | The opposite category --- --- The opposite category is the category where the direction of the arrows are --- flipped. -module Opposite {ℓa ℓb : Level} where - module _ (ℂ : Category ℓa ℓb) where - private - module _ where - module ℂ = Category ℂ - opRaw : RawCategory ℓa ℓb - RawCategory.Object opRaw = ℂ.Object - RawCategory.Arrow opRaw = flip ℂ.Arrow - RawCategory.identity opRaw = ℂ.identity - RawCategory._<<<_ opRaw = ℂ._>>>_ - - open RawCategory opRaw - - isPreCategory : IsPreCategory opRaw - IsPreCategory.isAssociative isPreCategory = sym ℂ.isAssociative - IsPreCategory.isIdentity isPreCategory = swap ℂ.isIdentity - IsPreCategory.arrowsAreSets isPreCategory = ℂ.arrowsAreSets - - open IsPreCategory isPreCategory - - module _ {A B : ℂ.Object} where - open Σ (toIso _ _ (ℂ.univalent {A} {B})) - renaming (fst to idToIso* ; snd to inv*) - open AreInverses {f = ℂ.idToIso A B} {idToIso*} inv* - - shuffle : A ≊ B → A ℂ.≊ B - shuffle (f , g , inv) = g , f , inv - - shuffle~ : A ℂ.≊ B → A ≊ B - shuffle~ (f , g , inv) = g , f , inv - - lem : (p : A ≡ B) → idToIso A B p ≡ shuffle~ (ℂ.idToIso A B p) - lem p = isoEq refl - - isoToId* : A ≊ B → A ≡ B - isoToId* = idToIso* ∘ shuffle - - inv : AreInverses (idToIso A B) isoToId* - inv = - ( funExt (λ x → begin - (isoToId* ∘ idToIso A B) x - ≡⟨⟩ - (idToIso* ∘ shuffle ∘ idToIso A B) x - ≡⟨ cong (λ φ → φ x) (cong (λ φ → idToIso* ∘ shuffle ∘ φ) (funExt lem)) ⟩ - (idToIso* ∘ shuffle ∘ shuffle~ ∘ ℂ.idToIso A B) x - ≡⟨⟩ - (idToIso* ∘ ℂ.idToIso A B) x - ≡⟨ (λ i → verso-recto i x) ⟩ - x ∎) - , funExt (λ x → begin - (idToIso A B ∘ idToIso* ∘ shuffle) x - ≡⟨ cong (λ φ → φ x) (cong (λ φ → φ ∘ idToIso* ∘ shuffle) (funExt lem)) ⟩ - (shuffle~ ∘ ℂ.idToIso A B ∘ idToIso* ∘ shuffle) x - ≡⟨ cong (λ φ → φ x) (cong (λ φ → shuffle~ ∘ φ ∘ shuffle) recto-verso) ⟩ - (shuffle~ ∘ shuffle) x - ≡⟨⟩ - x ∎) - ) - - isCategory : IsCategory opRaw - IsCategory.isPreCategory isCategory = isPreCategory - IsCategory.univalent isCategory - = univalenceFromIsomorphism (isoToId* , inv) - - opposite : Category ℓa ℓb - Category.raw opposite = opRaw - Category.isCategory opposite = isCategory - - -- As demonstrated here a side-effect of having no-eta-equality on constructors - -- means that we need to pick things apart to show that things are indeed - -- definitionally equal. I.e; a thing that would normally be provable in one - -- line now takes 13!! Admittedly it's a simple proof. - module _ {ℂ : Category ℓa ℓb} where - open Category ℂ - private - -- Since they really are definitionally equal we just need to pick apart - -- the data-type. - rawInv : Category.raw (opposite (opposite ℂ)) ≡ raw - RawCategory.Object (rawInv _) = Object - RawCategory.Arrow (rawInv _) = Arrow - RawCategory.identity (rawInv _) = identity - RawCategory._<<<_ (rawInv _) = _<<<_ - - oppositeIsInvolution : opposite (opposite ℂ) ≡ ℂ - oppositeIsInvolution = Category≡ rawInv - -open Opposite public diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda index 4856668..41d10e2 100644 --- a/src/Cat/Category/Product.agda +++ b/src/Cat/Category/Product.agda @@ -55,286 +55,122 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where × ℂ [ g ∘ snd ] ] -module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object ℂ} where +module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} + (let module ℂ = Category ℂ) {𝒜 ℬ : ℂ.Object} where private - open Category ℂ - module _ (raw : RawProduct ℂ A B) where - module _ (x y : IsProduct ℂ A B raw) where - private - module x = IsProduct x - module y = IsProduct y + module _ (raw : RawProduct ℂ 𝒜 ℬ) where + private + open Category ℂ hiding (raw) + module _ (x y : IsProduct ℂ 𝒜 ℬ raw) where + private + module x = IsProduct x + module y = IsProduct y - module _ {X : Object} (f : ℂ [ X , A ]) (g : ℂ [ X , B ]) where - module _ (f×g : Arrow X y.object) where - help : isProp (∀{y} → (ℂ [ y.fst ∘ y ] ≡ f) P.× (ℂ [ y.snd ∘ y ] ≡ g) → f×g ≡ y) - help = propPiImpl (λ _ → propPi (λ _ → arrowsAreSets _ _)) + module _ {X : Object} (f : ℂ [ X , 𝒜 ]) (g : ℂ [ X , ℬ ]) where + module _ (f×g : Arrow X y.object) where + help : isProp (∀{y} → (ℂ [ y.fst ∘ y ] ≡ f) P.× (ℂ [ y.snd ∘ y ] ≡ g) → f×g ≡ y) + help = propPiImpl (λ _ → propPi (λ _ → arrowsAreSets _ _)) - res = ∃-unique (x.ump f g) (y.ump f g) + res = ∃-unique (x.ump f g) (y.ump f g) - prodAux : x.ump f g ≡ y.ump f g - prodAux = lemSig ((λ f×g → propSig (propSig (arrowsAreSets _ _) λ _ → arrowsAreSets _ _) (λ _ → help f×g))) _ _ res + prodAux : x.ump f g ≡ y.ump f g + prodAux = lemSig ((λ f×g → propSig (propSig (arrowsAreSets _ _) λ _ → arrowsAreSets _ _) (λ _ → help f×g))) _ _ res - propIsProduct' : x ≡ y - propIsProduct' i = record { ump = λ f g → prodAux f g i } + propIsProduct' : x ≡ y + propIsProduct' i = record { ump = λ f g → prodAux f g i } - propIsProduct : isProp (IsProduct ℂ A B raw) + propIsProduct : isProp (IsProduct ℂ 𝒜 ℬ raw) propIsProduct = propIsProduct' - Product≡ : {x y : Product ℂ A B} → (Product.raw x ≡ Product.raw y) → x ≡ y - Product≡ {x} {y} p i = record { raw = p i ; isProduct = q i } - where - q : (λ i → IsProduct ℂ A B (p i)) [ Product.isProduct x ≡ Product.isProduct y ] - q = lemPropF propIsProduct p + Product≡ : {x y : Product ℂ 𝒜 ℬ} → (Product.raw x ≡ Product.raw y) → x ≡ y + Product≡ {x} {y} p i = record { raw = p i ; isProduct = q i } + where + q : (λ i → IsProduct ℂ 𝒜 ℬ (p i)) [ Product.isProduct x ≡ Product.isProduct y ] + q = lemPropF propIsProduct p -module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} - (let module ℂ = Category ℂ) {𝒜 ℬ : ℂ.Object} where + open P + open import Cat.Categories.Span - open P + open Category (span ℂ 𝒜 ℬ) - module _ where - raw : RawCategory _ _ - raw = record - { Object = Σ[ X ∈ ℂ.Object ] ℂ.Arrow X 𝒜 × ℂ.Arrow X ℬ - ; Arrow = λ{ (A , a0 , a1) (B , b0 , b1) - → Σ[ f ∈ ℂ.Arrow A B ] - ℂ [ b0 ∘ f ] ≡ a0 - × ℂ [ b1 ∘ f ] ≡ a1 - } - ; identity = λ{ {X , f , g} → ℂ.identity {X} , ℂ.rightIdentity , ℂ.rightIdentity} - ; _<<<_ = λ { {_ , a0 , a1} {_ , b0 , b1} {_ , c0 , c1} (f , f0 , f1) (g , g0 , g1) - → (f ℂ.<<< g) - , (begin - ℂ [ c0 ∘ ℂ [ f ∘ g ] ] ≡⟨ ℂ.isAssociative ⟩ - ℂ [ ℂ [ c0 ∘ f ] ∘ g ] ≡⟨ cong (λ φ → ℂ [ φ ∘ g ]) f0 ⟩ - ℂ [ b0 ∘ g ] ≡⟨ g0 ⟩ - a0 ∎ - ) - , (begin - ℂ [ c1 ∘ ℂ [ f ∘ g ] ] ≡⟨ ℂ.isAssociative ⟩ - ℂ [ ℂ [ c1 ∘ f ] ∘ g ] ≡⟨ cong (λ φ → ℂ [ φ ∘ g ]) f1 ⟩ - ℂ [ b1 ∘ g ] ≡⟨ g1 ⟩ - a1 ∎ - ) - } - } - - module _ where - open RawCategory raw - - propEqs : ∀ {X' : Object}{Y' : Object} (let X , xa , xb = X') (let Y , ya , yb = Y') - → (xy : ℂ.Arrow X Y) → isProp (ℂ [ ya ∘ xy ] ≡ xa × ℂ [ yb ∘ xy ] ≡ xb) - propEqs xs = propSig (ℂ.arrowsAreSets _ _) (\ _ → ℂ.arrowsAreSets _ _) - - arrowEq : {X Y : Object} {f g : Arrow X Y} → fst f ≡ fst g → f ≡ g - arrowEq {X} {Y} {f} {g} p = λ i → p i , lemPropF propEqs p {snd f} {snd g} i - - private - isAssociative : IsAssociative - isAssociative {f = f , f0 , f1} {g , g0 , g1} {h , h0 , h1} = arrowEq ℂ.isAssociative - - isIdentity : IsIdentity identity - isIdentity {AA@(A , a0 , a1)} {BB@(B , b0 , b1)} {f , f0 , f1} = arrowEq ℂ.leftIdentity , arrowEq ℂ.rightIdentity - - arrowsAreSets : ArrowsAreSets - arrowsAreSets {X , x0 , x1} {Y , y0 , y1} - = sigPresSet ℂ.arrowsAreSets λ a → propSet (propEqs _) - - isPreCat : IsPreCategory raw - IsPreCategory.isAssociative isPreCat = isAssociative - IsPreCategory.isIdentity isPreCat = isIdentity - IsPreCategory.arrowsAreSets isPreCat = arrowsAreSets - - open IsPreCategory isPreCat - - module _ {𝕏 𝕐 : Object} where - open Σ 𝕏 renaming (fst to X ; snd to x) - open Σ x renaming (fst to xa ; snd to xb) - open Σ 𝕐 renaming (fst to Y ; snd to y) - open Σ y renaming (fst to ya ; snd to yb) - open import Cat.Equivalence using (composeIso) renaming (_≅_ to _≅_) - step0 - : ((X , xa , xb) ≡ (Y , ya , yb)) - ≅ (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya) × (PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb)) - step0 - = (λ p → cong fst p , cong-d (fst ∘ snd) p , cong-d (snd ∘ snd) p) - -- , (λ x → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i)) - , (λ{ (p , q , r) → Σ≡ p λ i → q i , r i}) - , funExt (λ{ p → refl}) - , funExt (λ{ (p , q , r) → refl}) - - step1 - : (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya) × (PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb)) - ≅ Σ (X ℂ.≊ Y) (λ iso - → let p = ℂ.isoToId iso - in - ( PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya) - × PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb - ) - step1 - = symIso - (isoSigFst - {A = (X ℂ.≊ Y)} - {B = (X ≡ Y)} - (ℂ.groupoidObject _ _) - {Q = \ p → (PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya) × (PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb)} - ℂ.isoToId - (symIso (_ , ℂ.asTypeIso {X} {Y}) .snd) - ) - - step2 - : Σ (X ℂ.≊ Y) (λ iso - → let p = ℂ.isoToId iso - in - ( PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya) - × PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb - ) - ≅ ((X , xa , xb) ≊ (Y , ya , yb)) - step2 - = ( λ{ (iso@(f , f~ , inv-f) , p , q) - → ( f , sym (ℂ.domain-twist-sym iso p) , sym (ℂ.domain-twist-sym iso q)) - , ( f~ , sym (ℂ.domain-twist iso p) , sym (ℂ.domain-twist iso q)) - , arrowEq (fst inv-f) - , arrowEq (snd inv-f) - } - ) - , (λ{ (f , f~ , inv-f , inv-f~) → - let - iso : X ℂ.≊ Y - iso = fst f , fst f~ , cong fst inv-f , cong fst inv-f~ - p : X ≡ Y - p = ℂ.isoToId iso - pA : ℂ.Arrow X 𝒜 ≡ ℂ.Arrow Y 𝒜 - pA = cong (λ x → ℂ.Arrow x 𝒜) p - pB : ℂ.Arrow X ℬ ≡ ℂ.Arrow Y ℬ - pB = cong (λ x → ℂ.Arrow x ℬ) p - k0 = begin - coe pB xb ≡⟨ ℂ.coe-dom iso ⟩ - xb ℂ.<<< fst f~ ≡⟨ snd (snd f~) ⟩ - yb ∎ - k1 = begin - coe pA xa ≡⟨ ℂ.coe-dom iso ⟩ - xa ℂ.<<< fst f~ ≡⟨ fst (snd f~) ⟩ - ya ∎ - in iso , coe-lem-inv k1 , coe-lem-inv k0}) - , funExt (λ x → lemSig - (λ x → propSig prop0 (λ _ → prop1)) - _ _ - (Σ≡ refl (ℂ.propIsomorphism _ _ _))) - , funExt (λ{ (f , _) → lemSig propIsomorphism _ _ (Σ≡ refl (propEqs _ _ _))}) - where - prop0 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) 𝒜) xa ya) - prop0 {x} = pathJ (λ y p → ∀ x → isProp (PathP (λ i → ℂ.Arrow (p i) 𝒜) xa x)) (λ x → ℂ.arrowsAreSets _ _) Y (ℂ.isoToId x) ya - prop1 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) ℬ) xb yb) - prop1 {x} = pathJ (λ y p → ∀ x → isProp (PathP (λ i → ℂ.Arrow (p i) ℬ) xb x)) (λ x → ℂ.arrowsAreSets _ _) Y (ℂ.isoToId x) yb - -- One thing to watch out for here is that the isomorphisms going forwards - -- must compose to give idToIso - iso - : ((X , xa , xb) ≡ (Y , ya , yb)) - ≅ ((X , xa , xb) ≊ (Y , ya , yb)) - iso = step0 ⊙ step1 ⊙ step2 + lemma : Terminal ≃ Product ℂ 𝒜 ℬ + lemma = fromIsomorphism Terminal (Product ℂ 𝒜 ℬ) (f , g , inv) + where + f : Terminal → Product ℂ 𝒜 ℬ + f ((X , x0 , x1) , uniq) = p where - infixl 5 _⊙_ - _⊙_ = composeIso - equiv1 - : ((X , xa , xb) ≡ (Y , ya , yb)) - ≃ ((X , xa , xb) ≊ (Y , ya , yb)) - equiv1 = _ , fromIso _ _ (snd iso) - - univalent : Univalent - univalent = univalenceFrom≃ equiv1 - - isCat : IsCategory raw - IsCategory.isPreCategory isCat = isPreCat - IsCategory.univalent isCat = univalent - - cat : Category _ _ - cat = record - { raw = raw - ; isCategory = isCat - } - - open Category cat - - lemma : Terminal ≃ Product ℂ 𝒜 ℬ - lemma = fromIsomorphism Terminal (Product ℂ 𝒜 ℬ) (f , g , inv) - -- C-x 8 RET MATHEMATICAL BOLD SCRIPT CAPITAL A - -- 𝒜 - where - f : Terminal → Product ℂ 𝒜 ℬ - f ((X , x0 , x1) , uniq) = p - where - rawP : RawProduct ℂ 𝒜 ℬ - rawP = record - { object = X - ; fst = x0 - ; snd = x1 - } - -- open RawProduct rawP renaming (fst to x0 ; snd to x1) - module _ {Y : ℂ.Object} (p0 : ℂ [ Y , 𝒜 ]) (p1 : ℂ [ Y , ℬ ]) where - uy : isContr (Arrow (Y , p0 , p1) (X , x0 , x1)) - uy = uniq {Y , p0 , p1} - open Σ uy renaming (fst to Y→X ; snd to contractible) - open Σ Y→X renaming (fst to p0×p1 ; snd to cond) - ump : ∃![ f×g ] (ℂ [ x0 ∘ f×g ] ≡ p0 P.× ℂ [ x1 ∘ f×g ] ≡ p1) - ump = p0×p1 , cond , λ {f} cond-f → cong fst (contractible (f , cond-f)) - isP : IsProduct ℂ 𝒜 ℬ rawP - isP = record { ump = ump } - p : Product ℂ 𝒜 ℬ - p = record - { raw = rawP - ; isProduct = isP - } - g : Product ℂ 𝒜 ℬ → Terminal - g p = 𝒳 , t - where - open Product p renaming (object to X ; fst to x₀ ; snd to x₁) using () - module p = Product p - module isp = IsProduct p.isProduct - 𝒳 : Object - 𝒳 = X , x₀ , x₁ - module _ {𝒴 : Object} where - open Σ 𝒴 renaming (fst to Y) - open Σ (snd 𝒴) renaming (fst to y₀ ; snd to y₁) - ump = p.ump y₀ y₁ - open Σ ump renaming (fst to f') - open Σ (snd ump) renaming (fst to f'-cond) - 𝒻 : Arrow 𝒴 𝒳 - 𝒻 = f' , f'-cond - contractible : (f : Arrow 𝒴 𝒳) → 𝒻 ≡ f - contractible ff@(f , f-cond) = res - where - k : f' ≡ f - k = snd (snd ump) f-cond - prp : (a : ℂ.Arrow Y X) → isProp - ( (ℂ [ x₀ ∘ a ] ≡ y₀) - × (ℂ [ x₁ ∘ a ] ≡ y₁) - ) - prp f f0 f1 = Σ≡ - (ℂ.arrowsAreSets _ _ (fst f0) (fst f1)) - (ℂ.arrowsAreSets _ _ (snd f0) (snd f1)) - h : - ( λ i - → ℂ [ x₀ ∘ k i ] ≡ y₀ - × ℂ [ x₁ ∘ k i ] ≡ y₁ - ) [ f'-cond ≡ f-cond ] - h = lemPropF prp k - res : (f' , f'-cond) ≡ (f , f-cond) - res = Σ≡ k h - t : IsTerminal 𝒳 - t {𝒴} = 𝒻 , contractible - ve-re : ∀ x → g (f x) ≡ x - ve-re x = Propositionality.propTerminal _ _ - re-ve : ∀ p → f (g p) ≡ p - re-ve p = Product≡ e - where - module p = Product p - -- RawProduct does not have eta-equality. - e : Product.raw (f (g p)) ≡ Product.raw p - RawProduct.object (e i) = p.object - RawProduct.fst (e i) = p.fst - RawProduct.snd (e i) = p.snd - inv : AreInverses f g - inv = funExt ve-re , funExt re-ve + rawP : RawProduct ℂ 𝒜 ℬ + rawP = record + { object = X + ; fst = x0 + ; snd = x1 + } + -- open RawProduct rawP renaming (fst to x0 ; snd to x1) + module _ {Y : ℂ.Object} (p0 : ℂ [ Y , 𝒜 ]) (p1 : ℂ [ Y , ℬ ]) where + uy : isContr (Arrow (Y , p0 , p1) (X , x0 , x1)) + uy = uniq {Y , p0 , p1} + open Σ uy renaming (fst to Y→X ; snd to contractible) + open Σ Y→X renaming (fst to p0×p1 ; snd to cond) + ump : ∃![ f×g ] (ℂ [ x0 ∘ f×g ] ≡ p0 P.× ℂ [ x1 ∘ f×g ] ≡ p1) + ump = p0×p1 , cond , λ {f} cond-f → cong fst (contractible (f , cond-f)) + isP : IsProduct ℂ 𝒜 ℬ rawP + isP = record { ump = ump } + p : Product ℂ 𝒜 ℬ + p = record + { raw = rawP + ; isProduct = isP + } + g : Product ℂ 𝒜 ℬ → Terminal + g p = 𝒳 , t + where + open Product p renaming (object to X ; fst to x₀ ; snd to x₁) using () + module p = Product p + module isp = IsProduct p.isProduct + 𝒳 : Object + 𝒳 = X , x₀ , x₁ + module _ {𝒴 : Object} where + open Σ 𝒴 renaming (fst to Y) + open Σ (snd 𝒴) renaming (fst to y₀ ; snd to y₁) + ump = p.ump y₀ y₁ + open Σ ump renaming (fst to f') + open Σ (snd ump) renaming (fst to f'-cond) + 𝒻 : Arrow 𝒴 𝒳 + 𝒻 = f' , f'-cond + contractible : (f : Arrow 𝒴 𝒳) → 𝒻 ≡ f + contractible ff@(f , f-cond) = res + where + k : f' ≡ f + k = snd (snd ump) f-cond + prp : (a : ℂ.Arrow Y X) → isProp + ( (ℂ [ x₀ ∘ a ] ≡ y₀) + × (ℂ [ x₁ ∘ a ] ≡ y₁) + ) + prp f f0 f1 = Σ≡ + (ℂ.arrowsAreSets _ _ (fst f0) (fst f1)) + (ℂ.arrowsAreSets _ _ (snd f0) (snd f1)) + h : + ( λ i + → ℂ [ x₀ ∘ k i ] ≡ y₀ + × ℂ [ x₁ ∘ k i ] ≡ y₁ + ) [ f'-cond ≡ f-cond ] + h = lemPropF prp k + res : (f' , f'-cond) ≡ (f , f-cond) + res = Σ≡ k h + t : IsTerminal 𝒳 + t {𝒴} = 𝒻 , contractible + ve-re : ∀ x → g (f x) ≡ x + ve-re x = Propositionality.propTerminal _ _ + re-ve : ∀ p → f (g p) ≡ p + re-ve p = Product≡ e + where + module p = Product p + -- RawProduct does not have eta-equality. + e : Product.raw (f (g p)) ≡ Product.raw p + RawProduct.object (e i) = p.object + RawProduct.fst (e i) = p.fst + RawProduct.snd (e i) = p.snd + inv : AreInverses f g + inv = funExt ve-re , funExt re-ve propProduct : isProp (Product ℂ 𝒜 ℬ) propProduct = equivPreservesNType {n = ⟨-1⟩} lemma Propositionality.propTerminal @@ -348,10 +184,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object module y = HasProducts y productEq : x.product ≡ y.product - productEq = funExt λ A → funExt λ B → Try0.propProduct _ _ + productEq = funExt λ A → funExt λ B → propProduct _ _ propHasProducts : isProp (HasProducts ℂ) propHasProducts x y i = record { product = productEq x y i } - -fmap≡ : {A : Set} {a0 a1 : A} {B : Set} → (f : A → B) → Path a0 a1 → Path (f a0) (f a1) -fmap≡ = cong diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda index c02274b..1fbe990 100644 --- a/src/Cat/Category/Yoneda.agda +++ b/src/Cat/Category/Yoneda.agda @@ -9,9 +9,9 @@ open import Cat.Category.Functor open import Cat.Category.NaturalTransformation renaming (module Properties to F) using () - -open import Cat.Categories.Fun using (module Fun) +open import Cat.Categories.Opposite open import Cat.Categories.Sets hiding (presheaf) +open import Cat.Categories.Fun using (module Fun) -- There is no (small) category of categories. So we won't use _⇑_ from -- `HasExponential`