From b61749bb911a99b28070dae97a1b97582664e77a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 8 Mar 2018 01:09:40 +0100 Subject: [PATCH] Fixup some todo-notes --- BACKLOG.md | 4 ++++ src/Cat/Categories/Cat.agda | 5 ++--- src/Cat/Category.agda | 20 +++++++++++++------- src/Cat/Category/Functor.agda | 2 +- src/Cat/Category/Monad.agda | 2 +- 5 files changed, 21 insertions(+), 12 deletions(-) diff --git a/BACKLOG.md b/BACKLOG.md index 64ea62f..3eec938 100644 --- a/BACKLOG.md +++ b/BACKLOG.md @@ -15,6 +15,10 @@ Prove univalence for the category of * sets * functors and natural transformations +Prove: + * `isProp (Product ...)` + * `isProp (HasProducts ...)` + * Functor ✓ * Applicative Functor ✗ * Lax monoidal functor ✗ diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index ce493b6..5e442b3 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -46,9 +46,8 @@ module _ (ℓ ℓ' : Level) where open RawCategory RawCat isAssociative : IsAssociative isAssociative {f = F} {G} {H} = assc {F = F} {G = G} {H = H} - -- TODO: Rename `ident'` to `ident` after changing how names are exposed in Functor. - ident' : IsIdentity identity - ident' = ident-r , ident-l + ident : IsIdentity identity + ident = ident-r , ident-l -- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors, -- however, form a groupoid! Therefore there is no (1-)category of -- categories. There does, however, exist a 2-category of 1-categories. diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 62a7221..e547a81 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -24,9 +24,6 @@ -- ------ -- -- Propositionality for all laws about the category. --- --- TODO: An equality principle for categories that focuses on the pure data-part. --- {-# OPTIONS --allow-unsolved-metas --cubical #-} module Cat.Category where @@ -91,7 +88,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where -- | Laws about the data - -- TODO: It seems counter-intuitive that the normal-form is on the + -- FIXME It seems counter-intuitive that the normal-form is on the -- right-hand-side. IsAssociative : Set (ℓa ⊔ ℓb) IsAssociative = ∀ {A B C D} {f : Arrow A B} {g : Arrow B C} {h : Arrow C D} @@ -286,6 +283,17 @@ record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where open IsCategory isCategory public +Category≡ : {ℓa ℓb : Level} {ℂ 𝔻 : Category ℓa ℓb} → Category.raw ℂ ≡ Category.raw 𝔻 → ℂ ≡ 𝔻 +Category≡ {ℂ = ℂ} {𝔻} eq i = record + { raw = eq i + ; isCategory = isCategoryEq i + } + where + open Category + module ℂ = Category ℂ + isCategoryEq : (λ i → IsCategory (eq i)) [ isCategory ℂ ≡ isCategory 𝔻 ] + isCategoryEq = {!!} + -- | Syntax for arrows- and composition in a given category. module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where open Category ℂ @@ -353,9 +361,7 @@ module Opposite {ℓa ℓb : Level} where RawCategory.𝟙 (rawInv _) = 𝟙 RawCategory._∘_ (rawInv _) = _∘_ - -- TODO: Define and use Monad≡ oppositeIsInvolution : opposite (opposite ℂ) ≡ ℂ - Category.raw (oppositeIsInvolution i) = rawInv i - Category.isCategory (oppositeIsInvolution x) = {!!} + oppositeIsInvolution = Category≡ rawInv open Opposite public diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index d627539..6724dee 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -61,7 +61,7 @@ module _ {ℓc ℓc' ℓd ℓd'} record IsFunctor (F : RawFunctor) : 𝓤 where open RawFunctor F public field - -- TODO Really ought to be preserves identity or something like this. + -- FIXME Really ought to be preserves identity or something like this. isIdentity : IsIdentity isDistributive : IsDistributive diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index c0c42bf..6ce46bb 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -250,7 +250,7 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where fmap g ∘ fmap f ≡⟨⟩ bind (pure ∘ g) ∘ bind (pure ∘ f) ∎ - -- TODO: Naming! + -- FIXME Naming! R : EndoFunctor ℂ Functor.raw R = rawR Functor.isFunctor R = isFunctorR