From 8ac6b9721392c5ad9e4881e37b07b26e33f7d5d2 Mon Sep 17 00:00:00 2001
From: Andrea Vezzosi <sanzhiyan@gmail.com>
Date: Thu, 29 Mar 2018 00:07:49 +0200
Subject: [PATCH] isProp (Product C A B) setup

---
 src/Cat/Category.agda         |   7 ++
 src/Cat/Category/Product.agda | 213 ++++++++++++++++++----------------
 2 files changed, 120 insertions(+), 100 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 556fbd2..cac045e 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -253,6 +253,10 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
         res : (fx , cx) ≡ (fy , cy)
         res i = fp i , cp i
 
+    -- this needs the univalence of the category
+    propTerminal : isProp Terminal
+    propTerminal = {!!}
+
     -- Merely the dual of the above statement.
     propIsInitial : ∀ I → isProp (IsInitial I)
     propIsInitial I x y i {X} = res X i
@@ -269,6 +273,9 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
         res : (fx , cx) ≡ (fy , cy)
         res i = fp i , cp i
 
+    propInitial : isProp Initial
+    propInitial = {!!}
+
 -- | Propositionality of being a category
 module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
   open RawCategory ℂ
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index a601ca9..d2526b1 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -1,6 +1,7 @@
 {-# OPTIONS --allow-unsolved-metas --cubical #-}
 module Cat.Category.Product where
 
+open import Cubical.NType.Properties
 open import Cat.Prelude hiding (_×_ ; proj₁ ; proj₂)
 import Data.Product as P
 
@@ -128,108 +129,120 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
   raw : RawCategory _ _
   raw = record
     { Object = Σ[ X ∈ ℂ.Object ] ℂ.Arrow X A × ℂ.Arrow X B
-    ; Arrow = λ{ (A , _) (B , _) → ℂ.Arrow A B}
-    ; 𝟙 = λ{ {A , _} → ℂ.𝟙 {A}}
-    ; _∘_ = ℂ._∘_
-    }
-
-  open RawCategory raw
-  open Univalence ℂ.isIdentity
-  open import Cat.Equivalence hiding (_≅_)
-
-  k : {A B : ℂ.Object} → isEquiv (A ≡ B) (A ℂ.≅ B) (ℂ.id-to-iso A B)
-  k = ℂ.univalent
-
-  module _ {X' Y' : Σ[ X ∈ ℂ.Object ] (ℂ [ X , A ] × ℂ [ X , B ])} where
-    open Σ X' renaming (proj₁ to X) using ()
-    open Σ (proj₂ X') renaming (proj₁ to Xxa ; proj₂ to Xxb)
-    open Σ Y' renaming (proj₁ to Y) using ()
-    open Σ (proj₂ Y') renaming (proj₁ to Yxa ; proj₂ to Yxb)
-    module _ (p : X ≡ Y) where
-      D : ∀ y → X ≡ y → Set _
-      D y q = ∀ b → (λ i → ℂ [ q i , A ]) [ Xxa ≡ b ]
-      -- Not sure this is actually provable - but if it were it might involve
-      -- something like the ump of the product -- in which case perhaps the
-      -- objects of the category I'm constructing should not merely be the
-      -- data-part of the product but also the laws.
-
-      -- d : D X refl
-      d : ∀ b → (λ i → ℂ [ X , A ]) [ Xxa ≡ b ]
-      d b = {!!}
-      kk : D Y p
-      kk = pathJ D d Y p
-      a : (λ i → ℂ [ p i , A ]) [ Xxa ≡ Yxa ]
-      a = kk Yxa
-      b : (λ i → ℂ [ p i , B ]) [ Xxb ≡ Yxb ]
-      b = {!!}
-      f : X' ≡ Y'
-      f i = p i , a i , b i
-
-    module _ (p : X' ≡ Y') where
-      g : X ≡ Y
-      g i = proj₁ (p i)
-
-    step0 : (X' ≡ Y') ≃ (X ≡ Y)
-    step0 = Equiv≃.fromIsomorphism _ _ (g , f , record { verso-recto = {!refl!} ; recto-verso = refl})
-
-    step1 : (X ≡ Y) ≃ X ℂ.≅ Y
-    step1 = ℂ.univalent≃
-
-    -- Just a reminder
-    step1-5 : (X' ≅ Y') ≡ (X ℂ.≅ Y)
-    step1-5 = refl
-
-    step2 : (X' ≡ Y') ≃ (X ℂ.≅ Y)
-    step2 = Equivalence.compose step0 step1
-
-    univalent : isEquiv (X' ≡ Y') (X ℂ.≅ Y) (id-to-iso X' Y')
-    univalent = proj₂ step2
-
-  isCategory : IsCategory raw
-  isCategory = record
-    { isAssociative = ℂ.isAssociative
-    ; isIdentity = ℂ.isIdentity
-    ; arrowsAreSets = ℂ.arrowsAreSets
-    ; univalent = univalent
-    }
-
-  category : Category _ _
-  category = record
-    { raw = raw
-    ; isCategory = isCategory
-    }
-
-  open Category category hiding (IsTerminal ; Object)
-
-  -- Essential turns `p : Product ℂ A B` into a triple
-  productObject : Object
-  productObject = Product.object p , Product.proj₁ p , Product.proj₂ p
-
-  productObjectIsTerminal : IsTerminal productObject
-  productObjectIsTerminal = {!!}
-
-  proppp : isProp (IsTerminal productObject)
-  proppp = Propositionality.propIsTerminal productObject
-
-module Try1 {ℓa ℓb : Level} (A B : Set) where
-  open import Data.Product
-  raw : RawCategory _ _
-  raw = record
-    { Object = Σ[ X ∈ Set ] (X → A) × (X → B)
-    ; Arrow = λ{ (X0 , f0 , g0) (X1 , f1 , g1) → X0 → X1}
-    ; 𝟙 = λ x → x
-    ; _∘_ = λ x x₁ x₂ → x (x₁ x₂)
+    ; Arrow = λ{ (X , xa , xb) (Y , ya , yb) → Σ[ xy ∈ ℂ.Arrow X Y ] (ℂ [ ya ∘ xy ] ≡ xa) × (ℂ [ yb ∘ xy ] ≡ xb) }
+    ; 𝟙 = λ{ {A , _} → ℂ.𝟙 {A} , {!!}}
+    ; _∘_ = \ { (f , p) (g , q) → ℂ._∘_ f g , {!!} }
     }
 
   open RawCategory raw
 
-  isCategory : IsCategory raw
-  isCategory = record
-    { isAssociative = refl
-    ; isIdentity = refl , refl
-    ; arrowsAreSets = {!!}
-    ; univalent = {!!}
-    }
+  cat : IsCategory raw
+  cat = {!!}
 
-  t : IsTerminal ((A × B) , proj₁ , proj₂)
-  t = {!!}
+  module cat = IsCategory cat
+
+  lemma :  Terminal ≃ Product ℂ A B
+  lemma = {!!}
+
+  thm : isProp (Product ℂ A B)
+  thm = equivPreservesNType {n = ⟨-1⟩} lemma cat.Propositionality.propTerminal
+
+--   open Univalence ℂ.isIdentity
+--   open import Cat.Equivalence hiding (_≅_)
+
+--   k : {A B : ℂ.Object} → isEquiv (A ≡ B) (A ℂ.≅ B) (ℂ.id-to-iso A B)
+--   k = ℂ.univalent
+
+--   module _ {X' Y' : Σ[ X ∈ ℂ.Object ] (ℂ [ X , A ] × ℂ [ X , B ])} where
+--     open Σ X' renaming (proj₁ to X) using ()
+--     open Σ (proj₂ X') renaming (proj₁ to Xxa ; proj₂ to Xxb)
+--     open Σ Y' renaming (proj₁ to Y) using ()
+--     open Σ (proj₂ Y') renaming (proj₁ to Yxa ; proj₂ to Yxb)
+--     module _ (p : X ≡ Y) where
+--       D : ∀ y → X ≡ y → Set _
+--       D y q = ∀ b → (λ i → ℂ [ q i , A ]) [ Xxa ≡ b ]
+--       -- Not sure this is actually provable - but if it were it might involve
+--       -- something like the ump of the product -- in which case perhaps the
+--       -- objects of the category I'm constructing should not merely be the
+--       -- data-part of the product but also the laws.
+
+--       -- d : D X refl
+--       d : ∀ b → (λ i → ℂ [ X , A ]) [ Xxa ≡ b ]
+--       d b = {!!}
+--       kk : D Y p
+--       kk = pathJ D d Y p
+--       a : (λ i → ℂ [ p i , A ]) [ Xxa ≡ Yxa ]
+--       a = kk Yxa
+--       b : (λ i → ℂ [ p i , B ]) [ Xxb ≡ Yxb ]
+--       b = {!!}
+--       f : X' ≡ Y'
+--       f i = p i , a i , b i
+
+--     module _ (p : X' ≡ Y') where
+--       g : X ≡ Y
+--       g i = proj₁ (p i)
+
+--     step0 : (X' ≡ Y') ≃ (X ≡ Y)
+--     step0 = Equiv≃.fromIsomorphism _ _ (g , f , record { verso-recto = {!refl!} ; recto-verso = refl})
+
+--     step1 : (X ≡ Y) ≃ X ℂ.≅ Y
+--     step1 = ℂ.univalent≃
+
+--     -- Just a reminder
+--     step1-5 : (X' ≅ Y') ≡ (X ℂ.≅ Y)
+--     step1-5 = refl
+
+--     step2 : (X' ≡ Y') ≃ (X ℂ.≅ Y)
+--     step2 = Equivalence.compose step0 step1
+
+--     univalent : isEquiv (X' ≡ Y') (X ℂ.≅ Y) (id-to-iso X' Y')
+--     univalent = proj₂ step2
+
+--   isCategory : IsCategory raw
+--   isCategory = record
+--     { isAssociative = ℂ.isAssociative
+--     ; isIdentity = ℂ.isIdentity
+--     ; arrowsAreSets = ℂ.arrowsAreSets
+--     ; univalent = univalent
+--     }
+
+--   category : Category _ _
+--   category = record
+--     { raw = raw
+--     ; isCategory = isCategory
+--     }
+
+--   open Category category hiding (IsTerminal ; Object)
+
+--   -- Essential turns `p : Product ℂ A B` into a triple
+--   productObject : Object
+--   productObject = Product.object p , Product.proj₁ p , Product.proj₂ p
+
+--   productObjectIsTerminal : IsTerminal productObject
+--   productObjectIsTerminal = {!!}
+
+--   proppp : isProp (IsTerminal productObject)
+--   proppp = Propositionality.propIsTerminal productObject
+
+-- module Try1 {ℓa ℓb : Level} (A B : Set) where
+--   open import Data.Product
+--   raw : RawCategory _ _
+--   raw = record
+--     { Object = Σ[ X ∈ Set ] (X → A) × (X → B)
+--     ; Arrow = λ{ (X0 , f0 , g0) (X1 , f1 , g1) → X0 → X1}
+--     ; 𝟙 = λ x → x
+--     ; _∘_ = λ x x₁ x₂ → x (x₁ x₂)
+--     }
+
+--   open RawCategory raw
+
+--   isCategory : IsCategory raw
+--   isCategory = record
+--     { isAssociative = refl
+--     ; isIdentity = refl , refl
+--     ; arrowsAreSets = {!!}
+--     ; univalent = {!!}
+--     }
+
+--   t : IsTerminal ((A × B) , proj₁ , proj₂)
+--   t = {!!}