Stuff about the free category

src/Cat/Categories/Free.agda

@@ -8,55 +8,65 @@ open import Data.Product
 open import Cat.Category
 
 open IsCategory
-open Category
 
 -- data Path {ℓ : Level} {A : Set ℓ} : (a b : A) → Set ℓ where
 --   emptyPath : {a : A} → Path a a
 --   concatenate : {a b c : A} → Path a b → Path b c → Path a b
 
+-- import Data.List
+-- P : (a b : Object ℂ) → Set (ℓ ⊔ ℓ')
+-- P = {!Data.List.List ?!}
+-- Generalized paths:
+data Path {ℓ ℓ' : Level} {A : Set ℓ} (R : A → A → Set ℓ') : (a b : A) → Set (ℓ ⊔ ℓ') where
+  empty : {a : A} → Path R a a
+  cons : {a b c : A} → R b c → Path R a b → Path R a c
+
+concatenate _++_ : ∀ {ℓ ℓ'} {A : Set ℓ} {a b c : A} {R : A → A → Set ℓ'} → Path R b c → Path R a b → Path R a c
+concatenate empty p = p
+concatenate (cons x q) p = cons x (concatenate q p)
+_++_ = concatenate
+
+singleton : ∀ {ℓ} {𝓤 : Set ℓ} {ℓr} {R : 𝓤 → 𝓤 → Set ℓr} {A B : 𝓤} → R A B → Path R A B
+singleton f = cons f empty
+
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
   module ℂ = Category ℂ
-
-  -- import Data.List
-  -- P : (a b : Object ℂ) → Set (ℓ ⊔ ℓ')
-  -- P = {!Data.List.List ?!}
-  -- Generalized paths:
-  -- data P {ℓ : Level} {A : Set ℓ} (R : A → A → Set ℓ) : (a b : A) → Set ℓ where
-  --   e : {a : A} → P R a a
-  --   c : {a b c : A} → R a b → P R b c → P R a c
-
-  -- Path's are like lists with directions.
-  -- This implementation is specialized to categories.
-  data Path : (a b : Object ℂ) → Set (ℓ ⊔ ℓ') where
-    empty : {A : Object ℂ} → Path A A
-    cons : ∀ {A B C} → ℂ [ B , C ] → Path A B → Path A C
-
-  concatenate : ∀ {A B C : Object ℂ}  → Path B C → Path A B → Path A C
-  concatenate empty p = p
-  concatenate (cons x q) p = cons x (concatenate q p)
+  open Category ℂ
 
   private
-    module _ {A B C D : Object ℂ} where
-      p-assoc : {r : Path A B} {q : Path B C} {p : Path C D} → concatenate p (concatenate q r) ≡ concatenate (concatenate p q) r
-      p-assoc {r} {q} {p} = {!!}
-    module _ {A B : Object ℂ} {p : Path A B} where
-      -- postulate
-      --   ident-r : concatenate {A} {A} {B} p (lift 𝟙) ≡ p
-      --   ident-l : concatenate {A} {B} {B} (lift 𝟙) p ≡ p
-    module _ {A B : Object ℂ} where
-      isSet : Cubical.isSet (Path A B)
-      isSet = {!!}
+    p-assoc : {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
+    p-assoc {r = r} {q} {empty} = refl
+    p-assoc {A} {B} {C} {D} {r = r} {q} {cons x p} = begin
+      cons x p ++ (q ++ r)   ≡⟨ cong (cons x) lem ⟩
+      cons x ((p ++ q) ++ r) ≡⟨⟩
+      (cons x p ++ q) ++ r ∎
+      where
+        lem : p ++ (q ++ r) ≡ ((p ++ q) ++ r)
+        lem = p-assoc {r = r} {q} {p}
+
+    ident-r : ∀ {A} {B} {p : Path Arrow A B} → concatenate p empty ≡ p
+    ident-r {p = empty} = refl
+    ident-r {p = cons x p} = cong (cons x) ident-r
+
+    ident-l : ∀ {A} {B} {p : Path Arrow A B} → concatenate empty p ≡ p
+    ident-l = refl
+
+    module _ {A B : Object} where
+      isSet : Cubical.isSet (Path Arrow A B)
+      isSet a b p q = {!!}
+
   RawFree : RawCategory ℓ (ℓ ⊔ ℓ')
   RawFree = record
-    { Object = Object ℂ
-    ; Arrow = Path
-    ; 𝟙 = λ {o} → {!lift 𝟙!}
-    ; _∘_ = λ {a b c} → {!concatenate {a} {b} {c}!}
+    { Object = Object
+    ; Arrow = Path Arrow
+    ; 𝟙 = empty
+    ; _∘_ = concatenate
     }
   RawIsCategoryFree : IsCategory RawFree
   RawIsCategoryFree = record
-    { assoc = {!p-assoc!}
-    ; ident = {!ident-r , ident-l!}
+    { assoc = λ { {f = f} {g} {h} → p-assoc {r = f} {g} {h}}
+    ; ident = ident-r , ident-l
     ; arrowIsSet = {!!}
     ; univalent = {!!}
     }