A construction of the free category without quotienting

Cubical/Categories/Constructions/Free/Category/Unquotiented.agda

@@ -0,0 +1,93 @@
+{- The free category on a Quiver, but without using HITs -}
+{-# OPTIONS --safe #-}
+-- Free category with a terminal object, over a Quiver
+module Cubical.Categories.Constructions.Free.Category.Unquotiented where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Data.Quiver.Base
+open import Cubical.Data.Sigma
+open import Cubical.Data.W.Indexed
+
+open import Cubical.Categories.Constructions.Free.Category.Base
+
+private
+  variable
+    ℓc ℓc' ℓd ℓd' ℓg ℓg' ℓh ℓh' ℓj ℓ : Level
+    ℓC ℓC' ℓCᴰ ℓCᴰ' : Level
+
+open QuiverOver
+module _ (Q : Quiver ℓg ℓg') where
+  data Mor : Q .fst → Q .fst → Type (ℓ-max ℓg ℓg') where
+    nil  : ∀ {q} → Mor q q
+    cons : ∀ {q'} e → Mor (Q .snd .cod e) q' → Mor (Q .snd .dom e) q'
+
+  elim : ∀ {B : ∀ {q} {q'} → Mor q q' → Type ℓ}
+    → (∀ {q} → B (nil {q}))
+    → (∀ {q'} e (m : Mor _ q') → B m → B (cons e m))
+    → ∀ {q q'} → (m : Mor q q') → B m
+  elim {B = B} [nil] [cons] nil = [nil]
+  elim {B = B} [nil] [cons] (cons e m) = [cons] e m (elim {B = B} [nil] [cons] m)
+
+  rec : ∀ {B : Q .fst → Q .fst → Type ℓ}
+    → (∀ {q} → B q q)
+    → (∀ {q'} e → B (Q .snd .cod e) q' → B (Q .snd .dom e) q')
+    → ∀ {q q'} → Mor q q' → B q q'
+  rec {B = B} [nil] [cons] nil = [nil]
+  rec {B = B} [nil] [cons] (cons e m) = [cons] e (rec {B = B} [nil] [cons] m)
+
+  append : ∀ {q1 q2 q3} → Mor q1 q2 → Mor q2 q3 → Mor q1 q3
+  append {q3 = q3} = rec {B = λ q1 q2 → Mor q2 q3 → Mor q1 q3}
+    (λ {q} m' → m')
+    λ {q'} e r m' → cons e (r m')
+
+  append-nil : ∀ {q q'} → (m : Mor q q') → append m nil ≡ m
+  append-nil = elim {B = λ m → append m nil ≡ m}
+    refl
+    λ m m' → cong (cons m)
+
+  append-assoc : ∀ {q q' q'' q'''} → (m : Mor q q')(m' : Mor q' q'')(m'' : Mor q'' q''')
+    → append m (append m' m'') ≡ append (append m m') m''
+  append-assoc m m' m'' =
+    elim {B = λ m → ∀ {m'} → append m (append m' m'') ≡ append (append m m') m''}
+      refl (λ e m ih → cong (cons e) ih)
+      m {m'}
+
+  module _ (isGpdQOb : isGroupoid (Q .fst)) (isSetQMor : isSet (Q .snd .mor)) where
+    isSetMor : ∀ {q} {q'} → isSet (Mor q q')
+    isSetMor {q}{q'} = isSetRetract
+      {B = Tree q q'}
+      Mor→Tree Tree→Mor M◂T
+        (isOfHLevelSuc-IW 1 (λ (q , q') → isSet⊎ (isGpdQOb _ _) (isSetΣ isSetQMor λ _ → isGpdQOb _ _)) _)
+      where
+       open import Cubical.Data.Sum hiding (rec; elim)
+       import Cubical.Data.Sum as Sum
+       open import Cubical.Data.Empty hiding (rec; elim)
+       import Cubical.Data.Empty as Empty
+       open import Cubical.Data.Unit
+
+       Tree : ∀ q q' → Type _
+       Tree q q' = IW {X = Q .fst × Q .fst}
+              (λ (q , q') → (q ≡ q') ⊎ (Σ[ e ∈ _ ] Q .snd .dom e ≡ q))
+              (λ q → Sum.rec (λ _ → ⊥) λ _ → Unit)
+              (λ q → Sum.elim (λ _ → Empty.elim) λ (e , _) _ → Q .snd .cod e , q .snd)
+              (q , q')
+
+       Mor→Tree : ∀ {q q'} → Mor q q' → Tree q q'
+       Mor→Tree = rec {B = Tree}
+         (node (inl refl) Empty.elim)
+         λ e t → node (inr (e , refl)) λ _ → t
+
+       Tree→Mor : ∀ {q q'} → Tree q q' → Mor q q'
+       Tree→Mor {q}{q'} (node (inl p) subtree) = subst (λ q' → Mor q q') p nil
+       Tree→Mor {q}{q'} (node (inr (e , p)) subtree) =
+         subst (λ q → Mor q q') p (cons e (Tree→Mor (subtree _)))
+
+       M◂T : ∀ {q q'} → (m : Mor q q') → Tree→Mor (Mor→Tree m) ≡ m
+       M◂T = elim {B = λ m → Tree→Mor (Mor→Tree m) ≡ m}
+         (λ {q} → substRefl {A = Q .fst}{B = λ q' → Mor q q'} nil)
+         λ {q'} e m ih →
+           substRefl {A = Q .fst}{B = λ q → Mor q q'} (cons e (Tree→Mor (Mor→Tree m)))
+           ∙ cong (cons e) ih