Fix univalence and displayed cat stuff

src/Cat/Base.agda

@@ -64,9 +64,13 @@ record Precategory (o h : Level) : Type (ℓsuc (o ⊔ h)) where
     {-# OVERLAPPING ⇒-Hom #-}
 
     ≅-Cat-Ob : ≅-notation Ob Ob (𝒰 h)
-    ≅-Cat-Ob ._≅_ = Iso Hom Hom
+    ≅-Cat-Ob ._≅_ = HIso Hom
     {-# OVERLAPPING ≅-Cat-Ob #-}
 
+    ≊-Cat-Ob : ≊-notation Ob Ob (𝒰 h)
+    ≊-Cat-Ob ._≊_ = HBiinv Hom
+    {-# OVERLAPPING ≊-Cat-Ob #-}
+
 private variable o h : Level
 
 open Precategory

src/Cat/Constructions/Sets.agda

@@ -10,12 +10,13 @@ open Iso
 
 iso→equiv : {A B : Set ℓ} → A ≅ B → ⌞ A ⌟ ≃ ⌞ B ⌟
 iso→equiv x .fst = x .to
-iso→equiv x .snd = is-inv→is-equiv (invertible (x .from) (x .inv-o) (x .inv-i))
+iso→equiv x .snd = qinv→is-equiv (qinv (x .from) (x .inv-o) (x .inv-i))
 
-@0 Sets-is-category : is-category (Sets ℓ)
-Sets-is-category .to-path i = n-ua (iso→equiv i)
-Sets-is-category .to-path-over p =
-  Sets.≅-pathᴾ refl _ $ fun-ext λ _ → =→ua-pathᴾ _ refl
+-- TODO
+-- @0 Sets-is-category : is-category (Sets ℓ)
+-- Sets-is-category .to-path i = n-ua (iso→equiv i)
+-- Sets-is-category .to-path-over p =
+--   Sets.≅-pathᴾ refl _ $ fun-ext λ _ → =→ua-pathᴾ _ refl
 
 instance
   Sets-has-initial : Initial (Sets ℓ)

src/Cat/Constructions/Types.agda

@@ -10,14 +10,19 @@ open import Cat.Morphism (Types ℓ) as Types
 
 open import Data.Sum
 
-open Iso
+open Biinv
 
--- TODO check no-eta
--- @0 Types-is-category : is-category (Types ℓ)
--- Types-is-category .to-path i = ua (≅ₜ→≃ {!!}) -- (iso→equiv i)
--- Types-is-category .to-path-over p = {!!}
+biinv→equiv : {A B : Type ℓ} → A ≊ B → A ≃ B
+biinv→equiv e .fst = e .to
+biinv→equiv e .snd = qinv→is-equiv $ make-qinv (e .from)
+  (make-inverses ((is-biinv→unique-inverse (e .has-biinv) ▷ e .to) ∙ e .is-section) (e .from-is-retraction))
 
 instance
+  @0 Types-is-category : is-category (Types ℓ)
+  Types-is-category .to-path e = ua (biinv→equiv e)
+  Types-is-category .to-path-over p = ≊-pathᴾ refl (Types-is-category .to-path p)
+    (fun-ext λ _ → =→ua-pathᴾ (biinv→equiv p) refl)
+
   Types-has-initial : Initial (Types ℓ)
   Types-has-initial .Initial.bot = ⊥
   Types-has-initial .Initial.has-⊥ _ .fst = λ ()

src/Cat/Diagram/Coproduct.agda

@@ -48,8 +48,8 @@ module _ {C : Precategory o h} where
 
   private variable A B : Ob
 
-  ⊎-unique : (c₁ c₂ : Coproduct C A B) → Coproduct.coapex c₁ ≅ Coproduct.coapex c₂
-  ⊎-unique c₁ c₂ = iso c₁→c₂ c₂→c₁ c₁→c₂→c₁ c₂→c₁→c₂
+  ⊎-unique : (c₁ c₂ : Coproduct C A B) → Coproduct.coapex c₁ ≊ Coproduct.coapex c₂
+  ⊎-unique c₁ c₂ = ≅→≊ $ iso c₁→c₂ c₂→c₁ c₁→c₂→c₁ c₂→c₁→c₂
     where
       module c₁ = Coproduct c₁
       module c₂ = Coproduct c₂

src/Cat/Diagram/Initial.agda

@@ -42,8 +42,8 @@ module _ {o h} {C : Precategory o h} where
   open Cat.Morphism C
   open Initial
 
-  ⊥-unique : (i i′ : Initial C) → bot i ≅ bot i′
-  ⊥-unique i i′ = iso (¡ i) (¡ i′) (¡-unique² i′ _ _) (¡-unique² i _ _)
+  ⊥-unique : (i i′ : Initial C) → bot i ≊ bot i′
+  ⊥-unique i i′ = ≅→≊ $ iso (¡ i) (¡ i′) (¡-unique² i′ _ _) (¡-unique² i _ _)
 
   opaque
     initial-is-prop : is-category C → is-prop (Initial C)

src/Cat/Diagram/Product.agda

@@ -55,8 +55,8 @@ module _ {C : Precategory o h} where
 
   private variable A B : Ob
 
-  ×-unique : (p₁ p₂ : Product C A B) → Product.apex p₁ ≅ Product.apex p₂
-  ×-unique p₁ p₂ = iso p₁→p₂ p₂→p₁ p₁→p₂→p₁ p₂→p₁→p₂
+  ×-unique : (p₁ p₂ : Product C A B) → Product.apex p₁ ≊ Product.apex p₂
+  ×-unique p₁ p₂ = ≅→≊ $ iso p₁→p₂ p₂→p₁ p₁→p₂→p₁ p₂→p₁→p₂
     where
       module p₁ = Product p₁
       module p₂ = Product p₂

src/Cat/Diagram/Pullback.agda

@@ -37,7 +37,7 @@ record is-pullback {P : Ob} (p₁ : P ⇒ X) (f : X ⇒ Z) (p₂ : P ⇒ Y) (g :
     → O ⇒ P
     ≃ Σ[ h ꞉ O ⇒ X ] Σ[ h′ ꞉ O ⇒ Y ] (f ∘ h ＝ g ∘ h′)
   pullback-univ .fst h = p₁ ∘ h , p₂ ∘ h , cat! C ∙ ap (_∘ h) square ∙ cat! C
-  pullback-univ .snd = is-inv→is-equiv $ invertible (λ (f , g , α) → universal α)
+  pullback-univ .snd = qinv→is-equiv $ qinv (λ (f , g , α) → universal α)
     (fun-ext λ _ → p₁∘universal ,ₚ p₂∘universal ,ₚ prop!)
     (fun-ext λ _ → unique refl refl ⁻¹)
 

src/Cat/Diagram/Terminal.agda

@@ -43,11 +43,11 @@ module _ {o h} {C : Precategory o h} where
   open Terminal
   open Iso
 
-  !-invertible : (t₁ t₂ : Terminal C) → is-invertible (! t₁ {top t₂})
-  !-invertible t₁ t₂ = invertible (! t₂) (!-unique² t₁ _ _) (!-unique² t₂ _ _)
+  !-qinv : (t₁ t₂ : Terminal C) → quasi-inverse (! t₁ {top t₂})
+  !-qinv t₁ t₂ = qinv (! t₂) (!-unique² t₁ _ _) (!-unique² t₂ _ _)
 
-  ⊤-unique : (t₁ t₂ : Terminal C) → top t₁ ≅ top t₂
-  ⊤-unique t₁ t₂ = is-inv→≅ (! t₂) (!-invertible t₂ t₁)
+  ⊤-unique : (t₁ t₂ : Terminal C) → top t₁ ≊ top t₂
+  ⊤-unique t₁ t₂ = ≅→≊ $ qinv→≅ (! t₂) (!-qinv t₂ t₁)
 
   opaque
     terminal-is-prop : is-category C → is-prop (Terminal C)

src/Cat/Displayed/Morphism.agda

@@ -16,6 +16,8 @@ private variable
 
 -- TODO mono, epi
 
+-- iso
+
 record Inverses[_]
   {a b : Ob} {a′ : Ob[ a ]} {b′ : Ob[ b ]}
   {f : Hom a b} {g : Hom b a}
@@ -28,50 +30,49 @@ record Inverses[_]
     inv-lᵈ : f′ ∘ᵈ g′ ＝[ Inverses.inv-o inv ] idᵈ
     inv-rᵈ : g′ ∘ᵈ f′ ＝[ Inverses.inv-i inv ] idᵈ
 
-record is-invertible[_]
+record quasi-inverse[_]
   {a b a′ b′} {f : Hom a b}
-  (f-inv : is-invertible f)
+  (f-inv : quasi-inverse f)
   (f′ : Hom[ f ] a′ b′)
   : Type ℓ′
   where
   no-eta-equality
   field
-    invᵈ      : Hom[ is-invertible.inv f-inv ] b′ a′
-    inversesᵈ : Inverses[ is-invertible.inverses f-inv ] f′ invᵈ
+    invᵈ      : Hom[ quasi-inverse.inv f-inv ] b′ a′
+    inversesᵈ : Inverses[ quasi-inverse.inverses f-inv ] f′ invᵈ
 
   open Inverses[_] inversesᵈ public
 
-open Iso
-
 record _≅[_]_
   {a b} (a′ : Ob[ a ]) (i : a ≅ b) (b′ : Ob[ b ])
   : Type ℓ′
   where
   no-eta-equality
+  open Iso
   field
     toᵈ       : Hom[ i .to ] a′ b′
     fromᵈ     : Hom[ i .from ] b′ a′
     inversesᵈ : Inverses[ i .inverses ] toᵈ fromᵈ
 
   open Inverses[_] inversesᵈ public
 
-open _≅[_]_ public
+-- open _≅[_]_ public
 
 _≅↓_ : {x : Ob} (A B : Ob[ x ]) → Type ℓ′
 _≅↓_ = _≅[ refl ]_
 
-is-invertible↓ : {x : Ob} {x′ x″ : Ob[ x ]} → Hom[ id ] x′ x″ → Type _
-is-invertible↓ = is-invertible[ id-invertible ]
+quasi-inverse↓ : {x : Ob} {x′ x″ : Ob[ x ]} → Hom[ id ] x′ x″ → Type _
+quasi-inverse↓ = quasi-inverse[ id-qinv ]
 
 make-invertible↓
   : ∀ {x} {x′ x″ : Ob[ x ]} {f′ : Hom[ id ] x′ x″}
   → (g′ : Hom[ id ] x″ x′)
-  → f′ ∘ᵈ g′ ＝[ id-l _ ] idᵈ
-  → g′ ∘ᵈ f′ ＝[ id-l _ ] idᵈ
-  → is-invertible↓ f′
-make-invertible↓ g′ p q .is-invertible[_].invᵈ = g′
-make-invertible↓ g′ p q .is-invertible[_].inversesᵈ .Inverses[_].inv-lᵈ = p
-make-invertible↓ g′ p q .is-invertible[_].inversesᵈ .Inverses[_].inv-rᵈ = q
+  → f′ ∘ᵈ g′ ＝[ id-r _ ] idᵈ
+  → g′ ∘ᵈ f′ ＝[ id-r _ ] idᵈ
+  → quasi-inverse↓ f′
+make-invertible↓ g′ p q .quasi-inverse[_].invᵈ = g′
+make-invertible↓ g′ p q .quasi-inverse[_].inversesᵈ .Inverses[_].inv-lᵈ = p
+make-invertible↓ g′ p q .quasi-inverse[_].inversesᵈ .Inverses[_].inv-rᵈ = q
 
 opaque
   Inverses[]-are-prop
@@ -88,11 +89,14 @@ opaque
       refl (Inverses[_].inv-rᵈ inv[]) (Inverses[_].inv-rᵈ inv[]′) refl i
 
   -- TODO
-  -- is-invertible[]-is-prop
+  -- quasi-inverse[]-is-prop
   --   : ∀ {a b a′ b′} {f : Hom a b}
-  --   → (f-inv : is-invertible f)
+  --   → (f-inv : quasi-inverse f)
   --   → (f′ : Hom[ f ] a′ b′)
-  --   → is-prop (is-invertible[ f-inv ] f′)
+  --   → is-prop (quasi-inverse[ f-inv ] f′)
+
+open Iso
+open _≅[_]_
 
 make-iso[_]
   : ∀ {a b : Ob} {a′ b′}
@@ -116,22 +120,98 @@ make-vertical-iso = make-iso[ refl ]
 
 invertible[]→iso[]
   : ∀ {a b a′ b′} {f : Hom a b} {f′ : Hom[ f ] a′ b′}
-  → {i : is-invertible f}
-  → is-invertible[ i ] f′
-  → a′ ≅[ is-inv→≅ f i ] b′
+  → {i : quasi-inverse f}
+  → quasi-inverse[ i ] f′
+  → a′ ≅[ qinv→≅ f i ] b′
 invertible[]→iso[] {f′ = f′} i =
   make-iso[ _ ]
     f′
-    (is-invertible[_].invᵈ i)
-    (is-invertible[_].inv-lᵈ i)
-    (is-invertible[_].inv-rᵈ i)
+    (quasi-inverse[_].invᵈ i)
+    (quasi-inverse[_].inv-lᵈ i)
+    (quasi-inverse[_].inv-rᵈ i)
+
+id-iso↓ : ∀ {x} {x′ : Ob[ x ]} → x′ ≅↓ x′
+id-iso↓ = make-iso[ refl ] idᵈ idᵈ (id-rᵈ idᵈ) (id-rᵈ idᵈ)
+
+
+-- equiv
+
+record has-retraction[_]
+  {a b : Ob} {a′ : Ob[ a ]} {b′ : Ob[ b ]}
+  {f : Hom a b} (hr : has-retraction f)
+  (f′ : Hom[ f ] a′ b′) : Type ℓ′
+  where
+  no-eta-equality
+  field
+    retractionᵈ    : Hom[ hr .retraction ] b′ a′
+    is-retractionᵈ : retractionᵈ ∘ᵈ f′ ＝[ hr .is-retraction ] idᵈ
+
+record has-section[_]
+  {a b : Ob} {a′ : Ob[ a ]} {b′ : Ob[ b ]}
+  {f : Hom a b} (hs : has-section f)
+  (f′ : Hom[ f ] a′ b′) : Type ℓ′
+  where
+  no-eta-equality
+  field
+    sectionᵈ    : Hom[ hs .section ] b′ a′
+    is-sectionᵈ : f′ ∘ᵈ sectionᵈ ＝[ hs .is-section ] idᵈ
+
+is-biinv[_] : ∀ {a b a′ b′} {f : Hom a b} (f-bi : is-biinv f) (f′ : Hom[ f ] a′ b′) → Type ℓ′
+is-biinv[_] (hr , hs) f′ = has-retraction[ hr ] f′ × has-section[ hs ] f′
+
+record _≊[_]_
+  {a b} (a′ : Ob[ a ]) (e : a ≊ b) (b′ : Ob[ b ]) : Type ℓ′
+  where
+  no-eta-equality
+  open Biinv
+  field
+    toᵈ        : Hom[ e .to ] a′ b′
+    has-biinvᵈ : is-biinv[ e .has-biinv ] toᵈ
+
+  open has-retraction[_] (has-biinvᵈ .fst)
+    renaming (retractionᵈ to fromᵈ ; is-retractionᵈ to from-is-retractionᵈ)
+    public
+  open has-section[_] (has-biinvᵈ .snd) public
+
+open _≊[_]_
+
+_≊↓_ : {x : Ob} (A B : Ob[ x ]) → Type ℓ′
+_≊↓_ = _≊[ refl ]_
+
+is-biinv↓ : {x : Ob} {x′ x″ : Ob[ x ]} → Hom[ id ] x′ x″ → Type _
+is-biinv↓ = is-biinv[ (make-retract id (id-l id)) , make-section id (id-l id) ]
+
+open Biinv
+open _≊[_]_
+
+make-equiv[_]
+  : ∀ {a b : Ob} {a′ b′}
+  → (e : a ≊ b)
+  → (f′ : Hom[ e .to ] a′ b′)
+    (r′ : Hom[ e .from ] b′ a′) (rr′ : r′ ∘ᵈ f′ ＝[ e .from-is-retraction ] idᵈ)
+    (s′ : Hom[ e .section ] b′ a′) (ss′ : f′ ∘ᵈ s′ ＝[ e .is-section ] idᵈ)
+  → a′ ≊[ e ] b′
+make-equiv[ _ ] f′ _  _   _  _   .toᵈ = f′
+make-equiv[ _ ] _  r′ _   _  _   .has-biinvᵈ .fst .has-retraction[_].retractionᵈ = r′
+make-equiv[ _ ] _  _  rr′ _  _   .has-biinvᵈ .fst .has-retraction[_].is-retractionᵈ = rr′
+make-equiv[ _ ] _  _  _   s′ _   .has-biinvᵈ .snd .has-section[_].sectionᵈ = s′
+make-equiv[ _ ] _  _  _   _  ss′ .has-biinvᵈ .snd .has-section[_].is-sectionᵈ = ss′
+
+make-vertical-equiv
+  : ∀ {x} {x′ x″ : Ob[ x ]}
+  → (f′ : Hom[ id ] x′ x″)
+    (r′ : Hom[ id ] x″ x′) (rr′ : r′ ∘ᵈ f′ ＝[ id-r id ] idᵈ)
+    (s′ : Hom[ id ] x″ x′) (ss′ : f′ ∘ᵈ s′ ＝[ id-r id ] idᵈ)
+  → x′ ≊↓ x″
+make-vertical-equiv = make-equiv[ refl ]
 
 -- TODO
--- ≅[]-path
---   : {x y : Ob} {A : Ob[ x ]} {B : Ob[ y ]} {f : x ≅ y}
---     {p q : A ≅[ f ] B}
---   → p .to′ ＝ q .to′
+-- ≊[]-path
+--   : {x y : Ob} {A : Ob[ x ]} {B : Ob[ y ]} {e : x ≊ y}
+--     {p q : A ≊[ e ] B}
+--   → p .toᵈ ＝ q .toᵈ
 --   → p ＝ q
+-- ≊[]-path r = {!!}
 
-id-iso↓ : ∀ {x} {x′ : Ob[ x ]} → x′ ≅↓ x′
-id-iso↓ = make-iso[ refl ] idᵈ idᵈ (id-rᵈ idᵈ) (id-rᵈ idᵈ)
+id-equiv↓ : ∀ {x} {x′ : Ob[ x ]} → x′ ≊↓ x′
+id-equiv↓ = make-equiv[ refl ] idᵈ idᵈ (id-rᵈ idᵈ) idᵈ (id-rᵈ idᵈ)

src/Cat/Displayed/Total.agda

@@ -67,3 +67,21 @@ module _ {o ℓ o′ ℓ′} {B : Precategory o ℓ} (E : Displayed B o′ ℓ
     (f .from .preserves)
     (preserves # f .inv-o)
     (preserves # f .inv-i)
+
+  open Biinv
+
+  total-equiv→equiv : x ≊ y → x .fst ≊ y .fst
+  total-equiv→equiv f = biinv
+    (f .to .hom)
+    (f .from .hom)
+    (hom # f .from-is-retraction)
+    (f .section .hom)
+    (hom # f .is-section)
+
+  total-equiv→equiv[] : ∀ {x y : ∫E.Ob} → (f : x ≊ y) → x .snd ≊[ total-equiv→equiv f ] y .snd
+  total-equiv→equiv[] f = make-equiv[ total-equiv→equiv f ]
+    (f .to .preserves)
+    (f .from .preserves)
+    (preserves # f .from-is-retraction)
+    (f .section .preserves)
+    (preserves # f .is-section)