Functor comprehension simplification (#59)

Simplification of Functor Comprehension++

This commit simplifies the FunctorComprehension proof, specifically the
part that constructs a representation from a universal element, in two
ways:

1. Use a principle `change-contractum` to get rid of some tedious
   reasoning about squares

2. Redefine the displayed category of representations so that its
   structure lines up more closely with the one for universal elements
   so there's fewer associativities

In the process I added a few more minor things:

1. several more useful constructions to displayed categories
2. cleaning up some stuff in the IsoComma HLevel proofs
3. define the FullImage of a functor (which I didn't end up needing).
4. proofs for when LiftF and postComposeF are FullyFaithful

Cubical/Categories/Constructions/BinProduct/More.agda

@@ -27,6 +27,9 @@ open Functor
 Δ : ∀ (C : Category ℓC ℓC') → Functor C (C ×C C)
 Δ C = Id ,F Id
 
+Sym : {C : Category ℓC ℓC'}{D : Category ℓD ℓD'} → Functor (C ×C D) (D ×C C)
+Sym {C = C}{D = D} = Snd C D ,F Fst C D
+
 -- helpful decomposition of morphisms used in several proofs
 -- about product category
 module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}{E : Category ℓE ℓE'} where

Cubical/Categories/Constructions/FullImage.agda

@@ -0,0 +1,73 @@
+{-
+
+The Full Image of a Functor
+
+-}
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Constructions.FullImage where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Equiv.Properties
+open import Cubical.Functions.Embedding
+open import Cubical.Data.Sigma
+open import Cubical.HITs.PropositionalTruncation as PropTrunc
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Categories.Constructions.FullSubcategory
+
+private
+  variable
+    ℓC ℓC' ℓD ℓD' : Level
+
+
+open Category
+open Functor
+
+module _
+  {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}
+  (F : Functor C D) where
+
+  FullImage : Category ℓC ℓD'
+  FullImage .ob = C .ob
+  FullImage .Hom[_,_] c c' = D [ F ⟅ c ⟆ , F ⟅ c' ⟆ ]
+  FullImage .id = D .id
+  FullImage ._⋆_ = D ._⋆_
+  FullImage .⋆IdL = D .⋆IdL
+  FullImage .⋆IdR = D .⋆IdR
+  FullImage .⋆Assoc = D .⋆Assoc
+  FullImage .isSetHom = D .isSetHom
+
+  ToFullImage : Functor C FullImage
+  ToFullImage .F-ob = λ z → z
+  ToFullImage .F-hom = F-hom F
+  ToFullImage .F-id = F-id F
+  ToFullImage .F-seq = F-seq F
+
+  FromFullImage : Functor FullImage D
+  FromFullImage .F-ob = F-ob F
+  FromFullImage .F-hom = λ z → z
+  FromFullImage .F-id = refl
+  FromFullImage .F-seq f g = refl
+
+  CompFullImage : (FromFullImage ∘F ToFullImage ≡ F)
+  CompFullImage = Functor≡ (λ _ → refl) (λ _ → refl)
+
+module _
+  {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}
+  {F : Functor C D}
+  (isFullyFaithfulF : isFullyFaithful F)
+  where
+  private
+    FC = FullImage F
+    FF≃  : ∀ {x y} → C [ x , y ] ≃ D [ _ , _ ]
+    FF≃ = _ , (isFullyFaithfulF _ _)
+
+  inv : Functor FC C
+  inv .F-ob = λ z → z
+  inv .F-hom = invIsEq (isFullyFaithfulF _ _)
+  inv .F-id = sym (invEq (equivAdjointEquiv FF≃) (F .F-id))
+  inv .F-seq f g =
+    sym (invEq (equivAdjointEquiv FF≃)
+    (F .F-seq _ _ ∙ cong₂ (seq' D) (secEq FF≃ _) (secEq FF≃ _)))

Cubical/Categories/Displayed/Base/DisplayOverProjections.agda

@@ -9,17 +9,19 @@ open import Cubical.Data.Sigma
 open import Cubical.Categories.Category.Base
 open import Cubical.Categories.Constructions.BinProduct
   renaming (Fst to FstBP ; Snd to SndBP)
+open import Cubical.Categories.Constructions.BinProduct.More
 open import Cubical.Categories.Functor
 
 open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Reasoning
 open import Cubical.Categories.Displayed.Properties
 open import Cubical.Categories.Displayed.Functor
 open import Cubical.Categories.Displayed.Instances.Terminal
 open import Cubical.Categories.Displayed.Base.More
 
 private
   variable
-    ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓEᴰ ℓEᴰ' : Level
+    ℓB ℓB' ℓBᴰ ℓBᴰ' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓEᴰ ℓEᴰ' : Level
 
 open Categoryᴰ
 
@@ -54,25 +56,6 @@ module _
   Fstᴰsr .Functorᴰ.F-idᴰ = refl
   Fstᴰsr .Functorᴰ.F-seqᴰ = λ fᴰ gᴰ → refl
 
-  -- s for "simple" because C is not dependent on D
-  -- l for "left" because C is on the left of the product
-  ∫Cᴰsl : Categoryᴰ D (ℓ-max ℓC ℓCᴰ) (ℓ-max ℓC' ℓCᴰ')
-  ∫Cᴰsl .ob[_] d = Σ[ c ∈ C .ob ] Cᴰ.ob[ c , d ]
-  ∫Cᴰsl .Hom[_][_,_] g (c , cᴰ) (c' , cᴰ') =
-    Σ[ f ∈ C [ c , c' ] ] Cᴰ.Hom[ f , g ][ cᴰ , cᴰ' ]
-  ∫Cᴰsl .idᴰ = (C .id) , Cᴰ.idᴰ
-  ∫Cᴰsl ._⋆ᴰ_ (f , fᴰ) (g , gᴰ) = (f ⋆⟨ C ⟩ g) , (fᴰ Cᴰ.⋆ᴰ gᴰ)
-  ∫Cᴰsl .⋆IdLᴰ (f , fᴰ) = ΣPathP (_ , Cᴰ.⋆IdLᴰ _)
-  ∫Cᴰsl .⋆IdRᴰ _ = ΣPathP (_ , Cᴰ.⋆IdRᴰ _)
-  ∫Cᴰsl .⋆Assocᴰ _ _ _ = ΣPathP (_ , Cᴰ.⋆Assocᴰ _ _ _)
-  ∫Cᴰsl .isSetHomᴰ = isSetΣ (C .isSetHom) (λ _ → Cᴰ .isSetHomᴰ)
-
-  Fstᴰsl : Functorᴰ Id ∫Cᴰsl (weaken D C)
-  Fstᴰsl .Functorᴰ.F-obᴰ = fst
-  Fstᴰsl .Functorᴰ.F-homᴰ = fst
-  Fstᴰsl .Functorᴰ.F-idᴰ = refl
-  Fstᴰsl .Functorᴰ.F-seqᴰ = λ _ _ → refl
-
   module _
     {E : Category ℓE ℓE'}
     (F : Functor E C)
@@ -130,3 +113,86 @@ module _
     Assc' .F-homᴰ {_}{_}{f} _ = f .snd .snd
     Assc' .F-idᴰ = refl
     Assc' .F-seqᴰ _ _ = refl
+
+module _
+  {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}
+  (Cᴰ : Categoryᴰ (C ×C D) ℓCᴰ ℓCᴰ')
+  where
+  open Category
+
+  private
+    module Cᴰ = Categoryᴰ Cᴰ
+
+  private
+    -- can't use reindex bc transport hell
+    Cᴰ' : Categoryᴰ (D ×C C) _ _
+    ob[ Cᴰ' ] (d , c) = Cᴰ.ob[ c , d ]
+    Cᴰ' .Hom[_][_,_] (g , f) cᴰ cᴰ' = Cᴰ.Hom[ f , g ][ cᴰ , cᴰ' ]
+    Cᴰ' .idᴰ = Cᴰ.idᴰ
+    Cᴰ' ._⋆ᴰ_ = Cᴰ._⋆ᴰ_
+    Cᴰ' .⋆IdLᴰ = Cᴰ.⋆IdLᴰ
+    Cᴰ' .⋆IdRᴰ = Cᴰ.⋆IdRᴰ
+    Cᴰ' .⋆Assocᴰ = Cᴰ.⋆Assocᴰ
+    Cᴰ' .isSetHomᴰ = Cᴰ.isSetHomᴰ
+
+  -- s for "simple" because C is not dependent on D
+  -- l for "left" because C is on the left of the product
+  ∫Cᴰsl : Categoryᴰ D (ℓ-max ℓC ℓCᴰ) (ℓ-max ℓC' ℓCᴰ')
+  ∫Cᴰsl = ∫Cᴰsr {D = C} Cᴰ'
+
+  Fstᴰsl : Functorᴰ Id ∫Cᴰsl (weaken D C)
+  Fstᴰsl = Fstᴰsr Cᴰ'
+
+  module _
+    {E : Category ℓE ℓE'}
+    (F : Functor E D)
+    {Eᴰ : Categoryᴰ E ℓEᴰ ℓEᴰ'}
+    (Fᴰ : Functorᴰ F Eᴰ (weaken D C))
+    (Gᴰ : Functorᴰ (Sym {C = D}{D = C} ∘F ∫F Fᴰ) (Unitᴰ (∫C Eᴰ)) Cᴰ)
+    where
+
+    mk∫ᴰslFunctorᴰ : Functorᴰ F Eᴰ ∫Cᴰsl
+    mk∫ᴰslFunctorᴰ = mk∫ᴰsrFunctorᴰ Cᴰ' F Fᴰ Gᴰ' where
+      module Gᴰ = Functorᴰ Gᴰ
+      Gᴰ' : Functorᴰ (∫F Fᴰ) (Unitᴰ (∫C Eᴰ)) Cᴰ'
+      Gᴰ' .Functorᴰ.F-obᴰ  _ = Gᴰ.F-obᴰ _
+      Gᴰ' .Functorᴰ.F-homᴰ _ = Gᴰ.F-homᴰ _
+      Gᴰ' .Functorᴰ.F-idᴰ {x}{xᴰ} = ≡[]-rectify Cᴰ Gᴰ.F-idᴰ
+      Gᴰ' .Functorᴰ.F-seqᴰ _ _ = ≡[]-rectify Cᴰ (Gᴰ.F-seqᴰ _ _)
+  Assoc-sl⁻ : Functor (∫C ∫Cᴰsl) (∫C Cᴰ)
+  Assoc-sl⁻ = mk∫Functor Assc Assc' where
+    open Functor
+    open Functorᴰ
+    -- Might want this at the top level
+    Assc : Functor (∫C ∫Cᴰsl) (C ×C D)
+    Assc .F-ob (d , (c , _)) = c , d
+    Assc .F-hom (g , (f , _)) = f , g
+    Assc .F-id = refl
+    Assc .F-seq _ _ = refl
+
+    Assc' : Functorᴰ Assc _ Cᴰ
+    Assc' .F-obᴰ {x}        _ = x .snd .snd
+    Assc' .F-homᴰ {_}{_}{f} _ = f .snd .snd
+    Assc' .F-idᴰ = refl
+    Assc' .F-seqᴰ _ _ = refl
+
+module _
+  {B : Category ℓB ℓB'}{C : Category ℓC ℓC'}
+  {D : Category ℓD ℓD'}
+  {E : Category ℓE ℓE'}
+  {Bᴰ : Categoryᴰ (B ×C D) ℓBᴰ ℓBᴰ'}
+  {Cᴰ : Categoryᴰ (C ×C E) ℓCᴰ ℓCᴰ'}
+  {F : Functor D E}
+  {G : Functor B C}
+  (FGᴰ : Functorᴰ (G ×F F) Bᴰ Cᴰ)
+  where
+  private
+    module G = Functor G
+    module FGᴰ = Functorᴰ FGᴰ
+  -- ideally this would be implemented using mk∫ᴰslFunctorᴰ
+  ∫ᴰslF : Functorᴰ F (∫Cᴰsl {C = B}{D = D} Bᴰ) (∫Cᴰsl {C = C}{D = E} Cᴰ)
+  ∫ᴰslF .Functorᴰ.F-obᴰ {d} (b , bᴰ) = (G ⟅ b ⟆) , (FGᴰ.F-obᴰ bᴰ)
+  ∫ᴰslF .Functorᴰ.F-homᴰ {g} (f , fᴰ) = (G ⟪ f ⟫) , (FGᴰ.F-homᴰ fᴰ)
+  ∫ᴰslF .Functorᴰ.F-idᴰ = ΣPathP (G.F-id , (≡[]-rectify Cᴰ FGᴰ.F-idᴰ))
+  ∫ᴰslF .Functorᴰ.F-seqᴰ _ _ =
+    ΣPathP ((G.F-seq _ _) , (≡[]-rectify Cᴰ (FGᴰ.F-seqᴰ _ _)))

Cubical/Categories/Displayed/Base/HLevel1Homs.agda

@@ -73,3 +73,20 @@ module _
   mkFunctorᴰContrHoms contrHoms F-obᴰ =
     mkFunctorᴰPropHoms (hasContrHoms→hasPropHoms Dᴰ contrHoms) F-obᴰ
     λ _ → contrHoms _ _ _ .fst
+
+  -- Alternate version: maybe Dᴰ.Hom[_][_,_] isn't always
+  -- contractible, but it is in the image of F-obᴰ
+  mkFunctorᴰContrHoms'
+    : (F-obᴰ  : {x : C .ob} → Cᴰ.ob[ x ] → Dᴰ.ob[ F .F-ob x ])
+    → (F-homᴰ : {x y : C .ob}
+      {f : C [ x , y ]} {xᴰ : Cᴰ.ob[ x ]} {yᴰ : Cᴰ.ob[ y ]}
+    → Cᴰ [ f ][ xᴰ , yᴰ ]
+    → isContr (Dᴰ [ F .F-hom f ][ F-obᴰ xᴰ , F-obᴰ yᴰ ]))
+    → Functorᴰ F Cᴰ Dᴰ
+  mkFunctorᴰContrHoms' F-obᴰ F-homᴰ .Functorᴰ.F-obᴰ = F-obᴰ
+  mkFunctorᴰContrHoms' F-obᴰ F-homᴰ .Functorᴰ.F-homᴰ fᴰ = F-homᴰ fᴰ .fst
+  mkFunctorᴰContrHoms' F-obᴰ F-homᴰ .Functorᴰ.F-idᴰ =
+    symP (toPathP (isProp→PathP (λ i → isContr→isProp (F-homᴰ Cᴰ.idᴰ)) _ _))
+  mkFunctorᴰContrHoms' F-obᴰ F-homᴰ .Functorᴰ.F-seqᴰ fᴰ gᴰ =
+    symP (toPathP (isProp→PathP
+      (λ i → isContr→isProp (F-homᴰ (fᴰ Cᴰ.⋆ᴰ gᴰ))) _ _))

Cubical/Categories/Displayed/Constructions/Comma.agda

@@ -16,6 +16,7 @@ open import Cubical.Data.Unit
 
 open import Cubical.Categories.Category.Base
 open import Cubical.Categories.Constructions.FullSubcategory
+open import Cubical.Categories.Displayed.Constructions.FullSubcategory
 open import Cubical.Categories.Bifunctor.Redundant
 open import Cubical.Categories.Constructions.BinProduct as BinProduct
 open import Cubical.Categories.Functor.Base
@@ -69,52 +70,71 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}{E : Category ℓE 
   Commaᴰ₁ = ∫Cᴰsr Commaᴰ
 
   IsoCommaᴰ : Categoryᴰ (C ×C D) (ℓ-max ℓE' ℓE') ℓE'
-  IsoCommaᴰ = ∫Cᴰ Commaᴰ (Preorderᴰ→Catᴰ IsoCommaᴰ') where
-    IsoCommaᴰ' : Preorderᴰ Comma ℓE' ℓ-zero
-    IsoCommaᴰ' .ob[_] ((c , d) , f)= isIso E f
-    IsoCommaᴰ' .Hom[_][_,_] _ _ _ = Unit
-    IsoCommaᴰ' .idᴰ = tt
-    IsoCommaᴰ' ._⋆ᴰ_ _ _ = tt
-    IsoCommaᴰ' .isPropHomᴰ = isPropUnit
+  IsoCommaᴰ = ∫Cᴰ Commaᴰ (FullSubcategoryᴰ _ (λ (_ , f) → isIso E f))
 
   -- Not following from a gneral result about ∫Cᴰ but works
   hasPropHomsIsoCommaᴰ : hasPropHoms IsoCommaᴰ
   hasPropHomsIsoCommaᴰ {c , d}{c' , d'} f cᴰ cᴰ' =
   -- TODO generalize this as a reasoning principle for ∫Cᴰ
     isPropΣ
       (hasPropHomsCommaᴰ f (cᴰ .fst) (cᴰ' .fst))
-      λ x → hasPropHomsPreorderᴰ _ (f , x) (cᴰ .snd) (cᴰ' .snd)
+      λ x → hasPropHomsFullSubcategory _ _ (f , x) (cᴰ .snd) (cᴰ' .snd)
 
   IsoComma : Category _ _
   IsoComma = ∫C IsoCommaᴰ
 
-  IsoCommaᴰ₁ : Categoryᴰ C (ℓ-max ℓD ℓE') (ℓ-max ℓD' ℓE')
+  IsoCommaᴰ₁ : Categoryᴰ C _ _
   IsoCommaᴰ₁ = ∫Cᴰsr IsoCommaᴰ
 
+  IsoCommaᴰ₂ : Categoryᴰ D _ _
+  IsoCommaᴰ₂ = ∫Cᴰsl IsoCommaᴰ
+
   open isIso
   -- Characterization of HLevel of Commaᴰ₁ homs
+  private
+    module IC₁ = Categoryᴰ IsoCommaᴰ₁
+    module _ {c c'}(f : C [ c , c' ])
+             (c≅d : IC₁.ob[ c ])
+             (c'≅d' : IC₁.ob[ c' ]) where
+      AltHom : Type _
+      AltHom = fiber (G .F-hom)
+        (c≅d .snd .snd .inv ⋆⟨ E ⟩ F .F-hom f ⋆⟨ E ⟩ c'≅d' .snd .fst)
+
+      ICHom = IC₁.Hom[ f ][ c≅d , c'≅d' ]
+
+      Hom→Alt : ICHom → AltHom
+      Hom→Alt (g , sq , _) = g ,
+        ⋆InvLMove (c≅d .snd) (sym sq) ∙ sym (E .⋆Assoc _ _ _)
+
+      Alt→Hom : AltHom → ICHom
+      Alt→Hom (g , sq) = g ,
+        sym (⋆InvLMove⁻ (c≅d .snd) (sq ∙ E .⋆Assoc _ _ _)), tt
+
+      AltHomRetr : (x : ICHom) → Alt→Hom (Hom→Alt x) ≡ x
+      AltHomRetr _ = Σ≡Prop (λ g' → hasPropHomsIsoCommaᴰ _ _ _) refl
+
+      AltHomProp : isFaithful G → isProp AltHom
+      AltHomProp G-faithful = isEmbedding→hasPropFibers
+        (injEmbedding (E .isSetHom) (λ {g} {g'} → G-faithful _ _ _ _))
+        _
+
+      AltHomContr : isFullyFaithful G → isContr AltHom
+      AltHomContr G-ff = G-ff _ _ .equiv-proof _
+
+      HomProp : isFaithful G → isProp ICHom
+      HomProp G-faithful =
+        isPropRetract Hom→Alt Alt→Hom AltHomRetr (AltHomProp G-faithful)
+
+      HomContr : isFullyFaithful G → isContr ICHom
+      HomContr G-ff =
+        isContrRetract Hom→Alt Alt→Hom AltHomRetr (AltHomContr G-ff)
+
   hasPropHomsIsoCommaᴰ₁ : isFaithful G → hasPropHoms IsoCommaᴰ₁
-  hasPropHomsIsoCommaᴰ₁ G-faithful f (d , iso) (d' , iso') =
-    isPropRetract
-      (λ (g , sq , _) → g , ⋆InvLMove iso (sym sq) ∙ sym (E .⋆Assoc _ _ _))
-      (λ (g , sq) → g , sym (⋆InvLMove⁻ iso (sq ∙ E .⋆Assoc _ _ _)), tt)
-      ((λ (g , sq , _) → Σ≡Prop (λ g' → hasPropHomsIsoCommaᴰ _ _ _) refl))
-      (isEmbedding→hasPropFibers
-        (injEmbedding (E .isSetHom) (λ {g} {g'} → G-faithful d d' g g'))
-       (iso .snd .inv ⋆⟨ E ⟩ F .F-hom f ⋆⟨ E ⟩ iso' .fst))
+  hasPropHomsIsoCommaᴰ₁ G-faithful f diso diso' =
+    HomProp f diso diso' G-faithful
 
   hasContrHomsIsoCommaᴰ₁ : isFullyFaithful G → hasContrHoms IsoCommaᴰ₁
-  hasContrHomsIsoCommaᴰ₁ Gff f (d , e) (d' , e') =
-    inhProp→isContr
-      (g .fst .fst
-      , sym (⋆InvLMove⁻ e (g .fst .snd ∙ E .⋆Assoc _ _ _))
-      , tt)
-      (hasPropHomsIsoCommaᴰ₁
-        (isFullyFaithful→Faithful {F = G} Gff) f (d , e) (d' , e'))
-      where
-        G⟪g⟫ : E [ G .F-ob d , G .F-ob d' ]
-        G⟪g⟫ = e .snd .inv ⋆⟨ E ⟩ F ⟪ f ⟫ ⋆⟨ E ⟩ e' .fst
-        g = Gff d d' .equiv-proof G⟪g⟫
+  hasContrHomsIsoCommaᴰ₁ G-ff f diso diso' = HomContr f diso diso' G-ff
 
   πⁱ1 : Functor IsoComma C
   πⁱ1 = BinProduct.Fst C D ∘F Displayed.Fst {Cᴰ = IsoCommaᴰ}
@@ -127,6 +147,44 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}{E : Category ℓE 
   π≅ .NatIso.trans .N-hom (_ , sq , _) = sq
   π≅ .NatIso.nIso (_ , _ , isIso) = isIso
 
+module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}{E : Category ℓE ℓE'}
+         (F : Functor C E) (G : Functor D E) where
+
+  private
+    module IC₂ = Categoryᴰ (IsoCommaᴰ₂ F G)
+    module IC₁ = Categoryᴰ (IsoCommaᴰ₁ G F)
+    module _ {d d'}(g : D [ d , d' ])
+             (d≅c   : IC₂.ob[ d ])
+             (d'≅c' : IC₂.ob[ d' ]) where
+      c≅d : IC₁.ob[ d ]
+      c≅d = (d≅c .fst) , (invIso (d≅c .snd))
+      c'≅d' : IC₁.ob[ d' ]
+      c'≅d' = (d'≅c' .fst) , (invIso (d'≅c' .snd))
+      IC2Hom = IC₂.Hom[ g ][ d≅c , d'≅c' ]
+      IC1Hom = IC₁.Hom[ g ][ c≅d , c'≅d' ]
+
+      isOfHLevelIC2Hom : ∀ n → isOfHLevel n IC1Hom → isOfHLevel n IC2Hom
+      isOfHLevelIC2Hom n =
+        isOfHLevelRetract n
+          -- this proof would be better if it was an iff directly
+          (λ (f , sq2 , tt) → f ,
+          sym (⋆InvRMove (d'≅c' .snd)
+            (E .⋆Assoc _ _ _ ∙ sym (⋆InvLMove (d≅c .snd) (sym sq2))))
+          , tt)
+          (λ (f , sq1 , tt) → f ,
+            sym (⋆InvRMove (c'≅d' .snd)
+            (E .⋆Assoc _ _ _ ∙ sym (⋆InvLMove (c≅d .snd) (sym sq1))))
+            , tt)
+          λ sq2 → Σ≡Prop (λ _ → hasPropHomsIsoCommaᴰ F G _ _ _) refl
+
+  hasPropHomsIsoCommaᴰ₂ : isFaithful F → hasPropHoms (IsoCommaᴰ₂ F G)
+  hasPropHomsIsoCommaᴰ₂ F-faithful f diso diso' =
+    isOfHLevelIC2Hom _ _ _ 1 (hasPropHomsIsoCommaᴰ₁ G F F-faithful _ _ _)
+
+  hasContrHomsIsoCommaᴰ₂ : isFullyFaithful F → hasContrHoms (IsoCommaᴰ₂ F G)
+  hasContrHomsIsoCommaᴰ₂ F-ff f diso diso' =
+    isOfHLevelIC2Hom _ _ _ 0 (hasContrHomsIsoCommaᴰ₁ G F F-ff _ _ _)
+
 module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}{E : Category ℓE ℓE'}
          {F : Functor C E} {G : Functor D E}
          {B : Category ℓB ℓB'}