Merge branch 'Saizan-master' into dev

src/Cat.agda

@@ -8,7 +8,7 @@ import Cat.Category.Bij
 import Cat.Category.Free
 import Cat.Category.Properties
 import Cat.Categories.Sets
-import Cat.Categories.Cat
+-- import Cat.Categories.Cat
 import Cat.Categories.Rel
 import Cat.Categories.Fun
 import Cat.Categories.Cube

src/Cat/Categories/Cat.agda

@@ -1,3 +1,4 @@
+-- There is no category of categories in our interpretation
 {-# OPTIONS --cubical --allow-unsolved-metas #-}
 
 module Cat.Categories.Cat where

src/Cat/Categories/Rel.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --cubical --allow-unsolved-metas #-}
 module Cat.Categories.Rel where
 
 open import Cubical
@@ -160,5 +160,10 @@ Rel = record
   ; Arrow = λ S R → Subset (S × R)
   ; 𝟙 = λ {S} → Diag S
   ; _∘_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )}
-  ; isCategory = record { assoc = funExt is-assoc ; ident = funExt ident-l , funExt ident-r }
+  ; isCategory = record
+    { assoc = funExt is-assoc
+    ; ident = funExt ident-l , funExt ident-r
+    ; arrow-is-set = {!!}
+    ; univalent = {!!}
+    }
   }

src/Cat/Categories/Sets.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module Cat.Categories.Sets where
 
 open import Cubical

src/Cat/Category.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --allow-unsolved-metas --cubical #-}
 
 module Cat.Category where
 
@@ -22,23 +22,65 @@ open import Cubical
 
 syntax ∃!-syntax (λ x → B) = ∃![ x ] B
 
--- All projections must be `isProp`'s
+-- Thierry: All projections must be `isProp`'s
+
+-- According to definitions 9.1.1 and 9.1.6 in the HoTT book the
+-- arrows of a category form a set (arrow-is-set), and there is an
+-- equivalence between the equality of objects and isomorphisms
+-- (univalent).
 record IsCategory {ℓ ℓ' : Level}
   (Object : Set ℓ)
   (Arrow  : Object → Object → Set ℓ')
   (𝟙      : {o : Object} → Arrow o o)
-  (_⊕_    : { a b c : Object } → Arrow b c → Arrow a b → Arrow a c)
+  (_∘_    : { a b c : Object } → Arrow b c → Arrow a b → Arrow a c)
   : Set (lsuc (ℓ' ⊔ ℓ)) where
   field
     assoc : {A B C D : Object} { f : Arrow A B } { g : Arrow B C } { h : Arrow C D }
-      → h ⊕ (g ⊕ f) ≡ (h ⊕ g) ⊕ f
+      → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
     ident : {A B : Object} {f : Arrow A B}
-      → f ⊕ 𝟙 ≡ f × 𝟙 ⊕ f ≡ f
+      → f ∘ 𝟙 ≡ f × 𝟙 ∘ f ≡ f
+    arrow-is-set : ∀ {A B : Object} → isSet (Arrow A B)
+
+  Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓ'
+  Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙
+
+  _≅_ : (A B : Object) → Set ℓ'
+  _≅_ A B = Σ[ f ∈ Arrow A B ] (Isomorphism f)
+
+  idIso : (A : Object) → A ≅ A
+  idIso A = 𝟙 , (𝟙 , ident)
+
+  id-to-iso : (A B : Object) → A ≡ B → A ≅ B
+  id-to-iso A B eq = transp (\ i → A ≅ eq i) (idIso A)
+
+
+  -- TODO: might want to implement isEquiv differently, there are 3
+  -- equivalent formulations in the book.
+  field
+    univalent : {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
+
+  module _ {A B : Object} where
+    Epimorphism : {X : Object } → (f : Arrow A B) → Set ℓ'
+    Epimorphism {X} f = ( g₀ g₁ : Arrow B X ) → g₀ ∘ f ≡ g₁ ∘ f → g₀ ≡ g₁
+
+    Monomorphism : {X : Object} → (f : Arrow A B) → Set ℓ'
+    Monomorphism {X} f = ( g₀ g₁ : Arrow X A ) → f ∘ g₀ ≡ f ∘ g₁ → g₀ ≡ g₁
+
+module _  {ℓ} {ℓ'} {Object : Set ℓ}
+   {Arrow  : Object → Object → Set ℓ'}
+   {𝟙      : {o : Object} → Arrow o o}
+   {_⊕_ : { a b c : Object } → Arrow b c → Arrow a b → Arrow a c}
+    where
+
+  -- TODO, provable by using arrow-is-set and that isProp (isEquiv _ _ _)
+  -- This lemma will be useful to prove the equality of two categories.
+  IsCategory-is-prop : isProp (IsCategory Object Arrow 𝟙 _⊕_)
+  IsCategory-is-prop = {!!}
 
--- open IsCategory public
 
 record Category (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
   -- adding no-eta-equality can speed up type-checking.
+  -- ONLY IF you define your categories with copatterns though.
   no-eta-equality
   field
     -- Need something like:
@@ -64,23 +106,6 @@ _[_,_] = Arrow
 _[_∘_] : ∀ {ℓ ℓ'} → (ℂ : Category ℓ ℓ') → {A B C : ℂ .Object} → (g : ℂ [ B , C ]) → (f : ℂ [ A , B ]) → ℂ [ A , C ]
 _[_∘_] = _∘_
 
-
-
-module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} where
-  module _ { A B : ℂ .Object } where
-    Isomorphism : (f : ℂ .Arrow A B) → Set ℓ'
-    Isomorphism f = Σ[ g ∈ ℂ .Arrow B A ] ℂ [ g ∘ f ] ≡ ℂ .𝟙 × ℂ [ f ∘ g ] ≡ ℂ .𝟙
-
-    Epimorphism : {X : ℂ .Object } → (f : ℂ .Arrow A B) → Set ℓ'
-    Epimorphism {X} f = ( g₀ g₁ : ℂ .Arrow B X ) → ℂ [ g₀ ∘ f ] ≡ ℂ [ g₁ ∘ f ] → g₀ ≡ g₁
-
-    Monomorphism : {X : ℂ .Object} → (f : ℂ .Arrow A B) → Set ℓ'
-    Monomorphism {X} f = ( g₀ g₁ : ℂ .Arrow X A ) → ℂ [ f ∘ g₀ ] ≡ ℂ [ f ∘ g₁ ] → g₀ ≡ g₁
-
-  -- Isomorphism of objects
-  _≅_ : (A B : Object ℂ) → Set ℓ'
-  _≅_ A B = Σ[ f ∈ ℂ .Arrow A B ] (Isomorphism f)
-
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} where
   IsProduct : (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) → Set (ℓ ⊔ ℓ')
   IsProduct π₁ π₂
@@ -130,7 +155,9 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
       ; Arrow = Function.flip (ℂ .Arrow)
       ; 𝟙 = ℂ .𝟙
       ; _∘_ = Function.flip (ℂ ._∘_)
-      ; isCategory = record { assoc = sym assoc ; ident = swap ident }
+      ; isCategory = record { assoc = sym assoc ; ident = swap ident
+                            ; arrow-is-set = {!!}
+                            ; univalent = {!!} }
       }
       where
         open IsCategory (ℂ .isCategory)

src/Cat/Category/Free.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module Cat.Category.Free where
 
 open import Agda.Primitive
@@ -32,5 +33,10 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
     ; Arrow = Path
     ; 𝟙 = λ {o} → emptyPath o
     ; _∘_ = λ {a b c} → concatenate {a} {b} {c}
-    ; isCategory = record { assoc = p-assoc ; ident = ident-r , ident-l }
+    ; isCategory = record
+      { assoc = p-assoc
+      ; ident = ident-r , ident-l
+      ; arrow-is-set = {!!}
+      ; univalent = {!!}
+      }
     }

src/Cat/Category/Properties.agda

@@ -16,7 +16,7 @@ module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : ℂ .Category.Obje
   open Category ℂ
   open IsCategory (isCategory)
 
-  iso-is-epi : Isomorphism {ℂ = ℂ} f → Epimorphism {ℂ = ℂ} {X = X} f
+  iso-is-epi : Isomorphism f → Epimorphism {X = X} f
   iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin
     g₀              ≡⟨ sym (proj₁ ident) ⟩
     g₀ ∘ 𝟙          ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩
@@ -27,7 +27,7 @@ module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : ℂ .Category.Obje
     g₁ ∘ 𝟙          ≡⟨ proj₁ ident ⟩
     g₁              ∎
 
-  iso-is-mono : Isomorphism {ℂ = ℂ} f → Monomorphism {ℂ = ℂ} {X = X} f
+  iso-is-mono : Isomorphism f → Monomorphism {X = X} f
   iso-is-mono (f- , (left-inv , right-inv)) g₀ g₁ eq =
     begin
     g₀            ≡⟨ sym (proj₂ ident) ⟩
@@ -39,7 +39,7 @@ module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : ℂ .Category.Obje
     𝟙 ∘ g₁        ≡⟨ proj₂ ident ⟩
     g₁            ∎
 
-  iso-is-epi-mono : Isomorphism {ℂ = ℂ} f → Epimorphism {ℂ = ℂ} {X = X} f × Monomorphism {ℂ = ℂ} {X = X} f
+  iso-is-epi-mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
   iso-is-epi-mono iso = iso-is-epi iso , iso-is-mono iso
 
 {-
@@ -54,71 +54,71 @@ open Category
 open import Cat.Functor
 open Functor
 
-module _ {ℓ : Level} {ℂ : Category ℓ ℓ}
-  {isSObj : isSet (ℂ .Object)}
-  {isz2 : ∀ {ℓ} → {A B : Set ℓ} → isSet (Sets [ A , B ])} where
-  open import Cat.Categories.Cat using (Cat)
-  open import Cat.Categories.Fun
-  open import Cat.Categories.Sets
-  module Cat = Cat.Categories.Cat
-  open Exponential
-  private
-    Catℓ = Cat ℓ ℓ
-    prshf = presheaf {ℂ = ℂ}
-    module ℂ = IsCategory (ℂ .isCategory)
+-- module _ {ℓ : Level} {ℂ : Category ℓ ℓ}
+--   {isSObj : isSet (ℂ .Object)}
+--   {isz2 : ∀ {ℓ} → {A B : Set ℓ} → isSet (Sets [ A , B ])} where
+--   -- open import Cat.Categories.Cat using (Cat)
+--   open import Cat.Categories.Fun
+--   open import Cat.Categories.Sets
+--   -- module Cat = Cat.Categories.Cat
+--   open Exponential
+--   private
+--     Catℓ = Cat ℓ ℓ
+--     prshf = presheaf {ℂ = ℂ}
+--     module ℂ = IsCategory (ℂ .isCategory)
 
-    -- Exp : Set (lsuc (lsuc ℓ))
-    -- Exp = Exponential (Cat (lsuc ℓ) ℓ)
-    --   Sets (Opposite ℂ)
+--     -- Exp : Set (lsuc (lsuc ℓ))
+--     -- Exp = Exponential (Cat (lsuc ℓ) ℓ)
+--     --   Sets (Opposite ℂ)
 
-    _⇑_ : (A B : Catℓ .Object) → Catℓ .Object
-    A ⇑ B = (exponent A B) .obj
-      where
-        open HasExponentials (Cat.hasExponentials ℓ)
+--     _⇑_ : (A B : Catℓ .Object) → Catℓ .Object
+--     A ⇑ B = (exponent A B) .obj
+--       where
+--         open HasExponentials (Cat.hasExponentials ℓ)
 
-    module _ {A B : ℂ .Object} (f : ℂ .Arrow A B) where
-      :func→: : NaturalTransformation (prshf A) (prshf B)
-      :func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ _ → ℂ.assoc
+--     module _ {A B : ℂ .Object} (f : ℂ .Arrow A B) where
+--       :func→: : NaturalTransformation (prshf A) (prshf B)
+--       :func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ _ → ℂ.assoc
 
-    module _ {c : ℂ .Object} where
-      eqTrans : (λ _ → Transformation (prshf c) (prshf c))
-        [ (λ _ x → ℂ [ ℂ .𝟙 ∘ x ]) ≡ identityTrans (prshf c) ]
-      eqTrans = funExt λ x → funExt λ x → ℂ.ident .proj₂
+--     module _ {c : ℂ .Object} where
+--       eqTrans : (λ _ → Transformation (prshf c) (prshf c))
+--         [ (λ _ x → ℂ [ ℂ .𝟙 ∘ x ]) ≡ identityTrans (prshf c) ]
+--       eqTrans = funExt λ x → funExt λ x → ℂ.ident .proj₂
 
-      eqNat : (λ i → Natural (prshf c) (prshf c) (eqTrans i))
-        [(λ _ → funExt (λ _ → ℂ.assoc)) ≡ identityNatural (prshf c)]
-      eqNat = λ i {A} {B} f →
-        let
-         open IsCategory (Sets .isCategory)
-         lemm : (Sets [ eqTrans i B ∘ prshf c .func→ f ]) ≡
-           (Sets [ prshf c .func→ f ∘ eqTrans i A ])
-         lemm = {!!}
-         lem : (λ _ → Sets [ Functor.func* (prshf c) A , prshf c .func* B ])
-                [ Sets [ eqTrans i B ∘ prshf c .func→ f ]
-                ≡ Sets [ prshf c .func→ f ∘ eqTrans i A ] ]
-         lem
-          = isz2 _ _ lemm _ i
-            -- (Sets [ eqTrans i B ∘ prshf c .func→ f ])
-            -- (Sets [ prshf c .func→ f ∘ eqTrans i A ])
-            -- lemm
-            -- _ i
-        in
-          lem
-      -- eqNat = λ {A} {B} i ℂ[B,A] i' ℂ[A,c] →
-      --   let
-      --     k : ℂ [ {!!} , {!!} ]
-      --     k = ℂ[A,c]
-      --   in {!ℂ [ ? ∘ ? ]!}
+--       eqNat : (λ i → Natural (prshf c) (prshf c) (eqTrans i))
+--         [(λ _ → funExt (λ _ → ℂ.assoc)) ≡ identityNatural (prshf c)]
+--       eqNat = λ i {A} {B} f →
+--         let
+--          open IsCategory (Sets .isCategory)
+--          lemm : (Sets [ eqTrans i B ∘ prshf c .func→ f ]) ≡
+--            (Sets [ prshf c .func→ f ∘ eqTrans i A ])
+--          lemm = {!!}
+--          lem : (λ _ → Sets [ Functor.func* (prshf c) A , prshf c .func* B ])
+--                 [ Sets [ eqTrans i B ∘ prshf c .func→ f ]
+--                 ≡ Sets [ prshf c .func→ f ∘ eqTrans i A ] ]
+--          lem
+--           = isz2 _ _ lemm _ i
+--             -- (Sets [ eqTrans i B ∘ prshf c .func→ f ])
+--             -- (Sets [ prshf c .func→ f ∘ eqTrans i A ])
+--             -- lemm
+--             -- _ i
+--         in
+--           lem
+--       -- eqNat = λ {A} {B} i ℂ[B,A] i' ℂ[A,c] →
+--       --   let
+--       --     k : ℂ [ {!!} , {!!} ]
+--       --     k = ℂ[A,c]
+--       --   in {!ℂ [ ? ∘ ? ]!}
 
-      :ident: : (:func→: (ℂ .𝟙 {c})) ≡ (Fun .𝟙 {o = prshf c})
-      :ident: = Σ≡ eqTrans eqNat
+--       :ident: : (:func→: (ℂ .𝟙 {c})) ≡ (Fun .𝟙 {o = prshf c})
+--       :ident: = Σ≡ eqTrans eqNat
 
-  yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = Sets {ℓ}})
-  yoneda = record
-    { func* = prshf
-    ; func→ = :func→:
-    ; isFunctor = record
-      { ident = :ident:
-      ; distrib = {!!}
-      }
-    }
+--   yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = Sets {ℓ}})
+--   yoneda = record
+--     { func* = prshf
+--     ; func→ = :func→:
+--     ; isFunctor = record
+--       { ident = :ident:
+--       ; distrib = {!!}
+--       }
+--     }