From ef688202a2390b2410e06ac17b76e7b80b71b7a2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Mar 2018 13:55:03 +0100 Subject: [PATCH] Move identity functor laws to functor module... and make progress on univalence in the functor category --- src/Cat/Categories/Cat.agda | 24 +----- src/Cat/Categories/Fun.agda | 93 +++++++++++++++++---- src/Cat/Category/Functor.agda | 84 +++++++++++++------ src/Cat/Category/Monad.agda | 4 +- src/Cat/Category/Monad/Kleisli.agda | 2 +- src/Cat/Category/Monad/Monoidal.agda | 6 +- src/Cat/Category/Monad/Voevodsky.agda | 4 +- src/Cat/Category/NaturalTransformation.agda | 2 +- 8 files changed, 148 insertions(+), 71 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index e8a6f73..22b4a27 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -14,32 +14,12 @@ open import Cat.Categories.Fun -- The category of categories module _ (ℓ ℓ' : Level) where - private - module _ {𝔸 𝔹 ℂ 𝔻 : Category ℓ ℓ'} {F : Functor 𝔸 𝔹} {G : Functor 𝔹 ℂ} {H : Functor ℂ 𝔻} where - assc : F[ H ∘ F[ G ∘ F ] ] ≡ F[ F[ H ∘ G ] ∘ F ] - assc = Functor≡ refl - - module _ {ℂ 𝔻 : Category ℓ ℓ'} {F : Functor ℂ 𝔻} where - ident-r : F[ F ∘ identity ] ≡ F - ident-r = Functor≡ refl - - ident-l : F[ identity ∘ F ] ≡ F - ident-l = Functor≡ refl - RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ') RawCategory.Object RawCat = Category ℓ ℓ' RawCategory.Arrow RawCat = Functor - RawCategory.𝟙 RawCat = identity + RawCategory.𝟙 RawCat = Functors.identity RawCategory._∘_ RawCat = F[_∘_] - private - open RawCategory RawCat - isAssociative : IsAssociative - isAssociative {f = F} {G} {H} = assc {F = F} {G = G} {H = H} - - isIdentity : IsIdentity identity - isIdentity = ident-l , ident-r - -- 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. @@ -283,7 +263,7 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where : Functor 𝔸 object → Functor ℂ ℂ → Functor (𝔸 ⊗ ℂ) (object ⊗ ℂ) transpose : Functor 𝔸 object - eq : F[ eval ∘ (parallelProduct transpose (identity {C = ℂ})) ] ≡ F + eq : F[ eval ∘ (parallelProduct transpose (Functors.identity {ℂ = ℂ})) ] ≡ F -- eq : F[ :eval: ∘ {!!} ] ≡ F -- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F -- eq' : (Catℓ [ :eval: ∘ diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 18165d3..140b535 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -4,7 +4,7 @@ module Cat.Categories.Fun where open import Cat.Prelude open import Cat.Category -open import Cat.Category.Functor hiding (identity) +open import Cat.Category.Functor open import Cat.Category.NaturalTransformation module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where @@ -14,20 +14,18 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C module ℂ = Category ℂ module 𝔻 = Category 𝔻 private - module _ {A B C D : Functor ℂ 𝔻} {θ' : NaturalTransformation A B} - {η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where - θ = proj₁ θ' - η = proj₁ η' - ζ = proj₁ ζ' - θNat = proj₂ θ' - ηNat = proj₂ η' - ζNat = proj₂ ζ' - L : NaturalTransformation A D - L = (NT[_∘_] {A} {C} {D} ζ' (NT[_∘_] {A} {B} {C} η' θ')) - R : NaturalTransformation A D - R = (NT[_∘_] {A} {B} {D} (NT[_∘_] {B} {C} {D} ζ' η') θ') - _g⊕f_ = NT[_∘_] {A} {B} {C} - _h⊕g_ = NT[_∘_] {B} {C} {D} + module _ {A B C D : Functor ℂ 𝔻} {θNT : NaturalTransformation A B} + {ηNT : NaturalTransformation B C} {ζNT : NaturalTransformation C D} where + open Σ θNT renaming (proj₁ to θ ; proj₂ to θNat) + open Σ ηNT renaming (proj₁ to η ; proj₂ to ηNat) + open Σ ζNT renaming (proj₁ to ζ ; proj₂ to ζNat) + private + L : NaturalTransformation A D + L = (NT[_∘_] {A} {C} {D} ζNT (NT[_∘_] {A} {B} {C} ηNT θNT)) + R : NaturalTransformation A D + R = (NT[_∘_] {A} {B} {D} (NT[_∘_] {B} {C} {D} ζNT ηNT) θNT) + _g⊕f_ = NT[_∘_] {A} {B} {C} + _h⊕g_ = NT[_∘_] {B} {C} {D} isAssociative : L ≡ R isAssociative = lemSig (naturalIsProp {F = A} {D}) L R (funExt (λ x → 𝔻.isAssociative)) @@ -62,6 +60,71 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C open RawCategory RawFun open Univalence (λ {A} {B} {f} → isIdentity {A} {B} {f}) + private + module _ (F : Functor ℂ 𝔻) where + center : Σ[ G ∈ Object ] (F ≅ G) + center = F , id-to-iso F F refl + + open Σ center renaming (proj₂ to isoF) + + module _ (cG : Σ[ G ∈ Object ] (F ≅ G)) where + open Σ cG renaming (proj₁ to G ; proj₂ to isoG) + module G = Functor G + open Σ isoG renaming (proj₁ to θNT ; proj₂ to invθNT) + open Σ invθNT renaming (proj₁ to ηNT ; proj₂ to areInv) + open Σ θNT renaming (proj₁ to θ ; proj₂ to θN) + open Σ ηNT renaming (proj₁ to η ; proj₂ to ηN) + open Σ areInv renaming (proj₁ to ve-re ; proj₂ to re-ve) + + -- f ~ Transformation G G + -- f : (X : ℂ.Object) → 𝔻 [ G.omap X , G.omap X ] + -- f X = T[ θ ∘ η ] X + -- g = T[ η ∘ θ ] {!!} + + ntF : NaturalTransformation F F + ntF = 𝟙 {A = F} + + ntG : NaturalTransformation G G + ntG = 𝟙 {A = G} + + idFunctor = Functors.identity + + -- Dunno if this is the way to go, but if I can construct a an inverse of + -- G that is also inverse of F (possibly by being propositionally equal to + -- another functor F~) + postulate + G~ : Functor 𝔻 ℂ + F~ : Functor 𝔻 ℂ + F~ = G~ + postulate + prop0 : F[ G~ ∘ G ] ≡ idFunctor + prop1 : F[ F ∘ G~ ] ≡ idFunctor + + lem : F[ F ∘ F~ ] ≡ idFunctor + lem = begin + F[ F ∘ F~ ] ≡⟨⟩ + F[ F ∘ G~ ] ≡⟨ prop1 ⟩ + idFunctor ∎ + + open import Cubical.Univalence + p0 : F ≡ G + p0 = begin + F ≡⟨ sym Functors.rightIdentity ⟩ + F[ F ∘ idFunctor ] ≡⟨ cong (λ φ → F[ F ∘ φ ]) (sym prop0) ⟩ + F[ F ∘ F[ G~ ∘ G ] ] ≡⟨ Functors.isAssociative {F = G} {G = G~} {H = F} ⟩ + F[ F[ F ∘ G~ ] ∘ G ] ≡⟨⟩ + F[ F[ F ∘ F~ ] ∘ G ] ≡⟨ cong (λ φ → F[ φ ∘ G ]) lem ⟩ + F[ idFunctor ∘ G ] ≡⟨ Functors.leftIdentity ⟩ + G ∎ + + p1 : (λ i → Σ (Arrow F (p0 i)) (Isomorphism {A = F} {B = p0 i})) [ isoF ≡ isoG ] + p1 = {!!} + + isContractible : (F , isoF) ≡ (G , isoG) + isContractible i = p0 i , p1 i + + univalent[Contr] : isContr (Σ[ G ∈ Object ] (F ≅ G)) + univalent[Contr] = center , isContractible private module _ {A B : Functor ℂ 𝔻} where diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index 390d8bc..bbdda14 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -1,7 +1,7 @@ {-# OPTIONS --cubical #-} module Cat.Category.Functor where -open import Agda.Primitive +open import Cat.Prelude open import Function open import Cubical @@ -9,31 +9,31 @@ open import Cubical.NType.Properties using (lemPropF) open import Cat.Category -open Category hiding (_∘_ ; raw ; IsIdentity) - module _ {ℓc ℓc' ℓd ℓd'} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where private + module ℂ = Category ℂ + module 𝔻 = Category 𝔻 ℓ = ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd' 𝓤 = Set ℓ - Omap = Object ℂ → Object 𝔻 + Omap = ℂ.Object → 𝔻.Object Fmap : Omap → Set _ Fmap omap = ∀ {A B} → ℂ [ A , B ] → 𝔻 [ omap A , omap B ] record RawFunctor : 𝓤 where field - omap : Object ℂ → Object 𝔻 + omap : ℂ.Object → 𝔻.Object fmap : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ omap A , omap B ] IsIdentity : Set _ - IsIdentity = {A : Object ℂ} → fmap (𝟙 ℂ {A}) ≡ 𝟙 𝔻 {omap A} + IsIdentity = {A : ℂ.Object} → fmap (ℂ.𝟙 {A}) ≡ 𝔻.𝟙 {omap A} IsDistributive : Set _ - IsDistributive = {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]} + IsDistributive = {A B C : ℂ.Object} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]} → fmap (ℂ [ g ∘ f ]) ≡ 𝔻 [ fmap g ∘ fmap f ] -- | Equality principle for raw functors @@ -120,11 +120,18 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat res : (λ i → IsFunctor ℂ 𝔻 (eq i)) [ isFunctor F ≡ isFunctor G ] res = IsFunctorIsProp' (isFunctor F) (isFunctor G) -module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where +module _ {ℓ0 ℓ1 ℓ2 ℓ3 ℓ4 ℓ5 : Level} + {A : Category ℓ0 ℓ1} + {B : Category ℓ2 ℓ3} + {C : Category ℓ4 ℓ5} + (F : Functor B C) (G : Functor A B) where private + module A = Category A + module B = Category B + module C = Category C module F = Functor F module G = Functor G - module _ {a0 a1 a2 : Object A} {α0 : A [ a0 , a1 ]} {α1 : A [ a1 , a2 ]} where + module _ {a0 a1 a2 : A.Object} {α0 : A [ a0 , a1 ]} {α1 : A [ a1 , a2 ]} where dist : (F.fmap ∘ G.fmap) (A [ α1 ∘ α0 ]) ≡ C [ (F.fmap ∘ G.fmap) α1 ∘ (F.fmap ∘ G.fmap) α0 ] dist = begin (F.fmap ∘ G.fmap) (A [ α1 ∘ α0 ]) @@ -143,10 +150,10 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F isFunctor : IsFunctor A C raw isFunctor = record { isIdentity = begin - (F.fmap ∘ G.fmap) (𝟙 A) ≡⟨ refl ⟩ - F.fmap (G.fmap (𝟙 A)) ≡⟨ cong F.fmap (G.isIdentity)⟩ - F.fmap (𝟙 B) ≡⟨ F.isIdentity ⟩ - 𝟙 C ∎ + (F.fmap ∘ G.fmap) A.𝟙 ≡⟨ refl ⟩ + F.fmap (G.fmap A.𝟙) ≡⟨ cong F.fmap (G.isIdentity)⟩ + F.fmap B.𝟙 ≡⟨ F.isIdentity ⟩ + C.𝟙 ∎ ; isDistributive = dist } @@ -154,15 +161,42 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F Functor.raw F[_∘_] = raw Functor.isFunctor F[_∘_] = isFunctor --- The identity functor -identity : ∀ {ℓ ℓ'} → {C : Category ℓ ℓ'} → Functor C C -identity = record - { raw = record - { omap = λ x → x - ; fmap = λ x → x - } - ; isFunctor = record - { isIdentity = refl - ; isDistributive = refl - } - } +-- | The identity functor +module Functors where + module _ {ℓc ℓcc : Level} {ℂ : Category ℓc ℓcc} where + private + raw : RawFunctor ℂ ℂ + RawFunctor.omap raw = Function.id + RawFunctor.fmap raw = Function.id + + isFunctor : IsFunctor ℂ ℂ raw + IsFunctor.isIdentity isFunctor = refl + IsFunctor.isDistributive isFunctor = refl + + identity : Functor ℂ ℂ + Functor.raw identity = raw + Functor.isFunctor identity = isFunctor + + module _ + {ℓa ℓaa ℓb ℓbb ℓc ℓcc ℓd ℓdd : Level} + {𝔸 : Category ℓa ℓaa} + {𝔹 : Category ℓb ℓbb} + {ℂ : Category ℓc ℓcc} + {𝔻 : Category ℓd ℓdd} + {F : Functor 𝔸 𝔹} {G : Functor 𝔹 ℂ} {H : Functor ℂ 𝔻} where + isAssociative : F[ H ∘ F[ G ∘ F ] ] ≡ F[ F[ H ∘ G ] ∘ F ] + isAssociative = Functor≡ refl + + module _ + {ℓc ℓcc ℓd ℓdd : Level} + {ℂ : Category ℓc ℓcc} + {𝔻 : Category ℓd ℓdd} + {F : Functor ℂ 𝔻} where + leftIdentity : F[ identity ∘ F ] ≡ F + leftIdentity = Functor≡ refl + + rightIdentity : F[ F ∘ identity ] ≡ F + rightIdentity = Functor≡ refl + + isIdentity : F[ identity ∘ F ] ≡ F × F[ F ∘ identity ] ≡ F + isIdentity = leftIdentity , rightIdentity diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index 3b65149..d2aa713 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -176,9 +176,9 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where pureTEq : M.RawMonad.pureT (backRaw (forth m)) ≡ pureT pureTEq = funExt (λ X → refl) - pureNTEq : (λ i → NaturalTransformation F.identity (Req i)) + pureNTEq : (λ i → NaturalTransformation Functors.identity (Req i)) [ M.RawMonad.pureNT (backRaw (forth m)) ≡ pureNT ] - pureNTEq = lemSigP (λ i → propIsNatural F.identity (Req i)) _ _ pureTEq + pureNTEq = lemSigP (λ i → propIsNatural Functors.identity (Req i)) _ _ pureTEq joinTEq : M.RawMonad.joinT (backRaw (forth m)) ≡ joinT joinTEq = funExt (λ X → begin diff --git a/src/Cat/Category/Monad/Kleisli.agda b/src/Cat/Category/Monad/Kleisli.agda index 7377cdf..be48a8d 100644 --- a/src/Cat/Category/Monad/Kleisli.agda +++ b/src/Cat/Category/Monad/Kleisli.agda @@ -119,7 +119,7 @@ record IsMonad (raw : RawMonad) : Set ℓ where open NaturalTransformation ℂ ℂ R⁰ : EndoFunctor ℂ - R⁰ = F.identity + R⁰ = Functors.identity R² : EndoFunctor ℂ R² = F[ R ∘ R ] module R = Functor R diff --git a/src/Cat/Category/Monad/Monoidal.agda b/src/Cat/Category/Monad/Monoidal.agda index 360e5df..4270323 100644 --- a/src/Cat/Category/Monad/Monoidal.agda +++ b/src/Cat/Category/Monad/Monoidal.agda @@ -22,14 +22,14 @@ open NaturalTransformation ℂ ℂ record RawMonad : Set ℓ where field R : EndoFunctor ℂ - pureNT : NaturalTransformation F.identity R + pureNT : NaturalTransformation Functors.identity R joinNT : NaturalTransformation F[ R ∘ R ] R -- Note that `pureT` and `joinT` differs from their definition in the -- kleisli formulation only by having an explicit parameter. - pureT : Transformation F.identity R + pureT : Transformation Functors.identity R pureT = proj₁ pureNT - pureN : Natural F.identity R pureT + pureN : Natural Functors.identity R pureT pureN = proj₂ pureNT joinT : Transformation F[ R ∘ R ] R diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda index dfcdbda..6dfb245 100644 --- a/src/Cat/Category/Monad/Voevodsky.agda +++ b/src/Cat/Category/Monad/Voevodsky.agda @@ -50,9 +50,9 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where pureT X = pure {X} field - pureN : Natural F.identity R pureT + pureN : Natural Functors.identity R pureT - pureNT : NaturalTransformation F.identity R + pureNT : NaturalTransformation Functors.identity R pureNT = pureT , pureN joinT : (A : Object) → ℂ [ omap (omap A) , omap A ] diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda index 13e3d89..016f9a5 100644 --- a/src/Cat/Category/NaturalTransformation.agda +++ b/src/Cat/Category/NaturalTransformation.agda @@ -26,7 +26,7 @@ open import Data.Nat using (_≤_ ; z≤n ; s≤s) module Nat = Data.Nat open import Cat.Category -open import Cat.Category.Functor hiding (identity) +open import Cat.Category.Functor open import Cat.Wishlist module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}