Add notion of pre-category

src/Cat/Categories/Cat.agda

@@ -72,16 +72,20 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
       = Σ≡ (fst ℂ.isIdentity) (fst 𝔻.isIdentity)
       , Σ≡ (snd ℂ.isIdentity) (snd 𝔻.isIdentity)
 
+    isPreCategory : IsPreCategory rawProduct
+    IsPreCategory.isAssociative isPreCategory = Σ≡ ℂ.isAssociative 𝔻.isAssociative
+    IsPreCategory.isIdentity    isPreCategory = isIdentity
+    IsPreCategory.arrowsAreSets isPreCategory = arrowsAreSets
+
     postulate univalent : Univalence.Univalent isIdentity
-    instance
+
-      isCategory : IsCategory rawProduct
+    isCategory : IsCategory rawProduct
-      IsCategory.isAssociative isCategory = Σ≡ ℂ.isAssociative 𝔻.isAssociative
+    IsCategory.isPreCategory isCategory = isPreCategory
-      IsCategory.isIdentity    isCategory = isIdentity
+    IsCategory.univalent     isCategory = univalent
-      IsCategory.arrowsAreSets isCategory = arrowsAreSets
-      IsCategory.univalent     isCategory = univalent
 
   object : Category ℓ ℓ'
   Category.raw object = rawProduct
+  Category.isCategory object = isCategory
 
   fstF : Functor object ℂ
   fstF = record

src/Cat/Categories/Fam.agda

@@ -35,29 +35,31 @@ module _ (ℓa ℓb : Level) where
 
     open import Cubical.NType.Properties
     open import Cubical.Sigma
-    instance
+
-      isCategory : IsCategory RawFam
+    isPreCategory : IsPreCategory RawFam
-      isCategory = record
+    IsPreCategory.isAssociative isPreCategory
-        { isAssociative = λ {A} {B} {C} {D} {f} {g} {h} → isAssociative {A} {B} {C} {D} {f} {g} {h}
+      {A} {B} {C} {D} {f} {g} {h} = isAssociative {A} {B} {C} {D} {f} {g} {h}
-        ; isIdentity = λ {A} {B} {f} → isIdentity {A} {B} {f = f}
+    IsPreCategory.isIdentity isPreCategory
-        ; arrowsAreSets = λ {
+      {A} {B} {f} = isIdentity {A} {B} {f = f}
-          {((A , hA) , famA)}
+    IsPreCategory.arrowsAreSets isPreCategory
-          {((B , hB) , famB)}
+      {(A , hA) , famA} {(B , hB) , famB}
-            → setSig
+      = setSig
-              {sA = setPi λ _ → hB}
+        {sA = setPi λ _ → hB}
-              {sB = λ f →
+        {sB = λ f →
-                let
+          let
-                  helpr : isSet ((a : A) → fst (famA a) → fst (famB (f a)))
+            helpr : isSet ((a : A) → fst (famA a) → fst (famB (f a)))
-                  helpr = setPi λ a → setPi λ _ → snd (famB (f a))
+            helpr = setPi λ a → setPi λ _ → snd (famB (f a))
-                  -- It's almost like above, but where the first argument is
+            -- It's almost like above, but where the first argument is
-                  -- implicit.
+            -- implicit.
-                  res : isSet ({a : A} → fst (famA a) → fst (famB (f a)))
+            res : isSet ({a : A} → fst (famA a) → fst (famB (f a)))
-                  res = {!!}
+            res = {!!}
-                in res
+          in res
-              }
-          }
-        ; univalent = {!!}
         }
 
+    isCategory : IsCategory RawFam
+    IsCategory.isPreCategory isCategory = isPreCategory
+    IsCategory.univalent     isCategory = {!!}
+
   Fam : Category (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb)
   Category.raw Fam = RawFam
+  Category.isCategory Fam = isCategory

src/Cat/Categories/Free.agda

@@ -61,6 +61,12 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       arrowsAreSets : isSet (Path ℂ.Arrow A B)
       arrowsAreSets a b p q = {!!}
 
+    isPreCategory : IsPreCategory RawFree
+    IsPreCategory.isAssociative isPreCategory {f = f} {g} {h} = isAssociative {r = f} {g} {h}
+    IsPreCategory.isIdentity    isPreCategory = isIdentity
+    IsPreCategory.arrowsAreSets isPreCategory = arrowsAreSets
+
+    module _ {A B : ℂ.Object} where
       eqv : isEquiv (A ≡ B) (A ≅ B) (Univalence.id-to-iso isIdentity A B)
       eqv = {!!}
 
@@ -68,9 +74,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     univalent = eqv
 
     isCategory : IsCategory RawFree
-    IsCategory.isAssociative isCategory {f = f} {g} {h} = isAssociative {r = f} {g} {h}
+    IsCategory.isPreCategory isCategory = isPreCategory
-    IsCategory.isIdentity    isCategory = isIdentity
-    IsCategory.arrowsAreSets isCategory = arrowsAreSets
     IsCategory.univalent     isCategory = univalent
 
   Free : Category _ _

src/Cat/Categories/Fun.agda

@@ -10,20 +10,28 @@ import Cat.Category.NaturalTransformation
 
 module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
   open NaturalTransformation ℂ 𝔻 public hiding (module Properties)
-  open NaturalTransformation.Properties ℂ 𝔻
   private
     module ℂ = Category ℂ
     module 𝔻 = Category 𝔻
 
-    -- Functor categories. Objects are functors, arrows are natural transformations.
+    module _ where
-    raw : RawCategory (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
+      -- Functor categories. Objects are functors, arrows are natural transformations.
-    RawCategory.Object   raw = Functor ℂ 𝔻
+      raw : RawCategory (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
-    RawCategory.Arrow    raw = NaturalTransformation
+      RawCategory.Object   raw = Functor ℂ 𝔻
-    RawCategory.identity raw {F} = identity F
+      RawCategory.Arrow    raw = NaturalTransformation
-    RawCategory._∘_      raw {F} {G} {H} = NT[_∘_] {F} {G} {H}
+      RawCategory.identity raw {F} = identity F
+      RawCategory._∘_      raw {F} {G} {H} = NT[_∘_] {F} {G} {H}
 
-    open RawCategory raw hiding (identity)
+    module _ where
-    open Univalence (λ {A} {B} {f} → isIdentity {F = A} {B} {f})
+      open RawCategory raw hiding (identity)
+      open NaturalTransformation.Properties ℂ 𝔻
+
+      isPreCategory : IsPreCategory raw
+      IsPreCategory.isAssociative isPreCategory {A} {B} {C} {D} = isAssociative {A} {B} {C} {D}
+      IsPreCategory.isIdentity    isPreCategory {A} {B} = isIdentity {A} {B}
+      IsPreCategory.arrowsAreSets isPreCategory {F} {G} = naturalTransformationIsSet {F} {G}
+
+    open IsPreCategory isPreCategory hiding (identity)
 
     module _ (F : Functor ℂ 𝔻) where
       center : Σ[ G ∈ Object ] (F ≅ G)
@@ -167,17 +175,15 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
       re-ve : (x : A ≡ B) → reverse (obverse x) ≡ x
       re-ve = {!!}
 
-      done : isEquiv (A ≡ B) (A ≅ B) (Univalence.id-to-iso (λ { {A} {B} → isIdentity {F = A} {B}}) A B)
+      done : isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
       done = {!gradLemma obverse reverse ve-re re-ve!}
 
-    -- univalent : Univalent
+    univalent : Univalent
-    -- univalent = done
+    univalent = {!done!}
 
     isCategory : IsCategory raw
-    IsCategory.isAssociative isCategory {A} {B} {C} {D} = isAssociative {A} {B} {C} {D}
+    IsCategory.isPreCategory isCategory = isPreCategory
-    IsCategory.isIdentity    isCategory {A} {B} = isIdentity {A} {B}
+    IsCategory.univalent     isCategory = univalent
-    IsCategory.arrowsAreSets isCategory {F} {G} = naturalTransformationIsSet {F} {G}
-    IsCategory.univalent     isCategory = {!!}
 
   Fun : Category (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
   Category.raw        Fun = raw
@@ -199,26 +205,26 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
       ; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H}
       }
 
-    isCategory : IsCategory raw
+  --   isCategory : IsCategory raw
-    isCategory = record
+  --   isCategory = record
-      { isAssociative =
+  --     { isAssociative =
-        λ{ {A} {B} {C} {D} {f} {g} {h}
+  --       λ{ {A} {B} {C} {D} {f} {g} {h}
-        → F.isAssociative {A} {B} {C} {D} {f} {g} {h}
+  --       → F.isAssociative {A} {B} {C} {D} {f} {g} {h}
-        }
+  --       }
-      ; isIdentity =
+  --     ; isIdentity =
-        λ{ {A} {B} {f}
+  --       λ{ {A} {B} {f}
-        → F.isIdentity {A} {B} {f}
+  --       → F.isIdentity {A} {B} {f}
-        }
+  --       }
-      ; arrowsAreSets =
+  --     ; arrowsAreSets =
-        λ{ {A} {B}
+  --       λ{ {A} {B}
-        → F.arrowsAreSets {A} {B}
+  --       → F.arrowsAreSets {A} {B}
-        }
+  --       }
-      ; univalent =
+  --     ; univalent =
-        λ{ {A} {B}
+  --       λ{ {A} {B}
-        → F.univalent {A} {B}
+  --       → F.univalent {A} {B}
-        }
+  --       }
-      }
+  --     }
 
-  Presh : Category (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
+  -- Presh : Category (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
-  Category.raw        Presh = raw
+  -- Category.raw        Presh = raw
-  Category.isCategory Presh = isCategory
+  -- Category.isCategory Presh = isCategory

src/Cat/Categories/Rel.agda

@@ -157,10 +157,12 @@ RawRel = record
   ; _∘_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )}
   }
 
-RawIsCategoryRel : IsCategory RawRel
+isPreCategory : IsPreCategory RawRel
-RawIsCategoryRel = record
+
-  { isAssociative = funExt is-isAssociative
+IsPreCategory.isAssociative isPreCategory = funExt is-isAssociative
-  ; isIdentity = funExt ident-l , funExt ident-r
+IsPreCategory.isIdentity    isPreCategory = funExt ident-l , funExt ident-r
-  ; arrowsAreSets = {!!}
+IsPreCategory.arrowsAreSets isPreCategory = {!!}
-  ; univalent = {!!}
+
-  }
+Rel : PreCategory _ _
+PreCategory.raw Rel = RawRel
+PreCategory.isPreCategory Rel = isPreCategory

src/Cat/Categories/Sets.agda

@@ -34,16 +34,23 @@ module _ (ℓ : Level) where
     RawCategory.identity SetsRaw = Function.id
     RawCategory._∘_      SetsRaw = Function._∘′_
 
-    open RawCategory SetsRaw hiding (_∘_)
+    module _ where
+      private
+        open RawCategory SetsRaw hiding (_∘_)
 
-    isIdentity : IsIdentity Function.id
+        isIdentity : IsIdentity Function.id
-    fst isIdentity = funExt λ _ → refl
+        fst isIdentity = funExt λ _ → refl
-    snd isIdentity = funExt λ _ → refl
+        snd isIdentity = funExt λ _ → refl
 
-    open Univalence (λ {A} {B} {f} → isIdentity {A} {B} {f})
+        arrowsAreSets : ArrowsAreSets
+        arrowsAreSets {B = (_ , s)} = setPi λ _ → s
 
-    arrowsAreSets : ArrowsAreSets
+      isPreCat : IsPreCategory SetsRaw
-    arrowsAreSets {B = (_ , s)} = setPi λ _ → s
+      IsPreCategory.isAssociative isPreCat         = refl
+      IsPreCategory.isIdentity    isPreCat {A} {B} = isIdentity    {A} {B}
+      IsPreCategory.arrowsAreSets isPreCat {A} {B} = arrowsAreSets {A} {B}
+
+    open IsPreCategory isPreCat hiding (_∘_)
 
     isIso = Eqv.Isomorphism
     module _ {hA hB : hSet ℓ} where
@@ -255,9 +262,7 @@ module _ (ℓ : Level) where
     univalent = from[Contr] univalent[Contr]
 
     SetsIsCategory : IsCategory SetsRaw
-    IsCategory.isAssociative SetsIsCategory = refl
+    IsCategory.isPreCategory SetsIsCategory = isPreCat
-    IsCategory.isIdentity    SetsIsCategory {A} {B} = isIdentity    {A} {B}
-    IsCategory.arrowsAreSets SetsIsCategory {A} {B} = arrowsAreSets {A} {B}
     IsCategory.univalent     SetsIsCategory = univalent
 
   𝓢𝓮𝓽 Sets : Category (lsuc ℓ) ℓ

src/Cat/Category.agda

@@ -203,15 +203,13 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
 --
 -- Sans `univalent` this would be what is referred to as a pre-category in
 -- [HoTT].
-record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
+record IsPreCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
   open RawCategory ℂ public
   field
     isAssociative : IsAssociative
     isIdentity    : IsIdentity identity
     arrowsAreSets : ArrowsAreSets
   open Univalence isIdentity public
-  field
-    univalent     : Univalent
 
   leftIdentity : {A B : Object} {f : Arrow A B} → identity ∘ f ≡ f
   leftIdentity {A} {B} {f} = fst (isIdentity {A = A} {B} {f})
@@ -251,6 +249,83 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
     iso→epi×mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
     iso→epi×mono iso = iso→epi iso , iso→mono iso
 
+  propIsAssociative : isProp IsAssociative
+  propIsAssociative x y i = arrowsAreSets _ _ x y i
+
+  propIsIdentity : ∀ {f : ∀ {A} → Arrow A A} → isProp (IsIdentity f)
+  propIsIdentity a b i
+    = arrowsAreSets _ _ (fst a) (fst b) i
+    , arrowsAreSets _ _ (snd a) (snd b) i
+
+  propArrowIsSet : isProp (∀ {A B} → isSet (Arrow A B))
+  propArrowIsSet a b i = isSetIsProp a b i
+
+  propIsInverseOf : ∀ {A B f g} → isProp (IsInverseOf {A} {B} f g)
+  propIsInverseOf x y = λ i →
+    let
+      h : fst x ≡ fst y
+      h = arrowsAreSets _ _ (fst x) (fst y)
+      hh : snd x ≡ snd y
+      hh = arrowsAreSets _ _ (snd x) (snd y)
+    in h i , hh i
+
+  module _ {A B : Object} {f : Arrow A B} where
+    isoIsProp : isProp (Isomorphism f)
+    isoIsProp a@(g , η , ε) a'@(g' , η' , ε') =
+      lemSig (λ g → propIsInverseOf) a a' geq
+        where
+          geq : g ≡ g'
+          geq = begin
+            g             ≡⟨ sym rightIdentity ⟩
+            g ∘ identity  ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩
+            g ∘ (f ∘ g')  ≡⟨ isAssociative ⟩
+            (g ∘ f) ∘ g'  ≡⟨ cong (λ φ → φ ∘ g') η ⟩
+            identity ∘ g' ≡⟨ leftIdentity ⟩
+            g'            ∎
+
+  propIsInitial : ∀ I → isProp (IsInitial I)
+  propIsInitial I x y i {X} = res X i
+    where
+    module _ (X : Object) where
+      open Σ (x {X}) renaming (fst to fx ; snd to cx)
+      open Σ (y {X}) renaming (fst to fy ; snd to cy)
+      fp : fx ≡ fy
+      fp = cx fy
+      prop : (x : Arrow I X) → isProp (∀ f → x ≡ f)
+      prop x = propPi (λ y → arrowsAreSets x y)
+      cp : (λ i → ∀ f → fp i ≡ f) [ cx ≡ cy ]
+      cp = lemPropF prop fp
+      res : (fx , cx) ≡ (fy , cy)
+      res i = fp i , cp i
+
+  propIsTerminal : ∀ T → isProp (IsTerminal T)
+  propIsTerminal T x y i {X} = res X i
+    where
+    module _ (X : Object) where
+      open Σ (x {X}) renaming (fst to fx ; snd to cx)
+      open Σ (y {X}) renaming (fst to fy ; snd to cy)
+      fp : fx ≡ fy
+      fp = cx fy
+      prop : (x : Arrow X T) → isProp (∀ f → x ≡ f)
+      prop x = propPi (λ y → arrowsAreSets x y)
+      cp : (λ i → ∀ f → fp i ≡ f) [ cx ≡ cy ]
+      cp = lemPropF prop fp
+      res : (fx , cx) ≡ (fy , cy)
+      res i = fp i , cp i
+
+record PreCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
+  field
+    raw            : RawCategory ℓa ℓb
+    isPreCategory  : IsPreCategory raw
+  open IsPreCategory isPreCategory public
+
+record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
+  field
+    isPreCategory : IsPreCategory ℂ
+  open IsPreCategory isPreCategory public
+  field
+    univalent : Univalent
+
   -- | The formulation of univalence expressed with _≃_ is trivially admissable -
   -- just "forget" the equivalence.
   univalent≃ : Univalent≃
@@ -264,58 +339,9 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
 
   -- | All projections are propositions.
   module Propositionality where
-    propIsAssociative : isProp IsAssociative
-    propIsAssociative x y i = arrowsAreSets _ _ x y i
-
-    propIsIdentity : ∀ {f : ∀ {A} → Arrow A A} → isProp (IsIdentity f)
-    propIsIdentity a b i
-      = arrowsAreSets _ _ (fst a) (fst b) i
-      , arrowsAreSets _ _ (snd a) (snd b) i
-
-    propArrowIsSet : isProp (∀ {A B} → isSet (Arrow A B))
-    propArrowIsSet a b i = isSetIsProp a b i
-
-    propIsInverseOf : ∀ {A B f g} → isProp (IsInverseOf {A} {B} f g)
-    propIsInverseOf x y = λ i →
-      let
-        h : fst x ≡ fst y
-        h = arrowsAreSets _ _ (fst x) (fst y)
-        hh : snd x ≡ snd y
-        hh = arrowsAreSets _ _ (snd x) (snd y)
-      in h i , hh i
-
-    module _ {A B : Object} {f : Arrow A B} where
-      isoIsProp : isProp (Isomorphism f)
-      isoIsProp a@(g , η , ε) a'@(g' , η' , ε') =
-        lemSig (λ g → propIsInverseOf) a a' geq
-          where
-            geq : g ≡ g'
-            geq = begin
-              g             ≡⟨ sym rightIdentity ⟩
-              g ∘ identity  ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩
-              g ∘ (f ∘ g')  ≡⟨ isAssociative ⟩
-              (g ∘ f) ∘ g'  ≡⟨ cong (λ φ → φ ∘ g') η ⟩
-              identity ∘ g' ≡⟨ leftIdentity ⟩
-              g'            ∎
-
     propUnivalent : isProp Univalent
     propUnivalent a b i = propPi (λ iso → propIsContr) a b i
 
-    propIsTerminal : ∀ T → isProp (IsTerminal T)
-    propIsTerminal T x y i {X} = res X i
-      where
-      module _ (X : Object) where
-        open Σ (x {X}) renaming (fst to fx ; snd to cx)
-        open Σ (y {X}) renaming (fst to fy ; snd to cy)
-        fp : fx ≡ fy
-        fp = cx fy
-        prop : (x : Arrow X T) → isProp (∀ f → x ≡ f)
-        prop x = propPi (λ y → arrowsAreSets x y)
-        cp : (λ i → ∀ f → fp i ≡ f) [ cx ≡ cy ]
-        cp = lemPropF prop fp
-        res : (fx , cx) ≡ (fy , cy)
-        res i = fp i , cp i
-
     -- | Terminal objects are propositional - a.k.a uniqueness of terminal
     -- | objects.
     --
@@ -353,20 +379,6 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
       res i = p0 i , p1 i
 
     -- Merely the dual of the above statement.
-    propIsInitial : ∀ I → isProp (IsInitial I)
-    propIsInitial I x y i {X} = res X i
-      where
-      module _ (X : Object) where
-        open Σ (x {X}) renaming (fst to fx ; snd to cx)
-        open Σ (y {X}) renaming (fst to fy ; snd to cy)
-        fp : fx ≡ fy
-        fp = cx fy
-        prop : (x : Arrow I X) → isProp (∀ f → x ≡ f)
-        prop x = propPi (λ y → arrowsAreSets x y)
-        cp : (λ i → ∀ f → fp i ≡ f) [ cx ≡ cy ]
-        cp = lemPropF prop fp
-        res : (fx , cx) ≡ (fy , cy)
-        res i = fp i , cp i
 
     propInitial : isProp Initial
     propInitial Xi Yi = res
@@ -404,6 +416,23 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
   open RawCategory ℂ
   open Univalence
   private
+    module _ (x y : IsPreCategory ℂ) where
+      module x = IsPreCategory x
+      module y = IsPreCategory y
+      -- In a few places I use the result of propositionality of the various
+      -- projections of `IsCategory` - Here I arbitrarily chose to use this
+      -- result from `x : IsCategory C`. I don't know which (if any) possibly
+      -- adverse effects this may have.
+      -- module Prop = X.Propositionality
+
+      propIsPreCategory : x ≡ y
+      IsPreCategory.isAssociative (propIsPreCategory i)
+        = x.propIsAssociative x.isAssociative y.isAssociative i
+      IsPreCategory.isIdentity    (propIsPreCategory i)
+        = x.propIsIdentity x.isIdentity y.isIdentity i
+      IsPreCategory.arrowsAreSets (propIsPreCategory i)
+        = x.propArrowIsSet x.arrowsAreSets y.arrowsAreSets i
+
     module _ (x y : IsCategory ℂ) where
       module X = IsCategory x
       module Y = IsCategory y
@@ -414,7 +443,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
       module Prop = X.Propositionality
 
       isIdentity : (λ _ → IsIdentity identity) [ X.isIdentity ≡ Y.isIdentity ]
-      isIdentity = Prop.propIsIdentity X.isIdentity Y.isIdentity
+      isIdentity = X.propIsIdentity X.isIdentity Y.isIdentity
 
       U : ∀ {a : IsIdentity identity}
         → (λ _ → IsIdentity identity) [ X.isIdentity ≡ a ]
@@ -434,10 +463,13 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
       eqUni : U isIdentity Y.univalent
       eqUni = helper Y.univalent
       done : x ≡ y
-      IsCategory.isAssociative (done i) = Prop.propIsAssociative X.isAssociative Y.isAssociative i
+      IsCategory.isPreCategory (done i)
-      IsCategory.isIdentity    (done i) = isIdentity i
+        = propIsPreCategory X.isPreCategory Y.isPreCategory i
-      IsCategory.arrowsAreSets (done i) = Prop.propArrowIsSet X.arrowsAreSets Y.arrowsAreSets i
       IsCategory.univalent     (done i) = eqUni i
+      -- IsCategory.isAssociative (done i) = Prop.propIsAssociative X.isAssociative Y.isAssociative i
+      -- IsCategory.isIdentity    (done i) = isIdentity i
+      -- IsCategory.arrowsAreSets (done i) = Prop.propArrowIsSet X.arrowsAreSets Y.arrowsAreSets i
+      -- IsCategory.univalent     (done i) = eqUni i
 
   propIsCategory : isProp (IsCategory ℂ)
   propIsCategory = done
@@ -486,19 +518,25 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
 module Opposite {ℓa ℓb : Level} where
   module _ (ℂ : Category ℓa ℓb) where
     private
-      module ℂ = Category ℂ
+      module _ where
-      opRaw : RawCategory ℓa ℓb
+        module ℂ = Category ℂ
-      RawCategory.Object   opRaw = ℂ.Object
+        opRaw : RawCategory ℓa ℓb
-      RawCategory.Arrow    opRaw = Function.flip ℂ.Arrow
+        RawCategory.Object   opRaw = ℂ.Object
-      RawCategory.identity opRaw = ℂ.identity
+        RawCategory.Arrow    opRaw = Function.flip ℂ.Arrow
-      RawCategory._∘_      opRaw = Function.flip ℂ._∘_
+        RawCategory.identity opRaw = ℂ.identity
+        RawCategory._∘_      opRaw = Function.flip ℂ._∘_
 
-      open RawCategory opRaw
+        open RawCategory opRaw
 
-      isIdentity : IsIdentity identity
+        isIdentity : IsIdentity identity
-      isIdentity = swap ℂ.isIdentity
+        isIdentity = swap ℂ.isIdentity
 
-      open Univalence isIdentity
+        isPreCategory : IsPreCategory opRaw
+        IsPreCategory.isAssociative isPreCategory = sym ℂ.isAssociative
+        IsPreCategory.isIdentity isPreCategory = isIdentity
+        IsPreCategory.arrowsAreSets isPreCategory = ℂ.arrowsAreSets
+
+      open IsPreCategory isPreCategory
 
       module _ {A B : ℂ.Object} where
         open import Cat.Equivalence as Equivalence hiding (_≅_)
@@ -571,9 +609,7 @@ module Opposite {ℓa ℓb : Level} where
         univalent = Equiv≃.fromIso _ _ h
 
       isCategory : IsCategory opRaw
-      IsCategory.isAssociative isCategory = sym ℂ.isAssociative
+      IsCategory.isPreCategory isCategory = isPreCategory
-      IsCategory.isIdentity    isCategory = isIdentity
-      IsCategory.arrowsAreSets isCategory = ℂ.arrowsAreSets
       IsCategory.univalent     isCategory = univalent
 
     opposite : Category ℓa ℓb

src/Cat/Category/Product.agda

@@ -122,48 +122,54 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
         }
       }
 
-    open RawCategory raw
+    module _ where
+      open RawCategory raw
 
-    propEqs : ∀ {X' : Object}{Y' : Object} (let X , xa , xb = X') (let Y , ya , yb = Y')
+      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)
+                → (xy : ℂ.Arrow X Y) → isProp (ℂ [ ya ∘ xy ] ≡ xa × ℂ [ yb ∘ xy ] ≡ xb)
-    propEqs xs = propSig (ℂ.arrowsAreSets _ _) (\ _ → ℂ.arrowsAreSets _ _)
+      propEqs xs = propSig (ℂ.arrowsAreSets _ _) (\ _ → ℂ.arrowsAreSets _ _)
 
-    isAssocitaive : IsAssociative
+      isAssociative : IsAssociative
-    isAssocitaive {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
+      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
+        = 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
         where
-        L = identity ∘ (f , f0 , f1)
+        l = hh ∘ (gg ∘ ff)
-        R : Arrow AA BB
+        r = hh ∘ gg ∘ ff
-        R = f , f0 , f1
+        -- s0 : h ℂ.∘ (g ℂ.∘ f) ≡ h ℂ.∘ g ℂ.∘ f
-        l : fst L ≡ fst R
+        s0 : fst l ≡ fst r
-        l = ℂ.leftIdentity
+        s0 = ℂ.isAssociative {f = f} {g} {h}
-      rightIdentity : (f , f0 , f1) ∘ identity ≡ (f , f0 , f1)
+
-      rightIdentity i = l i , lemPropF propEqs l {snd L} {snd R} i
+
+      isIdentity : IsIdentity identity
+      isIdentity {AA@(A , a0 , a1)} {BB@(B , b0 , b1)} {f , f0 , f1} = leftIdentity , rightIdentity
         where
-        L = (f , f0 , f1) ∘ identity
+        leftIdentity : identity ∘ (f , f0 , f1) ≡ (f , f0 , f1)
-        R : Arrow AA BB
+        leftIdentity i = l i , lemPropF propEqs l {snd L} {snd R} i
-        R = (f , f0 , f1)
+          where
-        l : ℂ [ f ∘ ℂ.identity ] ≡ f
+          L = identity ∘ (f , f0 , f1)
-        l = ℂ.rightIdentity
+          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 : ArrowsAreSets
-    arrowsAreSets {X , x0 , x1} {Y , y0 , y1}
+      arrowsAreSets {X , x0 , x1} {Y , y0 , y1}
-      = sigPresNType {n = ⟨0⟩} ℂ.arrowsAreSets λ a → propSet (propEqs _)
+        = sigPresNType {n = ⟨0⟩} ℂ.arrowsAreSets λ a → propSet (propEqs _)
 
-    open Univalence isIdentity
+      isPreCat : IsPreCategory raw
+      IsPreCategory.isAssociative isPreCat = isAssociative
+      IsPreCategory.isIdentity    isPreCat = isIdentity
+      IsPreCategory.arrowsAreSets isPreCat = arrowsAreSets
+
+    open IsPreCategory isPreCat
 
     -- module _ (X : Object) where
     --   center : Σ Object (X ≅_)
@@ -327,12 +333,8 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
       res = Equiv≃.fromIso _ _ iso
 
     isCat : IsCategory raw
-    isCat = record
+    IsCategory.isPreCategory isCat = isPreCat
-      { isAssociative = isAssocitaive
+    IsCategory.univalent     isCat = univalent
-      ; isIdentity    = isIdentity
-      ; arrowsAreSets = arrowsAreSets
-      ; univalent     = univalent
-      }
 
     cat : Category _ _
     cat = record