Move identity functor laws to functor module...

and make progress on univalence in the functor category

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: ∘

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

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

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

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

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

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 ]

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}