Make univalence a submodule of RawCategory

src/Cat/Categories/Cat.agda

@@ -97,7 +97,8 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
     isIdentity
       = Σ≡ (fst ℂ.isIdentity) (fst 𝔻.isIdentity)
       , Σ≡ (snd ℂ.isIdentity) (snd 𝔻.isIdentity)
-    postulate univalent : Univalence.Univalent rawProduct isIdentity
+
+    postulate univalent : Univalence.Univalent isIdentity
     instance
       isCategory : IsCategory rawProduct
       IsCategory.isAssociative isCategory = Σ≡ ℂ.isAssociative 𝔻.isAssociative

src/Cat/Categories/Free.agda

@@ -35,8 +35,6 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     RawCategory._∘_    RawFree = concatenate
 
     open RawCategory RawFree
-    open Univalence  RawFree
-
 
     isAssociative : {A B C D : ℂ.Object} {r : Path ℂ.Arrow A B} {q : Path ℂ.Arrow B C} {p : Path ℂ.Arrow C D}
       → p ++ (q ++ r) ≡ (p ++ q) ++ r
@@ -59,13 +57,16 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     isIdentity : IsIdentity 𝟙
     isIdentity = ident-r , ident-l
 
+    open Univalence isIdentity
+
     module _ {A B : ℂ.Object} where
       arrowsAreSets : Cubical.isSet (Path ℂ.Arrow A B)
       arrowsAreSets a b p q = {!!}
 
-      eqv : isEquiv (A ≡ B) (A ≅ B) (id-to-iso isIdentity A B)
+      eqv : isEquiv (A ≡ B) (A ≅ B) (Univalence.id-to-iso isIdentity A B)
       eqv = {!!}
-    univalent : Univalent isIdentity
+
+    univalent : Univalent
     univalent = eqv
 
     isCategory : IsCategory RawFree

src/Cat/Categories/Fun.agda

@@ -67,7 +67,8 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
     }
 
   open RawCategory RawFun
-  open Univalence  RawFun
+  open Univalence (λ {A} {B} {f} → isIdentity {A} {B} {f})
+
   module _ {A B : Functor ℂ 𝔻} where
     module A = Functor A
     module B = Functor B
@@ -145,10 +146,10 @@ 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) (id-to-iso (λ { {A} {B} → isIdentity {A} {B}}) A B)
+    done : isEquiv (A ≡ B) (A ≅ B) (Univalence.id-to-iso (λ { {A} {B} → isIdentity {A} {B}}) A B)
     done = {!gradLemma obverse reverse ve-re re-ve!}
 
-  univalent : Univalent (λ{ {A} {B} → isIdentity {A} {B}})
+  univalent : Univalent
   univalent = done
 
   instance

src/Cat/Categories/Sets.agda

@@ -69,12 +69,13 @@ module _ (ℓ : Level) where
     RawCategory._∘_    SetsRaw = Function._∘′_
 
     open RawCategory SetsRaw hiding (_∘_)
-    open Univalence  SetsRaw
 
     isIdentity : IsIdentity Function.id
     proj₁ isIdentity = funExt λ _ → refl
     proj₂ isIdentity = funExt λ _ → refl
 
+    open Univalence (λ {A} {B} {f} → isIdentity {A} {B} {f})
+
     arrowsAreSets : ArrowsAreSets
     arrowsAreSets {B = (_ , s)} = setPi λ _ → s
 
@@ -266,7 +267,7 @@ module _ (ℓ : Level) where
       res : isEquiv (hA ≡ hB) (hA ≅ hB) (_≃_.eqv t)
       res = _≃_.isEqv t
     module _ {hA hB : hSet {ℓ}} where
-      univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB)
+      univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (Univalence.id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB)
       univalent = let k = _≃_.isEqv (sym≃ conclusion) in {!k!}
 
     SetsIsCategory : IsCategory SetsRaw

src/Cat/Category.agda

@@ -129,12 +129,8 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   Terminal : Set (ℓa ⊔ ℓb)
   Terminal = Σ Object IsTerminal
 
--- | Univalence is indexed by a raw category as well as an identity proof.
---
--- FIXME Put this in `RawCategory` and index it on the witness to `isIdentity`.
-module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
-  open RawCategory ℂ
-  module _ (isIdentity : IsIdentity 𝟙) where
+  -- | Univalence is indexed by a raw category as well as an identity proof.
+  module Univalence (isIdentity : IsIdentity 𝟙) where
     idIso : (A : Object) → A ≅ A
     idIso A = 𝟙 , (𝟙 , isIdentity)
 
@@ -162,12 +158,13 @@ module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
 -- [HoTT].
 record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
   open RawCategory ℂ public
-  open Univalence  ℂ public
   field
     isAssociative : IsAssociative
     isIdentity    : IsIdentity 𝟙
     arrowsAreSets : ArrowsAreSets
-    univalent     : Univalent isIdentity
+  open Univalence isIdentity public
+  field
+    univalent     : Univalent
 
   -- Some common lemmas about categories.
   module _ {A B : Object} {X : Object} (f : Arrow A B) where
@@ -243,7 +240,7 @@ module Propositionality {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
               𝟙 ∘ g'       ≡⟨ snd isIdentity ⟩
               g'           ∎
 
-    propUnivalent : isProp (Univalent isIdentity)
+    propUnivalent : isProp Univalent
     propUnivalent a b i = propPi (λ iso → propHasLevel ⟨-2⟩) a b i
 
   private
@@ -251,7 +248,7 @@ module Propositionality {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
       module IC = IsCategory
       module X = IsCategory x
       module Y = IsCategory y
-      open Univalence ℂ
+      open Univalence
       -- In a few places I use the result of propositionality of the various
       -- projections of `IsCategory` - I've arbitrarily chosed to use this
       -- result from `x : IsCategory C`. I don't know which (if any) possibly
@@ -336,21 +333,22 @@ module Opposite {ℓa ℓb : Level} where
       RawCategory._∘_    opRaw = Function.flip ℂ._∘_
 
       open RawCategory opRaw
-      open Univalence  opRaw
 
       isIdentity : IsIdentity 𝟙
       isIdentity = swap ℂ.isIdentity
 
+      open Univalence isIdentity
+
       module _ {A B : ℂ.Object} where
         univalent : isEquiv (A ≡ B) (A ≅ B)
-          (id-to-iso (swap ℂ.isIdentity) A B)
+          (Univalence.id-to-iso (swap ℂ.isIdentity) A B)
         fst (univalent iso) = flipFiber (fst (ℂ.univalent (flipIso iso)))
           where
             flipIso : A ≅ B → B ℂ.≅ A
             flipIso (f , f~ , iso) = f , f~ , swap iso
             flipFiber
-              : fiber (ℂ.id-to-iso ℂ.isIdentity B A) (flipIso iso)
-              → fiber (  id-to-iso   isIdentity A B)          iso
+              : fiber (ℂ.id-to-iso B A) (flipIso iso)
+              → fiber (  id-to-iso A B)          iso
             flipFiber (eq , eqIso) = sym eq , {!!}
         snd (univalent iso) = {!!}