Refactor Functor - only in module Functor

2018-02-06 14:24:34 +01:00 · 2018-02-06 14:24:34 +01:00 · 9349b37550
parent a27292dd53
commit 9349b37550
5 changed files with 133 additions and 72 deletions
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@ -14,15 +14,18 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
  open Functor

  module _ (F G : Functor ℂ 𝔻) where
+    private
+      module F = Functor F
+      module G = Functor G
    -- What do you call a non-natural tranformation?
    Transformation : Set (ℓc ⊔ ℓd')
-    Transformation = (C : Object ℂ) → 𝔻 [ F .func* C , G .func* C ]
+    Transformation = (C : Object ℂ) → 𝔻 [ F.func* C , G.func* C ]

    Natural : Transformation → Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
    Natural θ
      = {A B : Object ℂ}
      → (f : ℂ [ A , B ])
-      → 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ]
+      → 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ]

    NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
    NaturalTransformation = Σ Transformation Natural
@ -30,13 +33,12 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
    -- NaturalTranformation : Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
    -- NaturalTranformation = ∀ (θ : Transformation) {A B : ℂ .Object} → (f : ℂ .Arrow A B) → 𝔻 ._⊕_ (θ B) (F .func→ f) ≡ 𝔻 ._⊕_ (G .func→ f) (θ A)

-  module _ {F G : Functor ℂ 𝔻} where
-    NaturalTransformation≡ : {α β : NaturalTransformation F G}
+    NaturalTransformation≡ : {α β : NaturalTransformation}
      → (eq₁ : α .proj₁ ≡ β .proj₁)
      → (eq₂ : PathP
          (λ i → {A B : Object ℂ} (f : ℂ [ A , B ])
-            → 𝔻 [ eq₁ i B ∘ F .func→ f ]
-            ≡ 𝔻 [ G .func→ f ∘ eq₁ i A ])
+            → 𝔻 [ eq₁ i B ∘ F.func→ f ]
+            ≡ 𝔻 [ G.func→ f ∘ eq₁ i A ])
        (α .proj₂) (β .proj₂))
      → α ≡ β
    NaturalTransformation≡ eq₁ eq₂ i = eq₁ i , eq₂ i
@ -52,7 +54,8 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
    𝔻 [ F→ f ∘ 𝟙 𝔻 ]               ≡⟨⟩
    𝔻 [ F→ f ∘ identityTrans F A ]  ∎
    where
-      F→ = F .func→
+      module F = Functor F
+      F→ = F.func→
      module 𝔻 = IsCategory (isCategory 𝔻)

  identityNat : (F : Functor ℂ 𝔻) → NaturalTransformation F F
@ -60,20 +63,23 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat

  module _ {F G H : Functor ℂ 𝔻} where
    private
+      module F = Functor F
+      module G = Functor G
+      module H = Functor H
      _∘nt_ : Transformation G H → Transformation F G → Transformation F H
      (θ ∘nt η) C = 𝔻 [ θ C ∘ η C ]

    NatComp _:⊕:_ : NaturalTransformation G H → NaturalTransformation F G → NaturalTransformation F H
    proj₁ ((θ , _) :⊕: (η , _)) = θ ∘nt η
    proj₂ ((θ , θNat) :⊕: (η , ηNat)) {A} {B} f = begin
-      𝔻 [ (θ ∘nt η) B ∘ F .func→ f ]     ≡⟨⟩
-      𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F .func→ f ] ≡⟨ sym assoc ⟩
-      𝔻 [ θ B ∘ 𝔻 [ η B ∘ F .func→ f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩
-      𝔻 [ θ B ∘ 𝔻 [ G .func→ f ∘ η A ] ] ≡⟨ assoc ⟩
-      𝔻 [ 𝔻 [ θ B ∘ G .func→ f ] ∘ η A ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ η A ]) (θNat f) ⟩
-      𝔻 [ 𝔻 [ H .func→ f ∘ θ A ] ∘ η A ] ≡⟨ sym assoc ⟩
-      𝔻 [ H .func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
-      𝔻 [ H .func→ f ∘ (θ ∘nt η) A ]     ∎
+      𝔻 [ (θ ∘nt η) B ∘ F.func→ f ]     ≡⟨⟩
+      𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F.func→ f ] ≡⟨ sym assoc ⟩
+      𝔻 [ θ B ∘ 𝔻 [ η B ∘ F.func→ f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩
+      𝔻 [ θ B ∘ 𝔻 [ G.func→ f ∘ η A ] ] ≡⟨ assoc ⟩
+      𝔻 [ 𝔻 [ θ B ∘ G.func→ f ] ∘ η A ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ η A ]) (θNat f) ⟩
+      𝔻 [ 𝔻 [ H.func→ f ∘ θ A ] ∘ η A ] ≡⟨ sym assoc ⟩
+      𝔻 [ H.func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
+      𝔻 [ H.func→ f ∘ (θ ∘nt η) A ]     ∎
      where
        open IsCategory (isCategory 𝔻)

--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@ -56,8 +56,10 @@ Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'})
 -- The "co-yoneda" embedding.
 representable : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} → Category.Object ℂ → Representable ℂ
 representable {ℂ = ℂ} A = record
+  { raw = record
    { func* = λ B → ℂ [ A , B ]
    ; func→ = ℂ [_∘_]
+    }
  ; isFunctor = record
    { ident = funExt λ _ → proj₂ ident
    ; distrib = funExt λ x → sym assoc
@ -73,8 +75,10 @@ Presheaf {ℓ' = ℓ'} ℂ = Functor (Opposite ℂ) (Sets {ℓ'})
 -- Alternate name: `yoneda`
 presheaf : {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} → Category.Object (Opposite ℂ) → Presheaf ℂ
 presheaf {ℂ = ℂ} B = record
+  { raw = record
    { func* = λ A → ℂ [ A , B ]
    ; func→ = λ f g → ℂ [ g ∘ f ]
+  }
  ; isFunctor = record
    { ident = funExt λ x → proj₁ ident
    ; distrib = funExt λ x → assoc
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@ -53,10 +53,6 @@ record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
 -- (univalent).
 record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
  open RawCategory ℂ
-  -- (Object : Set ℓ)
-  -- (Arrow  : Object → Object → Set ℓ')
-  -- (𝟙      : {o : Object} → Arrow o o)
-  -- (_∘_    : { a b c : Object } → Arrow b c → Arrow a b → Arrow a c)
  field
    assoc : {A B C D : Object} { f : Arrow A B } { g : Arrow B C } { h : Arrow C D }
      → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
--- a/src/Cat/Category/Functor.agda
+++ b/src/Cat/Category/Functor.agda
@ -6,61 +6,110 @@ open import Function

 open import Cat.Category

-open Category hiding (_∘_)
+open Category hiding (_∘_ ; raw)

-module _ {ℓc ℓc' ℓd ℓd'} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
-  record IsFunctor
-    (func* : Object ℂ → Object 𝔻)
-    (func→ : {A B : Object ℂ} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ])
-      : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
+module _ {ℓc ℓc' ℓd ℓd'}
+    (ℂ : Category ℓc ℓc')
+    (𝔻 : Category ℓd ℓd')
+    where
+
+  private
+    ℓ = ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd'
+    𝓤 = Set ℓ
+
+  record RawFunctor : 𝓤 where
+    field
+      func* : Object ℂ → Object 𝔻
+      func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]
+
+  record IsFunctor (F : RawFunctor) : 𝓤 where
+    open RawFunctor F
    field
      ident   : {c : Object ℂ} → func→ (𝟙 ℂ {c}) ≡ 𝟙 𝔻 {func* c}
-      -- TODO: Avoid use of ugly explicit arguments somehow.
-      -- This guy managed to do it:
-      --    https://github.com/copumpkin/categories/blob/master/Categories/Functor/Core.agda
      distrib : {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
        → func→ (ℂ [ g ∘ f ]) ≡ 𝔻 [ func→ g ∘ func→ f ]

  record Functor : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
    field
+      raw : RawFunctor
+      {{isFunctor}} : IsFunctor raw
+
+    private
+      module R = RawFunctor raw
+
    func* : Object ℂ → Object 𝔻
+    func* = R.func*
+
    func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]
-      {{isFunctor}} : IsFunctor func* func→
+    func→ = R.func→

 open IsFunctor
 open Functor

+-- TODO: Is `IsFunctor` a proposition?
+module _
+    {ℓa ℓb : Level}
+    {ℂ 𝔻 : Category ℓa ℓb}
+    {F : RawFunctor ℂ 𝔻}
+    where
+  private
+    module 𝔻 = IsCategory (isCategory 𝔻)
+
+  -- isProp  : Set ℓ
+  -- isProp  = (x y : A) → x ≡ y
+
+  IsFunctorIsProp : isProp (IsFunctor _ _ F)
+  IsFunctorIsProp isF0 isF1 i = record
+    { ident = 𝔻.arrowIsSet isF0.ident isF1.ident i
+    ; distrib = 𝔻.arrowIsSet isF0.distrib isF1.distrib i
+    }
+    where
+      module isF0 = IsFunctor isF0
+      module isF1 = IsFunctor isF1
+
+-- Alternate version of above where `F` is a path in 
+module _
+    {ℓa ℓb : Level}
+    {ℂ 𝔻 : Category ℓa ℓb}
+    {F : I → RawFunctor ℂ 𝔻}
+    where
+  private
+    module 𝔻 = IsCategory (isCategory 𝔻)
+  IsProp' : {ℓ : Level} (A : I → Set ℓ) → Set ℓ
+  IsProp' A = (a0 : A i0) (a1 : A i1) → A [ a0 ≡ a1 ]
+
+  postulate IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i)
+  -- IsFunctorIsProp' isF0 isF1 i = record
+  --   { ident = {!𝔻.arrowIsSet {!isF0.ident!} {!isF1.ident!} i!}
+  --   ; distrib = {!𝔻.arrowIsSet {!isF0.distrib!} {!isF1.distrib!} i!}
+  --   }
+  --   where
+  --     module isF0 = IsFunctor isF0
+  --     module isF1 = IsFunctor isF1
+
 module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where
-
-  IsFunctor≡
-    : {func* : Object ℂ → Object 𝔻}
-      {func→ : {A B : Object ℂ} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]}
-      {F G : IsFunctor ℂ 𝔻 func* func→}
-    → (eqI
-      : (λ i → ∀ {A} → func→ (𝟙 ℂ {A}) ≡ 𝟙 𝔻 {func* A})
-        [ F .ident ≡ G .ident ])
-    → (eqD :
-        (λ i → ∀ {A B C} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
-          → func→ (ℂ [ g ∘ f ]) ≡ 𝔻 [ func→ g ∘ func→ f ])
-        [ F .distrib ≡ G .distrib ])
-    → (λ _ → IsFunctor ℂ 𝔻 (λ i → func* i) func→) [ F ≡ G ]
-  IsFunctor≡ eqI eqD i = record { ident = eqI i ; distrib = eqD i }
-
  Functor≡ : {F G : Functor ℂ 𝔻}
-    → (eq* : F .func* ≡ G .func*)
+    → (eq* : func* F ≡ func* G)
    → (eq→ : (λ i → ∀ {x y} → ℂ [ x , y ] → 𝔻 [ eq* i x , eq* i y ])
-        [ F .func→ ≡ G .func→ ])
-    -- → (eqIsF : PathP (λ i → IsFunctor ℂ 𝔻 (eq* i) (eq→ i)) (F .isFunctor) (G .isFunctor))
-    → (eqIsFunctor : (λ i → IsFunctor ℂ 𝔻 (eq* i) (eq→ i)) [ F .isFunctor ≡ G .isFunctor ])
+        [ func→ F ≡ func→ G ])
    → F ≡ G
-  Functor≡ eq* eq→ eqIsFunctor i = record { func* = eq* i ; func→ = eq→ i ; isFunctor = eqIsFunctor i }
+  Functor≡ {F} {G} eq* eq→ i = record
+    { raw = eqR i
+    ; isFunctor = f i
+    }
+    where
+      eqR : raw F ≡ raw G
+      eqR i = record { func* = eq* i ; func→ = eq→ i }
+      postulate T : isSet (IsFunctor _ _ (raw F))
+      f : (λ i →  IsFunctor ℂ 𝔻 (eqR i)) [ isFunctor F ≡ isFunctor G ]
+      f = IsFunctorIsProp' (isFunctor F) (isFunctor G)

 module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where
  private
-    F* = F .func*
-    F→ = F .func→
-    G* = G .func*
-    G→ = G .func→
+    F* = func* F
+    F→ = func→ F
+    G* = func* G
+    G→ = func→ G
    module _ {a0 a1 a2 : Object A} {α0 : A [ a0 , a1 ]} {α1 : A [ a1 , a2 ]} where

      dist : (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ]
@ -70,12 +119,12 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
        F→ (B [ G→ α1 ∘ G→ α0 ])          ≡⟨ F .isFunctor .distrib ⟩
        C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] ∎

-  _∘f_ : Functor A C
-  _∘f_ =
-    record
-      { func* = F* ∘ G*
-      ; func→ = F→ ∘ G→
-      ; isFunctor = record
+    _∘fr_ : RawFunctor A C
+    RawFunctor.func* _∘fr_ = F* ∘ G*
+    RawFunctor.func→ _∘fr_ = F→ ∘ G→
+    instance
+      isFunctor' : IsFunctor A C _∘fr_
+      isFunctor' = record
        { ident = begin
          (F→ ∘ G→) (𝟙 A) ≡⟨ refl ⟩
          F→ (G→ (𝟙 A))   ≡⟨ cong F→ (G .isFunctor .ident)⟩
@ -83,13 +132,17 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
          𝟙 C             ∎
        ; distrib = dist
        }
-      }
+
+  _∘f_ : Functor A C
+  raw _∘f_ = _∘fr_

 -- The identity functor
 identity : ∀ {ℓ ℓ'} → {C : Category ℓ ℓ'} → Functor C C
 identity = record
+  { raw = record
    { func* = λ x → x
    ; func→ = λ x → x
+    }
  ; isFunctor = record
    { ident = refl
    ; distrib = refl
--- a/src/Cat/CwF.agda
+++ b/src/Cat/CwF.agda
@ -25,8 +25,10 @@ module _ {ℓa ℓb : Level} where
      T : Functor (Opposite ℂ) (Fam ℓa ℓb)
      -- Empty context
      [] : Terminal ℂ
+    private
+      module T = Functor T
    Type : (Γ : Object ℂ) → Set ℓa
-    Type Γ = proj₁ (T .func* Γ)
+    Type Γ = proj₁ (T.func* Γ)

    module _ {Γ : Object ℂ} {A : Type Γ} where

@ -35,7 +37,7 @@ module _ {ℓa ℓb : Level} where
          (λ f →
          {x : proj₁ (func* T B)} →
          proj₂ (func* T B) x → proj₂ (func* T A) (f x))
-        k = T .func→ γ
+        k = T.func→ γ
        k₁ : proj₁ (func* T B) → proj₁ (func* T A)
        k₁ = proj₁ k
        k₂ : ({x : proj₁ (func* T B)} →