Provide preorder instance for some things - more work on product cat

src/Cat/Categories/Rel.agda

@@ -1,7 +1,7 @@
 {-# OPTIONS --cubical --allow-unsolved-metas #-}
 module Cat.Categories.Rel where
 
-open import Cat.Prelude renaming (fst to fst ; snd to snd)
+open import Cat.Prelude hiding (Rel)
 open import Function
 
 open import Cat.Category

src/Cat/Category.agda

@@ -120,6 +120,15 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     Univalent : Set (ℓa ⊔ ℓb)
     Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (idToIso A B)
 
+    import Cat.Equivalence as E
+    open E public using () renaming (Isomorphism to TypeIsomorphism)
+    open E using (module Equiv≃)
+    open Equiv≃ using (fromIso)
+
+    univalenceFromIsomorphism : {A B : Object}
+      → TypeIsomorphism (idToIso A B) → isEquiv (A ≡ B) (A ≅ B) (idToIso A B)
+    univalenceFromIsomorphism = fromIso _ _
+
     -- A perhaps more readable version of univalence:
     Univalent≃ = {A B : Object} → (A ≡ B) ≃ (A ≅ B)
 
@@ -244,6 +253,34 @@ record IsPreCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (ls
       res : (fx , cx) ≡ (fy , cy)
       res i = fp i , cp i
 
+  module _ where
+    private
+      trans≅ : Transitive _≅_
+      trans≅ (f , f~ , f-inv) (g , g~ , g-inv)
+        = g ∘ f
+        , f~ ∘ g~
+        , ( begin
+            (f~ ∘ g~) ∘ (g ∘ f) ≡⟨ isAssociative ⟩
+            (f~ ∘ g~) ∘ g ∘ f ≡⟨ cong (λ φ → φ ∘ f) (sym isAssociative) ⟩
+            f~ ∘ (g~ ∘ g) ∘ f ≡⟨ cong (λ φ → f~ ∘ φ ∘ f) (fst g-inv) ⟩
+            f~ ∘ identity ∘ f ≡⟨ cong (λ φ → φ ∘ f) rightIdentity ⟩
+            f~ ∘ f           ≡⟨ fst f-inv ⟩
+            identity ∎
+          )
+        , ( begin
+            g ∘ f ∘ (f~ ∘ g~) ≡⟨ isAssociative ⟩
+            g ∘ f ∘ f~ ∘ g~ ≡⟨ cong (λ φ → φ ∘ g~) (sym isAssociative) ⟩
+            g ∘ (f ∘ f~) ∘ g~ ≡⟨ cong (λ φ → g ∘ φ ∘ g~) (snd f-inv) ⟩
+            g ∘ identity ∘ g~ ≡⟨ cong (λ φ → φ ∘ g~) rightIdentity ⟩
+            g ∘ g~ ≡⟨ snd g-inv ⟩
+            identity ∎
+          )
+      isPreorder : IsPreorder _≅_
+      isPreorder = record { isEquivalence = equalityIsEquivalence ; reflexive = idToIso _ _ ; trans = trans≅ }
+
+    preorder≅ : Preorder _ _ _
+    preorder≅ = record { Carrier = Object ; _≈_ = _≡_ ; _∼_ = _≅_ ; isPreorder = isPreorder }
+
 record PreCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   field
     raw            : RawCategory ℓa ℓb

src/Cat/Category/Monoid.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module Cat.Category.Monoid where
 
 open import Agda.Primitive
@@ -6,9 +7,10 @@ open import Cat.Category
 open import Cat.Category.Product
 open import Cat.Category.Functor
 import Cat.Categories.Cat as Cat
+open import Cat.Prelude hiding (_×_ ; empty)
 
 -- TODO: Incorrect!
-module _ (ℓa ℓb : Level) where
+module _ {ℓa ℓb : Level} where
   private
     ℓ = lsuc (ℓa ⊔ ℓb)
 
@@ -21,30 +23,34 @@ module _ (ℓa ℓb : Level) where
     _×_ : ∀ {ℓa ℓb} → Category ℓa ℓb → Category ℓa ℓb → Category ℓa ℓb
     ℂ × 𝔻 = Cat.CatProduct.object ℂ 𝔻
 
-  record RawMonoidalCategory : Set ℓ where
+  record RawMonoidalCategory (ℂ : Category ℓa ℓb) : Set ℓ where
+    open Category ℂ public hiding (IsAssociative)
     field
-      category : Category ℓa ℓb
-    open Category category public
-    field
-      {{hasProducts}} : HasProducts category
       empty  : Object
       -- aka. tensor product, monoidal product.
-      append : Functor (category × category) category
+      append : Functor (ℂ × ℂ) ℂ
-    open HasProducts hasProducts public
 
-  record MonoidalCategory : Set ℓ where
+    module F = Functor append
+
+    _⊗_ = append
+    mappend = F.fmap
+
+    IsAssociative : Set _
+    IsAssociative = {A B : Object} → (f g h : Arrow A A) → mappend ({!mappend!} , {!mappend!}) ≡ mappend (f , mappend (g , h))
+
+  record MonoidalCategory (ℂ : Category ℓa ℓb) : Set ℓ where
     field
-      raw : RawMonoidalCategory
+      raw : RawMonoidalCategory ℂ
     open RawMonoidalCategory raw public
 
-module _ {ℓa ℓb : Level} (ℂ : MonoidalCategory ℓa ℓb) where
+module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) {monoidal : MonoidalCategory ℂ} {hasProducts : HasProducts ℂ} where
   private
     ℓ = ℓa ⊔ ℓb
 
-  open MonoidalCategory ℂ public
+  open MonoidalCategory monoidal public hiding (mappend)
+  open HasProducts hasProducts
 
-  record Monoid : Set ℓ where
+  record MonoidalObject (M : Object) : Set ℓ where
     field
-      carrier : Object
+      mempty  : Arrow empty M
-      mempty  : Arrow empty carrier
+      mappend : Arrow (M × M) M
-      mappend : Arrow (carrier × carrier) carrier

src/Cat/Category/Product.agda

@@ -123,6 +123,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
       }
 
     module _ where
+      private
         open RawCategory raw
 
         propEqs : ∀ {X' : Object}{Y' : Object} (let X , xa , xb = X') (let Y , ya , yb = Y')
@@ -171,69 +172,106 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
 
     open IsPreCategory isPreCat
 
-    -- module _ (X : Object) where
-    --   center : Σ Object (X ≅_)
-    --   center = X , idIso X
-
-    --   module _ (y : Σ Object (X ≅_)) where
-    --     open Σ y renaming (fst to Y ; snd to X≅Y)
-
-    --     contractible : (X , idIso X) ≡ (Y , X≅Y)
-    --     contractible = {!!}
-
-    --   univalent[Contr] : isContr (Σ Object (X ≅_))
-    --   univalent[Contr] = center , contractible
-    --   module _ (y : Σ Object (X ≡_)) where
-    --     open Σ y renaming (fst to Y ; snd to p)
-    --     a0 : X ≡ Y
-    --     a0 = {!!}
-    --     a1 : PathP (λ i → X ≡ a0 i) refl p
-    --     a1 = {!!}
-    --       where
-    --       P : (Z : Object) → X ≡ Z → Set _
-    --       P Z p = PathP (λ i → X ≡ Z)
-
-    --     alt' : (X , refl) ≡ y
-    --     alt' i = a0 i , a1 i
-    --   alt : isContr (Σ Object (X ≡_))
-    --   alt = (X , refl) , alt'
-
     univalent : Univalent
-    univalent {X , x} {Y , y} = {!res!}
+    univalent {(X , xa , xb)} {(Y , ya , yb)} = univalenceFromIsomorphism res
       where
-      open import Cat.Equivalence as E hiding (_≅_)
+      open import Cat.Equivalence using (composeIso) renaming (_≅_ to _≈_)
-      open import Cubical.Univalence
+      -- open import Relation.Binary.PreorderReasoning (Cat.Equivalence.preorder≅ {!!}) using ()
-      module _ (c : (X , x) ≅ (Y , y)) where
+      --   renaming
-      -- module _ (c : _ ≅ _) where
+      --     ( _∼⟨_⟩_ to _≈⟨_⟩_
-        open Σ c renaming (fst to f_c ; snd to inv_c)
+      --     ; begin_ to begin!_
-        open Σ inv_c renaming (fst to g_c ; snd to ainv_c)
+      --     ; _∎ to _∎! )
-        open Σ ainv_c renaming (fst to left ; snd to right)
+      -- lawl
-        c0 : X ℂ.≅ Y
+      --   : ((X , xa , xb) ≡ (Y , ya , yb))
-        c0 = fst f_c , fst g_c , (λ i → fst (left i)) , (λ i → fst (right i))
+      --   ≈ (Σ[ iso ∈ (X ℂ.≅ Y) ] let p = ℂ.iso-to-id iso in (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
-        f0 : X ≡ Y
+      -- lawl = {!begin! ? ≈⟨ ? ⟩ ? ∎!!}
-        f0 = ℂ.iso-to-id c0
+      -- Problem with the above approach: Preorders only work for heterogeneous equaluties.
-        module _ {A : ℂ.Object} (α : ℂ.Arrow X A) where
+
-          coedom : ℂ.Arrow Y A
+      -- (X , xa , xb) ≡ (Y , ya , yb)
-          coedom = coe (λ i → ℂ.Arrow (f0 i) A) α
+      -- ≅
-        coex : ℂ.Arrow Y A × ℂ.Arrow Y B
+      -- Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb)
-        coex = coe (λ i → ℂ.Arrow (f0 i) A × ℂ.Arrow (f0 i) B) x
+      -- ≅
-        f1 : PathP (λ i → ℂ.Arrow (f0 i) A × ℂ.Arrow (f0 i) B) x coex
+      -- Σ (X ℂ.≅ Y) (λ iso
-        f1 = {!sym!}
+      --   → let p = ℂ.iso-to-id iso
-        f2 : coex ≡ y
+      --   in
-        f2 = {!!}
+      --   ( PathP (λ i → ℂ.Arrow (p i) A) xa ya)
-        f : (X , x) ≡ (Y , y)
+      --   × PathP (λ i → ℂ.Arrow (p i) B) xb yb
-        f i = f0 i , {!f1 i!}
+      --   )
-      prp : isSet (ℂ.Object × ℂ.Arrow Y A × ℂ.Arrow Y B)
+      -- ≅
-      prp = setSig {sA = {!!}} {(λ _ → setSig {sA = ℂ.arrowsAreSets} {λ _ → ℂ.arrowsAreSets})}
+      -- (X , xa , xb) ≅ (Y , ya , yb)
-      ve-re : (p : (X , x) ≡ (Y , y)) → f (idToIso _ _ p) ≡ p
+      step0
-      -- ve-re p i j = {!ℂ.arrowsAreSets!} , ℂ.arrowsAreSets _ _ (let k = fst (snd (p i)) in {!!}) {!!} {!!} {!!} , {!!}
+        : ((X , xa , xb) ≡ (Y , ya , yb))
-      ve-re p = let k = prp {!!} {!!} {!!} {!p!} in {!!}
+        ≈ (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
-      re-ve : (iso : (X , x) ≅ (Y , y)) → idToIso _ _ (f iso) ≡ iso
+      step0
-      re-ve = {!!}
+        = (λ p → (λ i → fst (p i)) , (λ i → fst (snd (p i))) , (λ i → snd (snd (p i))))
-      iso : E.Isomorphism (idToIso (X , x) (Y , y))
+        , (λ x  → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i))
-      iso = f , record { verso-recto = funExt ve-re ; recto-verso = funExt re-ve }
+        , record
-      res : isEquiv ((X , x) ≡ (Y , y)) ((X , x) ≅ (Y , y)) (idToIso (X , x) (Y , y))
+          { verso-recto = {!!}
-      res = Equiv≃.fromIso _ _ iso
+          ; recto-verso = {!!}
+          }
+      step1
+        : (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
+        ≈ Σ (X ℂ.≅ Y) (λ iso
+          → let p = ℂ.iso-to-id iso
+          in
+          ( PathP (λ i → ℂ.Arrow (p i) A) xa ya)
+          × PathP (λ i → ℂ.Arrow (p i) B) xb yb
+          )
+      step1
+        = (λ{ (p , x) → (ℂ.idToIso _ _ p) , {!snd x!}})
+        -- Goal is:
+        --
+        --     φ x
+        --
+        -- where `x` is
+        --
+        --   ℂ.iso-to-id (ℂ.idToIso _ _ p)
+        --
+        -- I have `φ p` in scope, but surely `p` and `x` are the same - though
+        -- perhaps not definitonally.
+        , (λ{ (iso , x) → ℂ.iso-to-id iso , x})
+        , record { verso-recto = {!!} ; recto-verso = {!!} }
+      lemA : {A B : Object} {f g : Arrow A B} → fst f ≡ fst g → f ≡ g
+      lemA {A} {B} {f = f} {g} p i = p i , h i
+        where
+        h : PathP (λ i →
+            (ℂ [ fst (snd B) ∘ p i ]) ≡ fst (snd A) ×
+            (ℂ [ snd (snd B) ∘ p i ]) ≡ snd (snd A)
+          ) (snd f) (snd g)
+        h = lemPropF (λ a → propSig
+          (ℂ.arrowsAreSets (ℂ [ fst (snd B) ∘ a ]) (fst (snd A)))
+          λ _ → ℂ.arrowsAreSets (ℂ [ snd (snd B) ∘ a ]) (snd (snd A)))
+          p
+      step2
+        : Σ (X ℂ.≅ Y) (λ iso
+          → let p = ℂ.iso-to-id iso
+          in
+          ( PathP (λ i → ℂ.Arrow (p i) A) xa ya)
+          × PathP (λ i → ℂ.Arrow (p i) B) xb yb
+          )
+        ≈ ((X , xa , xb) ≅ (Y , ya , yb))
+      step2
+        = ( λ{ ((f , f~ , inv-f) , x)
+            → ( f , {!!})
+            , ( (f~ , {!!})
+              , lemA {!!}
+              , lemA {!!}
+              )
+            }
+          )
+        , (λ x → {!!})
+        , {!!}
+      -- One thing to watch out for here is that the isomorphisms going forwards
+      -- must compose to give idToIso
+      iso
+        : ((X , xa , xb) ≡ (Y , ya , yb))
+        ≈ ((X , xa , xb) ≅ (Y , ya , yb))
+      iso = step0 ⊙ step1 ⊙ step2
+        where
+        infixl 5 _⊙_
+        _⊙_ = composeIso
+      res : TypeIsomorphism (idToIso (X , xa , xb) (Y , ya , yb))
+      res = {!snd iso!}
 
     isCat : IsCategory raw
     IsCategory.isPreCategory isCat = isPreCat
@@ -346,3 +384,6 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object
 
   propHasProducts : isProp (HasProducts ℂ)
   propHasProducts x y i = record { product = productEq x y i }
+
+fmap≡ : {A : Set} {a0 a1 : A} {B : Set} → (f : A → B) → Path a0 a1 → Path (f a0) (f a1)
+fmap≡ = cong

src/Cat/Equivalence.agda

@@ -7,7 +7,7 @@ open import Cubical.PathPrelude hiding (inverse ; _≃_)
 open import Cubical.PathPrelude using (isEquiv ; isContr ; fiber) public
 open import Cubical.GradLemma
 
-open import Cat.Prelude using (lemPropF ; setPi ; lemSig ; propSet)
+open import Cat.Prelude using (lemPropF ; setPi ; lemSig ; propSet ; Preorder ; equalityIsEquivalence)
 
 module _ {ℓa ℓb : Level} where
   private
@@ -278,6 +278,8 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
       a' = Equiv≃.toIso A B a
       b' = Equiv≃.toIso B C b
 
+  composeIso : {ℓc : Level} {C : Set ℓc} → (A ≅ B) → (B ≅ C) → A ≅ C
+  composeIso {C = C} (f , iso-f) (g , iso-g) = g ∘ f , composeIsomorphism iso-f iso-g
 
   -- Gives the quasi inverse from an equivalence.
   module Equivalence (e : A ≃ B) where
@@ -288,9 +290,6 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
 
     open AreInverses (snd iso) public
 
-    composeIso : {ℓc : Level} {C : Set ℓc} → (B ≅ C) → A ≅ C
-    composeIso {C = C} (g , iso-g) = g ∘ obverse , composeIsomorphism iso iso-g
-
     compose : {ℓc : Level} {C : Set ℓc} → (B ≃ C) → A ≃ C
     compose (f , isEquiv) = f ∘ obverse , composeIsEquiv (snd e) isEquiv
 
@@ -308,6 +307,23 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
       where
       module B≃A = Equiv≃ B A
 
+preorder≅ : (ℓ : Level) → Preorder _ _ _
+preorder≅ ℓ = record
+  { Carrier = Set ℓ ; _≈_ = _≡_ ; _∼_ = _≅_
+  ; isPreorder = record
+    { isEquivalence = equalityIsEquivalence
+    ; reflexive = λ p
+      → coe p
+      , coe (sym p)
+      -- I believe I stashed the proof of this somewhere.
+      , record
+        { verso-recto = {!refl!}
+        ; recto-verso = {!!}
+        }
+    ; trans = composeIso
+    }
+  }
+
 module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
   open import Cubical.PathPrelude renaming (_≃_ to _≃η_)
   open import Cubical.Univalence using (_≃_)

src/Cat/Prelude.agda

@@ -71,3 +71,17 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb} {a b : Σ A B}
   Σ≡ : a ≡ b
   fst (Σ≡ i) = fst≡ i
   snd (Σ≡ i) = snd≡ i
+
+import Relation.Binary
+open Relation.Binary public using (Preorder ; Transitive ; IsEquivalence ; Rel)
+
+equalityIsEquivalence : {ℓ : Level} {A : Set ℓ} → IsEquivalence {A = A} _≡_
+IsEquivalence.refl  equalityIsEquivalence = refl
+IsEquivalence.sym   equalityIsEquivalence = sym
+IsEquivalence.trans equalityIsEquivalence = trans
+
+IsPreorder
+  : {a ℓ : Level} {A : Set a}
+  → (_∼_ : Rel A ℓ) -- The relation.
+  → Set _
+IsPreorder _~_ = Relation.Binary.IsPreorder _≡_ _~_