Use equality construction principle

Also update submodules

libs/agda-stdlib

@@ -1 +1 @@
-Subproject commit de23244a73d6dab55715fd5a107a5de805c55764
+Subproject commit b5bfbc3c170b0bd0c9aaac1b4d4b3f9b06832bf6

libs/cubical

@@ -1 +1 @@
-Subproject commit a83f5f4c63e5dfd8143ac03163868c63a56802de
+Subproject commit 1d6730c4999daa2b04e9dd39faa0791d0b5c3b48

src/Cat/Categories/Cat.agda

@@ -44,7 +44,7 @@ module _ (ℓ ℓ' : Level) where
                             ((h ∘f (g ∘f f)) .isFunctor .distrib) (((h ∘f g) ∘f f) .isFunctor .distrib)
 
       assc : h ∘f (g ∘f f) ≡ (h ∘f g) ∘f f
-      assc = Functor≡ eq* eq→ eqI eqD
+      assc = Functor≡ eq* eq→ (IsFunctor≡ eqI eqD)
 
     module _ {ℂ 𝔻 : Category ℓ ℓ'} {F : Functor ℂ 𝔻} where
       module _ where
@@ -58,16 +58,17 @@ module _ (ℓ ℓ' : Level) where
             (func→ (F ∘f identity)) (func→ F)
           eq→ = refl
           postulate
-            eqI-r : PathP (λ i → {c : ℂ .Object}
+            eqI-r
-                → PathP (λ _ → Arrow 𝔻 (func* F c) (func* F c)) (func→ F (ℂ .𝟙)) (𝔻 .𝟙))
+              : (λ i → {c : ℂ .Object} → (λ _ → 𝔻 [ func* F c , func* F c ])
-                  ((F ∘f identity) .isFunctor .ident) (F .isFunctor .ident)
+                [ func→ F (ℂ .𝟙) ≡ 𝔻 .𝟙 ])
+              [(F ∘f identity) .isFunctor .ident ≡ F .isFunctor .ident ]
             eqD-r : PathP
                         (λ i →
                         {A B C : ℂ .Object} {f : ℂ .Arrow A B} {g : ℂ .Arrow B C} →
                         eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ])
                         ((F ∘f identity) .isFunctor .distrib) (F .isFunctor .distrib)
         ident-r : F ∘f identity ≡ F
-        ident-r = Functor≡ eq* eq→ eqI-r eqD-r
+        ident-r = Functor≡ eq* eq→ (IsFunctor≡ eqI-r eqD-r)
       module _ where
         private
           postulate
@@ -75,13 +76,14 @@ module _ (ℓ ℓ' : Level) where
             eq→ : PathP
               (λ i → {x y : Object ℂ} → ℂ .Arrow x y → 𝔻 .Arrow (eq* i x) (eq* i y))
               ((identity ∘f F) .func→) (F .func→)
-            eqI : PathP (λ i → ∀ {A : ℂ .Object} → eq→ i (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {eq* i A})
+            eqI : (λ i → ∀ {A : ℂ .Object} → eq→ i (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {eq* i A})
-                  ((identity ∘f F) .isFunctor .ident) (F .isFunctor .ident)
+                  [ ((identity ∘f F) .isFunctor .ident) ≡ (F .isFunctor .ident) ]
             eqD : PathP (λ i → {A B C : ℂ .Object} {f : ℂ .Arrow A B} {g : ℂ .Arrow B C}
                  → eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ])
                  ((identity ∘f F) .isFunctor .distrib) (F .isFunctor .distrib)
+                 -- (λ z → eq* i z) (eq→ i)
         ident-l : identity ∘f F ≡ F
-        ident-l = Functor≡ eq* eq→ eqI eqD
+        ident-l = Functor≡ eq* eq→ λ i → record { ident = eqI i ; distrib = eqD i }
 
   Cat : Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
   Cat =

src/Cat/Categories/Fun.agda

@@ -53,7 +53,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
     𝔻 [ F→ f ∘ identityTrans F A ]  ∎
     where
       F→ = F .func→
-      open module 𝔻 = IsCategory (𝔻 .isCategory)
+      module 𝔻 = IsCategory (𝔻 .isCategory)
 
   identityNat : (F : Functor ℂ 𝔻) → NaturalTransformation F F
   identityNat F = identityTrans F , identityNatural F

src/Cat/Category/Properties.agda

@@ -9,6 +9,8 @@ open import Cubical
 open import Cat.Category
 open import Cat.Functor
 open import Cat.Categories.Sets
+open import Cat.Equality
+open Equality.Data.Product
 
 module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : ℂ .Category.Object } {X : ℂ .Category.Object} (f : ℂ .Category.Arrow A B) where
   open Category ℂ
@@ -58,6 +60,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
   private
     Catℓ = Cat ℓ ℓ
     prshf = presheaf {ℂ = ℂ}
+    module ℂ = IsCategory (ℂ .isCategory)
 
     -- Exp : Set (lsuc (lsuc ℓ))
     -- Exp = Exponential (Cat (lsuc ℓ) ℓ)
@@ -70,22 +73,24 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
 
     module _ {A B : ℂ .Object} (f : ℂ .Arrow A B) where
       :func→: : NaturalTransformation (prshf A) (prshf B)
-      :func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ x → lem
+      :func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ _ → ℂ.assoc
-        where
+
-          lem = (ℂ .isCategory) .IsCategory.assoc
     module _ {c : ℂ .Object} where
-      eqTrans : (:func→: (ℂ .𝟙 {c})) .proj₁ ≡ (Fun .𝟙 {o = prshf c}) .proj₁
+      eqTrans : (λ _ → Transformation (prshf c) (prshf c))
-      eqTrans = funExt λ x → funExt λ x → ℂ .isCategory .IsCategory.ident .proj₂
+        [ (λ _ x → ℂ [ ℂ .𝟙 ∘ x ]) ≡ identityTrans (prshf c) ]
-      eqNat
+      eqTrans = funExt λ x → funExt λ x → ℂ.ident .proj₂
-                 : PathP (λ i → {A B : ℂ .Object} (f : Opposite ℂ .Arrow A B)
+
-                   →   Sets [ eqTrans i B ∘ prshf c .Functor.func→ f ]
+      eqNat : (λ i → Natural (prshf c) (prshf c) (eqTrans i))
-                     ≡ Sets [ prshf c .Functor.func→ f ∘ eqTrans i A ])
+        [(λ _ → funExt (λ _ → ℂ.assoc)) ≡ identityNatural (prshf c)]
-                   ((:func→: (ℂ .𝟙 {c})) .proj₂) ((Fun .𝟙 {o = prshf c}) .proj₂)
+      eqNat = {!!}
-      eqNat = λ i f i' x₁ → {!ℂ ._⊕_ ? ?!}
+      -- eqNat = λ {A} {B} i ℂ[B,A] i' ℂ[A,c] →
-      -- eqNat i f = {!!}
+      --   let
-      -- Sets ._⊕_ (eq₁ i B) (prshf A .func→ f) ≡ Sets ._⊕_ (prshf B .func→ f) (eq₁ i A)
+      --     k : ℂ [ {!!} , {!!} ]
+      --     k = ℂ[A,c]
+      --   in {!ℂ [ ? ∘ ? ]!}
+
       :ident: : (:func→: (ℂ .𝟙 {c})) ≡ (Fun .𝟙 {o = prshf c})
-      :ident: = NaturalTransformation≡ eqTrans eqNat
+      :ident: = Σ≡ eqTrans eqNat
 
   yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = Sets {ℓ}})
   yoneda = record

src/Cat/Equality.agda

@@ -0,0 +1,21 @@
+-- Defines equality-principles for data-types from the standard library.
+
+module Cat.Equality where
+
+open import Level
+open import Cubical
+
+-- _[_≡_] = PathP
+
+module Equality where
+  module Data where
+    module Product where
+      open import Data.Product public
+
+      module _ {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb} {a b : Σ A B}
+        (proj₁≡ : (λ _ → A)            [ proj₁ a ≡ proj₁ b ])
+        (proj₂≡ : (λ i → B (proj₁≡ i)) [ proj₂ a ≡ proj₂ b ]) where
+
+        Σ≡ : a ≡ b
+        proj₁ (Σ≡ i) = proj₁≡ i
+        proj₂ (Σ≡ i) = proj₂≡ i

src/Cat/Functor.agda

@@ -32,27 +32,28 @@ open Functor
 
 module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where
 
-  -- IsFunctor≡ : ∀ {A B : ℂ .Object} {func* : ℂ .Object → 𝔻 .Object} {func→ : {A B : ℂ .Object} → ℂ .Arrow A B → 𝔻 .Arrow (func* A) (func* B)} {F G : IsFunctor ℂ 𝔻 func* func→}
+  IsFunctor≡
-  --   → (eqI : PathP (λ i → ∀ {A : ℂ .Object} → func→ (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {func* A})
+    : {func* : ℂ .Object → 𝔻 .Object}
-  --     (F .ident) (G .ident))
+      {func→ : {A B : ℂ .Object} → ℂ .Arrow A B → 𝔻 .Arrow (func* A) (func* B)}
-  --   → (eqD : PathP (λ i → {A B C : ℂ .Object} {f : ℂ .Arrow A B} {g : ℂ .Arrow B C}
+      {F G : IsFunctor ℂ 𝔻 func* func→}
-  --     → func→ (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (func→ g) (func→ f))
+    → (eqI
-  --       (F .distrib) (G .distrib))
+      : (λ i → ∀ {A} → func→ (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {func* A})
-  --   → F ≡ G
+        [ F .ident ≡ G .ident ])
-  -- IsFunctor≡ eqI eqD i = record { ident = eqI i ; distrib = eqD i }
+    → (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→ : PathP (λ 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))
-    → (eqI : PathP (λ i → ∀ {A : ℂ .Object} → eq→ i (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {eq* i A})
+    → (eqIsFunctor : (λ i → IsFunctor ℂ 𝔻 (eq* i) (eq→ i)) [ F .isFunctor ≡ G .isFunctor ])
-        (F .isFunctor .ident) (G .isFunctor .ident))
-    → (eqD : PathP (λ i → {A B C : ℂ .Object} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
-      → eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ])
-        (F .isFunctor .distrib) (G .isFunctor .distrib))
     → F ≡ G
-  Functor≡ eq* eq→ eqI eqD i = record { func* = eq* i ; func→ = eq→ i ; isFunctor = record { ident = eqI i ; distrib = eqD i } }
+  Functor≡ eq* eq→ eqIsFunctor i = record { func* = eq* i ; func→ = eq→ i ; isFunctor = eqIsFunctor i }
 
 module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where
   private