fix naming

Author: anshwad10

Cubical/Categories/Dagger/Functor.agda

@@ -19,47 +19,47 @@ private variable
 open †Category
 
 module _ (C : †Category ℓC ℓC') (D : †Category ℓD ℓD') where
-  record IsDagFunctor (F : Functor (C .cat) (D .cat)) : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
+  record Is†Functor (F : Functor (C .cat) (D .cat)) : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
     no-eta-equality
     field
       F-† : ∀ {x y} (f : C .cat [ x , y ]) → F ⟪ f †[ C ] ⟫ ≡ F ⟪ f ⟫ †[ D ]
 
-  open IsDagFunctor public
+  open Is†Functor public
 
-  isPropIsDagFunctor : ∀ F → isProp (IsDagFunctor F)
-  isPropIsDagFunctor F a b i .F-† f = D .isSetHom _ _ (a .F-† f) (b .F-† f) i
+  isPropIs†Functor : ∀ F → isProp (Is†Functor F)
+  isPropIs†Functor F a b i .F-† f = D .isSetHom _ _ (a .F-† f) (b .F-† f) i
 
-  DagFunctor : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD'))
-  DagFunctor = Σ[ F ∈ Functor (C .cat) (D .cat) ] IsDagFunctor F
+  †Functor : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD'))
+  †Functor = Σ[ F ∈ Functor (C .cat) (D .cat) ] Is†Functor F
 
 open Functor
 
-†Id : DagFunctor C C
+†Id : †Functor C C
 †Id .fst = Id
 †Id .snd .F-† f = refl
 
-†FuncComp : DagFunctor C D → DagFunctor D E → DagFunctor C E
+†FuncComp : †Functor C D → †Functor D E → †Functor C E
 †FuncComp F G .fst = G .fst ∘F F .fst
 †FuncComp {C = C} {D = D} {E = E} F G .snd .F-† f =
   G .fst ⟪ F .fst ⟪ f †[ C ] ⟫ ⟫ ≡⟨ cong (G .fst .F-hom) (F .snd .F-† f) ⟩
   G .fst ⟪ F .fst ⟪ f ⟫ †[ D ] ⟫ ≡⟨ G .snd .F-† (F .fst .F-hom f) ⟩
   G .fst ⟪ F .fst ⟪ f ⟫ ⟫ †[ E ] ∎
 
-_∘†F_ : DagFunctor D E → DagFunctor C D → DagFunctor C E
+_∘†F_ : †Functor D E → †Functor C D → †Functor C E
 G ∘†F F = †FuncComp F G
 
-†Func≡ : (F G : DagFunctor C D) → F .fst ≡ G .fst → F ≡ G
-†Func≡ {C} {D} F G = Σ≡Prop (isPropIsDagFunctor C D)
+†Func≡ : (F G : †Functor C D) → F .fst ≡ G .fst → F ≡ G
+†Func≡ {C} {D} F G = Σ≡Prop (isPropIs†Functor C D)
 
 open †Category
 
-†Constant : ob D → DagFunctor C D
+†Constant : ob D → †Functor C D
 †Constant {D} d .fst = Constant _ _ d
 †Constant {D} d .snd .F-† _ = sym (D .†-id)
 
 open NatTrans
 
-NT† : (F G : DagFunctor C D) → NatTrans (F .fst) (G .fst) → NatTrans (G .fst) (F .fst)
+NT† : (F G : †Functor C D) → NatTrans (F .fst) (G .fst) → NatTrans (G .fst) (F .fst)
 NT† {C} {D} F G n .N-ob x = n ⟦ x ⟧ †[ D ]
 NT† {C} {D} F G n .N-hom {x} {y} f =
   G .fst ⟪ f ⟫ D.⋆ n ⟦ y ⟧ D.†         ≡⟨ congL D._⋆_ (sym (D .†-invol (G .fst ⟪ f ⟫))) ⟩

Cubical/Categories/Dagger/Instances/BinProduct.agda

@@ -27,42 +27,42 @@ BinProdDaggerStr dagC dagD .is-dag .†-invol (f , g) = ≡-× (dagC .†-invol
 BinProdDaggerStr dagC dagD .is-dag .†-id = ≡-× (dagC .†-id) (dagD .†-id)
 BinProdDaggerStr dagC dagD .is-dag .†-seq (f , g) (f' , g') = ≡-× (dagC .†-seq f f') (dagD .†-seq g g')
 
-DagBinProd _׆_ : †Category ℓ ℓ' → †Category ℓ'' ℓ''' → †Category (ℓ-max ℓ ℓ'') (ℓ-max ℓ' ℓ''')
-DagBinProd C D .cat = C .cat ×C D .cat
-DagBinProd C D .dagstr = BinProdDaggerStr (C .dagstr) (D .dagstr)
-_׆_ = DagBinProd
+†BinProd _׆_ : †Category ℓ ℓ' → †Category ℓ'' ℓ''' → †Category (ℓ-max ℓ ℓ'') (ℓ-max ℓ' ℓ''')
+†BinProd C D .cat = C .cat ×C D .cat
+†BinProd C D .dagstr = BinProdDaggerStr (C .dagstr) (D .dagstr)
+_׆_ = †BinProd
 
 module _ (C : †Category ℓ ℓ') (D : †Category ℓ'' ℓ''') where
-  †Fst : DagFunctor (C ׆ D) C
+  †Fst : †Functor (C ׆ D) C
   †Fst .fst = Fst (C .cat) (D .cat)
   †Fst .snd .F-† (f , g) = refl
 
-  †Snd : DagFunctor (C ׆ D) D
+  †Snd : †Functor (C ׆ D) D
   †Snd .fst = Snd (C .cat) (D .cat)
   †Snd .snd .F-† (f , g) = refl
 
 module _ where
   private variable
     B C D E : †Category ℓ ℓ'
 
-  _,†F_ : DagFunctor C D → DagFunctor C E → DagFunctor C (D ׆ E)
+  _,†F_ : †Functor C D → †Functor C E → †Functor C (D ׆ E)
   (F ,†F G) .fst = F .fst ,F G .fst
   (F ,†F G) .snd .F-† f = ≡-× (F .snd .F-† f) (G .snd .F-† f)
 
-  _׆F_ : DagFunctor B D → DagFunctor C E → DagFunctor (B ׆ C) (D ׆ E)
+  _׆F_ : †Functor B D → †Functor C E → †Functor (B ׆ C) (D ׆ E)
   _׆F_ {B = B} {C = C} F G = (F ∘†F †Fst B C) ,†F (G ∘†F †Snd B C)
 
-  †Δ : DagFunctor C (C ׆ C)
+  †Δ : †Functor C (C ׆ C)
   †Δ = †Id ,†F †Id
 
 module _ (C : †Category ℓ ℓ') (D : †Category ℓ'' ℓ''') where
-  †Swap : DagFunctor (C ׆ D) (D ׆ C)
+  †Swap : †Functor (C ׆ D) (D ׆ C)
   †Swap = †Snd C D ,†F †Fst C D
 
-  †Linj : ob D → DagFunctor C (C ׆ D)
+  †Linj : ob D → †Functor C (C ׆ D)
   †Linj d = †Id ,†F †Constant d
 
-  †Rinj : ob C → DagFunctor D (C ׆ D)
+  †Rinj : ob C → †Functor D (C ׆ D)
   †Rinj c = †Constant c ,†F †Id
 
   open areInv

Cubical/Categories/Dagger/Instances/Functors.agda

@@ -27,7 +27,7 @@ module _ (C : †Category ℓC ℓC') (D : †Category ℓD ℓD') where
   open NatTrans
 
   †FUNCTOR : †Category (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) (ℓ-max (ℓ-max ℓC ℓC') ℓD')
-  †FUNCTOR .cat = FullSubcategory (FUNCTOR (C .cat) (D .cat)) (IsDagFunctor C D)
+  †FUNCTOR .cat = FullSubcategory (FUNCTOR (C .cat) (D .cat)) (Is†Functor C D)
   †FUNCTOR .dagstr ._† {x = F} {y = G} = NT† F G
   †FUNCTOR .dagstr .is-dag .†-invol n = makeNatTransPath (funExt λ x → D .†-invol (n ⟦ x ⟧))
   †FUNCTOR .dagstr .is-dag .†-id = makeNatTransPath (funExt λ x → D .†-id)

Cubical/Categories/Dagger/Properties.agda

@@ -27,15 +27,14 @@ module _ (†C : †Category ℓ ℓ') where
   open CategoryPath
 
   -- Every dagger category is equal to its opposite
-  dagCat≡op : C ≡ C ^op
-  dagCat≡op = CategoryPath.mk≡ λ where
+  †Cat≡op : C ≡ C ^op
+  †Cat≡op = CategoryPath.mk≡ λ where
     .ob≡ → refl
-    .Hom≡ → funExt λ x → funExt λ y →
-      TypeIso.isoToPath λ where
-        .TypeIso.fun → _†
-        .TypeIso.inv → _†
-        .TypeIso.leftInv → †-invol
-        .TypeIso.rightInv → †-invol
+    .Hom≡ → funExt λ x → funExt λ y → TypeIso.isoToPath λ where
+      .TypeIso.fun → _†
+      .TypeIso.inv → _†
+      .TypeIso.leftInv → †-invol
+      .TypeIso.rightInv → †-invol
     .id≡ → implicitFunExt (toPathP (transportRefl (id †) ∙ †-id))
     .⋆≡ → implicitFunExt $ implicitFunExt $ implicitFunExt $ toPathP $ funExt λ f → funExt λ g →
       transport refl ((transport refl f † ⋆ transport refl g †) †) ≡⟨ transportRefl _ ⟩
@@ -51,23 +50,23 @@ module _ (†C : †Category ℓ ℓ') where
   open NatTrans
   open UnitCounit.TriangleIdentities
 
-  dagCatEquivOp : AdjointEquivalence C (C ^op)
-  dagCatEquivOp .fun .F-ob = idfun _
-  dagCatEquivOp .fun .F-hom = _†
-  dagCatEquivOp .fun .F-id = †-id
-  dagCatEquivOp .fun .F-seq = †-seq
-  dagCatEquivOp .inv .F-ob = idfun _
-  dagCatEquivOp .inv .F-hom = _†
-  dagCatEquivOp .inv .F-id = †-id
-  dagCatEquivOp .inv .F-seq = flip †-seq
-  dagCatEquivOp .η .trans .N-ob _ = id
-  dagCatEquivOp .η .trans .N-hom f = ⋆IdR f ∙∙ sym (†-invol f) ∙∙ sym (⋆IdL ((f †) †))
-  dagCatEquivOp .η .nIso _ = idCatIso .snd
-  dagCatEquivOp .ε .trans .N-ob _ = id
-  dagCatEquivOp .ε .trans .N-hom f = ⋆IdL ((f †) †) ∙∙ †-invol f ∙∙ sym (⋆IdR f)
-  dagCatEquivOp .ε .nIso _ = idCatIso .snd
-  dagCatEquivOp .triangleIdentities .Δ₁ _ = ⋆IdL _ ∙ †-id
-  dagCatEquivOp .triangleIdentities .Δ₂ _ = ⋆IdL _ ∙ †-id
+  †CatEquivOp : AdjointEquivalence C (C ^op)
+  †CatEquivOp .fun .F-ob = idfun _
+  †CatEquivOp .fun .F-hom = _†
+  †CatEquivOp .fun .F-id = †-id
+  †CatEquivOp .fun .F-seq = †-seq
+  †CatEquivOp .inv .F-ob = idfun _
+  †CatEquivOp .inv .F-hom = _†
+  †CatEquivOp .inv .F-id = †-id
+  †CatEquivOp .inv .F-seq = flip †-seq
+  †CatEquivOp .η .trans .N-ob _ = id
+  †CatEquivOp .η .trans .N-hom f = ⋆IdR f ∙∙ sym (†-invol f) ∙∙ sym (⋆IdL ((f †) †))
+  †CatEquivOp .η .nIso _ = idCatIso .snd
+  †CatEquivOp .ε .trans .N-ob _ = id
+  †CatEquivOp .ε .trans .N-hom f = ⋆IdL ((f †) †) ∙∙ †-invol f ∙∙ sym (⋆IdR f)
+  †CatEquivOp .ε .nIso _ = idCatIso .snd
+  †CatEquivOp .triangleIdentities .Δ₁ _ = ⋆IdL _ ∙ †-id
+  †CatEquivOp .triangleIdentities .Δ₂ _ = ⋆IdL _ ∙ †-id
 
 module †Morphisms (†C : †Category ℓ ℓ') where
   open †Category †C renaming (cat to C)