diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda index 6b08717..3c7648c 100644 --- a/src/Cat/Categories/Rel.agda +++ b/src/Cat/Categories/Rel.agda @@ -1,7 +1,7 @@ {-# OPTIONS --cubical --allow-unsolved-metas #-} module Cat.Categories.Rel where -open import Cat.Prelude renaming (fst to fst ; snd to snd) +open import Cat.Prelude hiding (Rel) open import Function open import Cat.Category diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 09ac382..dfbbc17 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -120,6 +120,15 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where Univalent : Set (ℓa ⊔ ℓb) Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (idToIso A B) + import Cat.Equivalence as E + open E public using () renaming (Isomorphism to TypeIsomorphism) + open E using (module Equiv≃) + open Equiv≃ using (fromIso) + + univalenceFromIsomorphism : {A B : Object} + → TypeIsomorphism (idToIso A B) → isEquiv (A ≡ B) (A ≅ B) (idToIso A B) + univalenceFromIsomorphism = fromIso _ _ + -- A perhaps more readable version of univalence: Univalent≃ = {A B : Object} → (A ≡ B) ≃ (A ≅ B) @@ -244,6 +253,34 @@ record IsPreCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (ls res : (fx , cx) ≡ (fy , cy) res i = fp i , cp i + module _ where + private + trans≅ : Transitive _≅_ + trans≅ (f , f~ , f-inv) (g , g~ , g-inv) + = g ∘ f + , f~ ∘ g~ + , ( begin + (f~ ∘ g~) ∘ (g ∘ f) ≡⟨ isAssociative ⟩ + (f~ ∘ g~) ∘ g ∘ f ≡⟨ cong (λ φ → φ ∘ f) (sym isAssociative) ⟩ + f~ ∘ (g~ ∘ g) ∘ f ≡⟨ cong (λ φ → f~ ∘ φ ∘ f) (fst g-inv) ⟩ + f~ ∘ identity ∘ f ≡⟨ cong (λ φ → φ ∘ f) rightIdentity ⟩ + f~ ∘ f ≡⟨ fst f-inv ⟩ + identity ∎ + ) + , ( begin + g ∘ f ∘ (f~ ∘ g~) ≡⟨ isAssociative ⟩ + g ∘ f ∘ f~ ∘ g~ ≡⟨ cong (λ φ → φ ∘ g~) (sym isAssociative) ⟩ + g ∘ (f ∘ f~) ∘ g~ ≡⟨ cong (λ φ → g ∘ φ ∘ g~) (snd f-inv) ⟩ + g ∘ identity ∘ g~ ≡⟨ cong (λ φ → φ ∘ g~) rightIdentity ⟩ + g ∘ g~ ≡⟨ snd g-inv ⟩ + identity ∎ + ) + isPreorder : IsPreorder _≅_ + isPreorder = record { isEquivalence = equalityIsEquivalence ; reflexive = idToIso _ _ ; trans = trans≅ } + + preorder≅ : Preorder _ _ _ + preorder≅ = record { Carrier = Object ; _≈_ = _≡_ ; _∼_ = _≅_ ; isPreorder = isPreorder } + record PreCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where field raw : RawCategory ℓa ℓb diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index 5b3c657..387dc75 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -29,7 +29,7 @@ import Cat.Category.Monad.Kleisli open import Cat.Categories.Fun module Monoidal = Cat.Category.Monad.Monoidal -module Kleisli = Cat.Category.Monad.Kleisli +module Kleisli = Cat.Category.Monad.Kleisli -- | The monoidal- and kleisli presentation of monads are equivalent. module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where diff --git a/src/Cat/Category/Monoid.agda b/src/Cat/Category/Monoid.agda index 75eaa68..e813005 100644 --- a/src/Cat/Category/Monoid.agda +++ b/src/Cat/Category/Monoid.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --allow-unsolved-metas #-} module Cat.Category.Monoid where open import Agda.Primitive @@ -6,9 +7,10 @@ open import Cat.Category open import Cat.Category.Product open import Cat.Category.Functor import Cat.Categories.Cat as Cat +open import Cat.Prelude hiding (_×_ ; empty) -- TODO: Incorrect! -module _ (ℓa ℓb : Level) where +module _ {ℓa ℓb : Level} where private ℓ = lsuc (ℓa ⊔ ℓb) @@ -21,30 +23,34 @@ module _ (ℓa ℓb : Level) where _×_ : ∀ {ℓa ℓb} → Category ℓa ℓb → Category ℓa ℓb → Category ℓa ℓb ℂ × 𝔻 = Cat.CatProduct.object ℂ 𝔻 - record RawMonoidalCategory : Set ℓ where + record RawMonoidalCategory (ℂ : Category ℓa ℓb) : Set ℓ where + open Category ℂ public hiding (IsAssociative) field - category : Category ℓa ℓb - open Category category public - field - {{hasProducts}} : HasProducts category empty : Object -- aka. tensor product, monoidal product. - append : Functor (category × category) category - open HasProducts hasProducts public + append : Functor (ℂ × ℂ) ℂ - record MonoidalCategory : Set ℓ where + module F = Functor append + + _⊗_ = append + mappend = F.fmap + + IsAssociative : Set _ + IsAssociative = {A B : Object} → (f g h : Arrow A A) → mappend ({!mappend!} , {!mappend!}) ≡ mappend (f , mappend (g , h)) + + record MonoidalCategory (ℂ : Category ℓa ℓb) : Set ℓ where field - raw : RawMonoidalCategory + raw : RawMonoidalCategory ℂ open RawMonoidalCategory raw public -module _ {ℓa ℓb : Level} (ℂ : MonoidalCategory ℓa ℓb) where +module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) {monoidal : MonoidalCategory ℂ} {hasProducts : HasProducts ℂ} where private ℓ = ℓa ⊔ ℓb - open MonoidalCategory ℂ public + open MonoidalCategory monoidal public hiding (mappend) + open HasProducts hasProducts - record Monoid : Set ℓ where + record MonoidalObject (M : Object) : Set ℓ where field - carrier : Object - mempty : Arrow empty carrier - mappend : Arrow (carrier × carrier) carrier + mempty : Arrow empty M + mappend : Arrow (M × M) M diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda index ed49dac..9def8a2 100644 --- a/src/Cat/Category/Product.agda +++ b/src/Cat/Category/Product.agda @@ -123,46 +123,47 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} } module _ where - open RawCategory raw + private + 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 _ _) + 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 _ _) - isAssociative : IsAssociative - isAssociative {A'@(A , a0 , a1)} {B , _} {C , c0 , c1} {D'@(D , d0 , d1)} {ff@(f , f0 , f1)} {gg@(g , g0 , g1)} {hh@(h , h0 , h1)} i - = s0 i , lemPropF propEqs s0 {P.snd l} {P.snd r} i - where - l = hh ∘ (gg ∘ ff) - r = hh ∘ gg ∘ ff - -- s0 : h ℂ.∘ (g ℂ.∘ f) ≡ h ℂ.∘ g ℂ.∘ f - s0 : fst l ≡ fst r - s0 = ℂ.isAssociative {f = f} {g} {h} - - - isIdentity : IsIdentity identity - isIdentity {AA@(A , a0 , a1)} {BB@(B , b0 , b1)} {f , f0 , f1} = leftIdentity , rightIdentity - where - leftIdentity : identity ∘ (f , f0 , f1) ≡ (f , f0 , f1) - leftIdentity i = l i , lemPropF propEqs l {snd L} {snd R} i + isAssociative : IsAssociative + isAssociative {A'@(A , a0 , a1)} {B , _} {C , c0 , c1} {D'@(D , d0 , d1)} {ff@(f , f0 , f1)} {gg@(g , g0 , g1)} {hh@(h , h0 , h1)} i + = s0 i , lemPropF propEqs s0 {P.snd l} {P.snd r} i where - L = identity ∘ (f , f0 , f1) - R : Arrow AA BB - R = f , f0 , f1 - l : fst L ≡ fst R - l = ℂ.leftIdentity - rightIdentity : (f , f0 , f1) ∘ identity ≡ (f , f0 , f1) - rightIdentity i = l i , lemPropF propEqs l {snd L} {snd R} i - where - L = (f , f0 , f1) ∘ identity - R : Arrow AA BB - R = (f , f0 , f1) - l : ℂ [ f ∘ ℂ.identity ] ≡ f - l = ℂ.rightIdentity + l = hh ∘ (gg ∘ ff) + r = hh ∘ gg ∘ ff + -- s0 : h ℂ.∘ (g ℂ.∘ f) ≡ h ℂ.∘ g ℂ.∘ f + s0 : fst l ≡ fst r + s0 = ℂ.isAssociative {f = f} {g} {h} - arrowsAreSets : ArrowsAreSets - arrowsAreSets {X , x0 , x1} {Y , y0 , y1} - = sigPresNType {n = ⟨0⟩} ℂ.arrowsAreSets λ a → propSet (propEqs _) + + isIdentity : IsIdentity identity + isIdentity {AA@(A , a0 , a1)} {BB@(B , b0 , b1)} {f , f0 , f1} = leftIdentity , rightIdentity + where + leftIdentity : identity ∘ (f , f0 , f1) ≡ (f , f0 , f1) + leftIdentity i = l i , lemPropF propEqs l {snd L} {snd R} i + where + L = identity ∘ (f , f0 , f1) + R : Arrow AA BB + R = f , f0 , f1 + l : fst L ≡ fst R + l = ℂ.leftIdentity + rightIdentity : (f , f0 , f1) ∘ identity ≡ (f , f0 , f1) + rightIdentity i = l i , lemPropF propEqs l {snd L} {snd R} i + where + L = (f , f0 , f1) ∘ identity + R : Arrow AA BB + R = (f , f0 , f1) + l : ℂ [ f ∘ ℂ.identity ] ≡ f + l = ℂ.rightIdentity + + arrowsAreSets : ArrowsAreSets + arrowsAreSets {X , x0 , x1} {Y , y0 , y1} + = sigPresNType {n = ⟨0⟩} ℂ.arrowsAreSets λ a → propSet (propEqs _) isPreCat : IsPreCategory raw IsPreCategory.isAssociative isPreCat = isAssociative @@ -171,69 +172,106 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} open IsPreCategory isPreCat - -- module _ (X : Object) where - -- center : Σ Object (X ≅_) - -- center = X , idIso X - - -- module _ (y : Σ Object (X ≅_)) where - -- open Σ y renaming (fst to Y ; snd to X≅Y) - - -- contractible : (X , idIso X) ≡ (Y , X≅Y) - -- contractible = {!!} - - -- univalent[Contr] : isContr (Σ Object (X ≅_)) - -- univalent[Contr] = center , contractible - -- module _ (y : Σ Object (X ≡_)) where - -- open Σ y renaming (fst to Y ; snd to p) - -- a0 : X ≡ Y - -- a0 = {!!} - -- a1 : PathP (λ i → X ≡ a0 i) refl p - -- a1 = {!!} - -- where - -- P : (Z : Object) → X ≡ Z → Set _ - -- P Z p = PathP (λ i → X ≡ Z) - - -- alt' : (X , refl) ≡ y - -- alt' i = a0 i , a1 i - -- alt : isContr (Σ Object (X ≡_)) - -- alt = (X , refl) , alt' - univalent : Univalent - univalent {X , x} {Y , y} = {!res!} + univalent {(X , xa , xb)} {(Y , ya , yb)} = univalenceFromIsomorphism res where - open import Cat.Equivalence as E hiding (_≅_) - open import Cubical.Univalence - module _ (c : (X , x) ≅ (Y , y)) where - -- module _ (c : _ ≅ _) where - open Σ c renaming (fst to f_c ; snd to inv_c) - open Σ inv_c renaming (fst to g_c ; snd to ainv_c) - open Σ ainv_c renaming (fst to left ; snd to right) - c0 : X ℂ.≅ Y - c0 = fst f_c , fst g_c , (λ i → fst (left i)) , (λ i → fst (right i)) - f0 : X ≡ Y - f0 = ℂ.iso-to-id c0 - module _ {A : ℂ.Object} (α : ℂ.Arrow X A) where - coedom : ℂ.Arrow Y A - coedom = coe (λ i → ℂ.Arrow (f0 i) A) α - coex : ℂ.Arrow Y A × ℂ.Arrow Y B - coex = coe (λ i → ℂ.Arrow (f0 i) A × ℂ.Arrow (f0 i) B) x - f1 : PathP (λ i → ℂ.Arrow (f0 i) A × ℂ.Arrow (f0 i) B) x coex - f1 = {!sym!} - f2 : coex ≡ y - f2 = {!!} - f : (X , x) ≡ (Y , y) - f i = f0 i , {!f1 i!} - prp : isSet (ℂ.Object × ℂ.Arrow Y A × ℂ.Arrow Y B) - prp = setSig {sA = {!!}} {(λ _ → setSig {sA = ℂ.arrowsAreSets} {λ _ → ℂ.arrowsAreSets})} - ve-re : (p : (X , x) ≡ (Y , y)) → f (idToIso _ _ p) ≡ p - -- ve-re p i j = {!ℂ.arrowsAreSets!} , ℂ.arrowsAreSets _ _ (let k = fst (snd (p i)) in {!!}) {!!} {!!} {!!} , {!!} - ve-re p = let k = prp {!!} {!!} {!!} {!p!} in {!!} - re-ve : (iso : (X , x) ≅ (Y , y)) → idToIso _ _ (f iso) ≡ iso - re-ve = {!!} - iso : E.Isomorphism (idToIso (X , x) (Y , y)) - iso = f , record { verso-recto = funExt ve-re ; recto-verso = funExt re-ve } - res : isEquiv ((X , x) ≡ (Y , y)) ((X , x) ≅ (Y , y)) (idToIso (X , x) (Y , y)) - res = Equiv≃.fromIso _ _ iso + open import Cat.Equivalence using (composeIso) renaming (_≅_ to _≈_) + -- open import Relation.Binary.PreorderReasoning (Cat.Equivalence.preorder≅ {!!}) using () + -- renaming + -- ( _∼⟨_⟩_ to _≈⟨_⟩_ + -- ; begin_ to begin!_ + -- ; _∎ to _∎! ) + -- lawl + -- : ((X , xa , xb) ≡ (Y , ya , yb)) + -- ≈ (Σ[ iso ∈ (X ℂ.≅ Y) ] let p = ℂ.iso-to-id iso in (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb)) + -- lawl = {!begin! ? ≈⟨ ? ⟩ ? ∎!!} + -- Problem with the above approach: Preorders only work for heterogeneous equaluties. + + -- (X , xa , xb) ≡ (Y , ya , yb) + -- ≅ + -- Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb) + -- ≅ + -- Σ (X ℂ.≅ Y) (λ iso + -- → let p = ℂ.iso-to-id iso + -- in + -- ( PathP (λ i → ℂ.Arrow (p i) A) xa ya) + -- × PathP (λ i → ℂ.Arrow (p i) B) xb yb + -- ) + -- ≅ + -- (X , xa , xb) ≅ (Y , ya , yb) + step0 + : ((X , xa , xb) ≡ (Y , ya , yb)) + ≈ (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb)) + step0 + = (λ p → (λ i → fst (p i)) , (λ i → fst (snd (p i))) , (λ i → snd (snd (p i)))) + , (λ x → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i)) + , record + { verso-recto = {!!} + ; recto-verso = {!!} + } + step1 + : (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb)) + ≈ Σ (X ℂ.≅ Y) (λ iso + → let p = ℂ.iso-to-id iso + in + ( PathP (λ i → ℂ.Arrow (p i) A) xa ya) + × PathP (λ i → ℂ.Arrow (p i) B) xb yb + ) + step1 + = (λ{ (p , x) → (ℂ.idToIso _ _ p) , {!snd x!}}) + -- Goal is: + -- + -- φ x + -- + -- where `x` is + -- + -- ℂ.iso-to-id (ℂ.idToIso _ _ p) + -- + -- I have `φ p` in scope, but surely `p` and `x` are the same - though + -- perhaps not definitonally. + , (λ{ (iso , x) → ℂ.iso-to-id iso , x}) + , record { verso-recto = {!!} ; recto-verso = {!!} } + lemA : {A B : Object} {f g : Arrow A B} → fst f ≡ fst g → f ≡ g + lemA {A} {B} {f = f} {g} p i = p i , h i + where + h : PathP (λ i → + (ℂ [ fst (snd B) ∘ p i ]) ≡ fst (snd A) × + (ℂ [ snd (snd B) ∘ p i ]) ≡ snd (snd A) + ) (snd f) (snd g) + h = lemPropF (λ a → propSig + (ℂ.arrowsAreSets (ℂ [ fst (snd B) ∘ a ]) (fst (snd A))) + λ _ → ℂ.arrowsAreSets (ℂ [ snd (snd B) ∘ a ]) (snd (snd A))) + p + step2 + : Σ (X ℂ.≅ Y) (λ iso + → let p = ℂ.iso-to-id iso + in + ( PathP (λ i → ℂ.Arrow (p i) A) xa ya) + × PathP (λ i → ℂ.Arrow (p i) B) xb yb + ) + ≈ ((X , xa , xb) ≅ (Y , ya , yb)) + step2 + = ( λ{ ((f , f~ , inv-f) , x) + → ( f , {!!}) + , ( (f~ , {!!}) + , lemA {!!} + , lemA {!!} + ) + } + ) + , (λ x → {!!}) + , {!!} + -- 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 + res : TypeIsomorphism (idToIso (X , xa , xb) (Y , ya , yb)) + res = {!snd iso!} isCat : IsCategory raw IsCategory.isPreCategory isCat = isPreCat @@ -346,3 +384,6 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object 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/Equivalence.agda b/src/Cat/Equivalence.agda index 7d976af..a7386b1 100644 --- a/src/Cat/Equivalence.agda +++ b/src/Cat/Equivalence.agda @@ -7,7 +7,7 @@ open import Cubical.PathPrelude hiding (inverse ; _≃_) open import Cubical.PathPrelude using (isEquiv ; isContr ; fiber) public open import Cubical.GradLemma -open import Cat.Prelude using (lemPropF ; setPi ; lemSig ; propSet) +open import Cat.Prelude using (lemPropF ; setPi ; lemSig ; propSet ; Preorder ; equalityIsEquivalence) module _ {ℓa ℓb : Level} where private @@ -278,6 +278,8 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where a' = Equiv≃.toIso A B a b' = Equiv≃.toIso B C b + composeIso : {ℓc : Level} {C : Set ℓc} → (A ≅ B) → (B ≅ C) → A ≅ C + composeIso {C = C} (f , iso-f) (g , iso-g) = g ∘ f , composeIsomorphism iso-f iso-g -- Gives the quasi inverse from an equivalence. module Equivalence (e : A ≃ B) where @@ -288,9 +290,6 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where open AreInverses (snd iso) public - composeIso : {ℓc : Level} {C : Set ℓc} → (B ≅ C) → A ≅ C - composeIso {C = C} (g , iso-g) = g ∘ obverse , composeIsomorphism iso iso-g - compose : {ℓc : Level} {C : Set ℓc} → (B ≃ C) → A ≃ C compose (f , isEquiv) = f ∘ obverse , composeIsEquiv (snd e) isEquiv @@ -308,6 +307,23 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where where module B≃A = Equiv≃ B A +preorder≅ : (ℓ : Level) → Preorder _ _ _ +preorder≅ ℓ = record + { Carrier = Set ℓ ; _≈_ = _≡_ ; _∼_ = _≅_ + ; isPreorder = record + { isEquivalence = equalityIsEquivalence + ; reflexive = λ p + → coe p + , coe (sym p) + -- I believe I stashed the proof of this somewhere. + , record + { verso-recto = {!refl!} + ; recto-verso = {!!} + } + ; trans = composeIso + } + } + module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where open import Cubical.PathPrelude renaming (_≃_ to _≃η_) open import Cubical.Univalence using (_≃_) diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda index e18cb72..a01dc25 100644 --- a/src/Cat/Prelude.agda +++ b/src/Cat/Prelude.agda @@ -71,3 +71,17 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb} {a b : Σ A B} Σ≡ : a ≡ b fst (Σ≡ i) = fst≡ i snd (Σ≡ i) = snd≡ i + +import Relation.Binary +open Relation.Binary public using (Preorder ; Transitive ; IsEquivalence ; Rel) + +equalityIsEquivalence : {ℓ : Level} {A : Set ℓ} → IsEquivalence {A = A} _≡_ +IsEquivalence.refl equalityIsEquivalence = refl +IsEquivalence.sym equalityIsEquivalence = sym +IsEquivalence.trans equalityIsEquivalence = trans + +IsPreorder + : {a ℓ : Level} {A : Set a} + → (_∼_ : Rel A ℓ) -- The relation. + → Set _ +IsPreorder _~_ = Relation.Binary.IsPreorder _≡_ _~_