From 54becd83181c32370687901e47c2da268de3ed8a Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 25 Apr 2024 15:26:35 +0200
Subject: [PATCH] Postulate components of coherent two-sided inverses for
 function extensionality and univalence (#1119)

Changes the postulates for funext and univalence such that there is
judgmentally only one converse map to `htpy-eq` and `equiv-eq`. The main
benefit, however, is that now `eq-htpy` and `eq-equiv` will appear with
their own names in Agda interactive mode, rather than as `pr1 (pr1
(funext ... ...))` and `pr1 (pr1 (univalence ... ...))`.

I leave it for potential future work to prove
`is-retraction-eq-(equiv|htpy)'` and `coh-eq-(equiv|htpy)'` rather than
postulate them, **_if_** we want this. Note that we could get away with
even fewer postulates if we really wanted to (see
[`TypeTopology/UF.Lower-FunExt`](https://www.cs.bham.ac.uk/~mhe/TypeTopology/UF.Lower-FunExt.html)).
---
 .../contractible-types.lagda.md               |  4 +-
 .../function-extensionality.lagda.md          | 57 +++++++++++++------
 src/foundation/identity-systems.lagda.md      | 45 ++++++++++-----
 src/foundation/univalence.lagda.md            | 46 +++++++++++----
 4 files changed, 106 insertions(+), 46 deletions(-)

diff --git a/src/foundation-core/contractible-types.lagda.md b/src/foundation-core/contractible-types.lagda.md
index 55bb4cc7d1..5e457cbe84 100644
--- a/src/foundation-core/contractible-types.lagda.md
+++ b/src/foundation-core/contractible-types.lagda.md
@@ -248,9 +248,7 @@ abstract
     ((x : A) → is-contr (B x)) → is-contr ((x : A) → B x)
   pr1 (is-contr-Π {A = A} {B = B} H) x = center (H x)
   pr2 (is-contr-Π {A = A} {B = B} H) f =
-    map-inv-is-equiv
-      ( funext (λ x → center (H x)) f)
-      ( λ x → contraction (H x) (f x))
+    eq-htpy (λ x → contraction (H x) (f x))
 
 abstract
   is-contr-implicit-Π :
diff --git a/src/foundation/function-extensionality.lagda.md b/src/foundation/function-extensionality.lagda.md
index 7ba761bdd8..5633842ad1 100644
--- a/src/foundation/function-extensionality.lagda.md
+++ b/src/foundation/function-extensionality.lagda.md
@@ -14,10 +14,13 @@ open import foundation.evaluation-functions
 open import foundation.implicit-function-types
 open import foundation.universe-levels
 
+open import foundation-core.coherently-invertible-maps
 open import foundation-core.equivalences
 open import foundation-core.function-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
+open import foundation-core.retractions
+open import foundation-core.sections
 ```
 
 </details>
@@ -127,9 +130,37 @@ function-extensionality-Level l1 l2 =
 ```agda
 function-extensionality : UUω
 function-extensionality = {l1 l2 : Level} → function-extensionality-Level l1 l2
+```
+
+Rather than postulating a witness of `function-extensionality` directly, we
+postulate the constituents of a coherent two-sided inverse to `htpy-eq`. The
+benefits are that we end up with a single converse map to `htpy-eq`, rather than
+a separate section and retraction, although they would be homotopic regardless.
+In addition, this formulation helps Agda display goals involving function
+extensionality in a more readable way.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g : (x : A) → B x}
+  where
 
-postulate
-  funext : function-extensionality
+  postulate
+    eq-htpy : f ~ g → f ＝ g
+
+    is-section-eq-htpy : is-section htpy-eq eq-htpy
+
+    is-retraction-eq-htpy' : is-retraction htpy-eq eq-htpy
+
+    coh-eq-htpy' :
+      coherence-is-coherently-invertible
+        ( htpy-eq)
+        ( eq-htpy)
+        ( is-section-eq-htpy)
+        ( is-retraction-eq-htpy')
+
+funext : function-extensionality
+funext f g =
+  is-equiv-is-invertible eq-htpy is-section-eq-htpy is-retraction-eq-htpy'
 
 module _
   {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
@@ -139,25 +170,19 @@ module _
   pr1 (equiv-funext) = htpy-eq
   pr2 (equiv-funext {f} {g}) = funext f g
 
-  eq-htpy : {f g : (x : A) → B x} → f ~ g → f ＝ g
-  eq-htpy {f} {g} = map-inv-is-equiv (funext f g)
+  is-equiv-eq-htpy :
+    (f g : (x : A) → B x) → is-equiv (eq-htpy {f = f} {g})
+  is-equiv-eq-htpy f g =
+    is-equiv-is-invertible htpy-eq is-retraction-eq-htpy' is-section-eq-htpy
 
   abstract
-    is-section-eq-htpy :
-      {f g : (x : A) → B x} → (htpy-eq ∘ eq-htpy {f} {g}) ~ id
-    is-section-eq-htpy {f} {g} = is-section-map-inv-is-equiv (funext f g)
-
     is-retraction-eq-htpy :
-      {f g : (x : A) → B x} → (eq-htpy ∘ htpy-eq {f = f} {g = g}) ~ id
+      {f g : (x : A) → B x} → is-retraction (htpy-eq {f = f} {g}) eq-htpy
     is-retraction-eq-htpy {f} {g} = is-retraction-map-inv-is-equiv (funext f g)
 
-    is-equiv-eq-htpy :
-      (f g : (x : A) → B x) → is-equiv (eq-htpy {f} {g})
-    is-equiv-eq-htpy f g = is-equiv-map-inv-is-equiv (funext f g)
-
-    eq-htpy-refl-htpy :
-      (f : (x : A) → B x) → eq-htpy (refl-htpy {f = f}) ＝ refl
-    eq-htpy-refl-htpy f = is-retraction-eq-htpy refl
+  eq-htpy-refl-htpy :
+    (f : (x : A) → B x) → eq-htpy (refl-htpy {f = f}) ＝ refl
+  eq-htpy-refl-htpy f = is-retraction-eq-htpy refl
 
   equiv-eq-htpy : {f g : (x : A) → B x} → (f ~ g) ≃ (f ＝ g)
   pr1 (equiv-eq-htpy {f} {g}) = eq-htpy
diff --git a/src/foundation/identity-systems.lagda.md b/src/foundation/identity-systems.lagda.md
index 44e04f05f9..9f1f3c9ff0 100644
--- a/src/foundation/identity-systems.lagda.md
+++ b/src/foundation/identity-systems.lagda.md
@@ -9,13 +9,17 @@ module foundation.identity-systems where
 ```agda
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
+open import foundation.function-extensionality
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.universe-levels
 
 open import foundation-core.contractible-types
 open import foundation-core.families-of-equivalences
+open import foundation-core.function-types
+open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.identity-types
 open import foundation-core.propositions
+open import foundation-core.retractions
 open import foundation-core.sections
 open import foundation-core.torsorial-type-families
 open import foundation-core.transport-along-identifications
@@ -79,27 +83,38 @@ module _
   {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (a : A) (b : B a)
   where
 
+  map-section-is-identity-system-is-torsorial :
+    is-torsorial B →
+    {l3 : Level} (P : (x : A) (y : B x) → UU l3) →
+    P a b → (x : A) (y : B x) → P x y
+  map-section-is-identity-system-is-torsorial H P p x y =
+    tr (fam-Σ P) (eq-is-contr H) p
+
+  is-section-map-section-is-identity-system-is-torsorial :
+    (H : is-torsorial B) →
+    {l3 : Level} (P : (x : A) (y : B x) → UU l3) →
+    is-section
+      ( ev-refl-identity-system b)
+      ( map-section-is-identity-system-is-torsorial H P)
+  is-section-map-section-is-identity-system-is-torsorial H P p =
+    ap
+      ( λ t → tr (fam-Σ P) t p)
+      ( eq-is-contr'
+        ( is-prop-is-contr H (a , b) (a , b))
+        ( eq-is-contr H)
+        ( refl))
+
   abstract
     is-identity-system-is-torsorial :
-      (H : is-torsorial B) → is-identity-system B a b
-    pr1 (is-identity-system-is-torsorial H P) p x y =
-      tr
-        ( fam-Σ P)
-        ( eq-is-contr H)
-        ( p)
-    pr2 (is-identity-system-is-torsorial H P) p =
-      ap
-        ( λ t → tr (fam-Σ P) t p)
-        ( eq-is-contr'
-          ( is-prop-is-contr H (a , b) (a , b))
-          ( eq-is-contr H)
-          ( refl))
+      is-torsorial B → is-identity-system B a b
+    is-identity-system-is-torsorial H P =
+      ( map-section-is-identity-system-is-torsorial H P ,
+        is-section-map-section-is-identity-system-is-torsorial H P)
 
   abstract
     is-torsorial-is-identity-system :
       is-identity-system B a b → is-torsorial B
-    pr1 (pr1 (is-torsorial-is-identity-system H)) = a
-    pr2 (pr1 (is-torsorial-is-identity-system H)) = b
+    pr1 (is-torsorial-is-identity-system H) = (a , b)
     pr2 (is-torsorial-is-identity-system H) (x , y) =
       pr1 (H (λ x' y' → (a , b) ＝ (x' , y'))) refl x y
 
diff --git a/src/foundation/univalence.lagda.md b/src/foundation/univalence.lagda.md
index d2ea5cb549..7b5a2bf621 100644
--- a/src/foundation/univalence.lagda.md
+++ b/src/foundation/univalence.lagda.md
@@ -16,6 +16,7 @@ open import foundation.equivalences
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.universe-levels
 
+open import foundation-core.coherently-invertible-maps
 open import foundation-core.contractible-types
 open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-pair-types
@@ -39,11 +40,37 @@ that the map `(A ＝ B) → (A ≃ B)` is an
 In this file we postulate the univalence axiom. Its statement is defined in
 [`foundation-core.univalence`](foundation-core.univalence.md).
 
-## Postulate
+## Postulates
+
+Rather than postulating a witness of `univalence-axiom` directly, we postulate
+the constituents of a coherent two-sided inverse to `equiv-eq`. The benefits are
+that we end up with a single converse map to `equiv-eq`, rather than a separate
+section and retraction, although they would be homotopic regardless. In
+addition, this formulation helps Agda display goals involving the univalence
+axiom in a more readable way.
 
 ```agda
-postulate
-  univalence : univalence-axiom
+module _
+  {l : Level} {A B : UU l}
+  where
+
+  postulate
+    eq-equiv : A ≃ B → A ＝ B
+
+    is-section-eq-equiv : is-section equiv-eq eq-equiv
+
+    is-retraction-eq-equiv' : is-retraction equiv-eq eq-equiv
+
+    coh-eq-equiv' :
+      coherence-is-coherently-invertible
+        ( equiv-eq)
+        ( eq-equiv)
+        ( is-section-eq-equiv)
+        ( is-retraction-eq-equiv')
+
+univalence : univalence-axiom
+univalence A B =
+  is-equiv-is-invertible eq-equiv is-section-eq-equiv is-retraction-eq-equiv'
 ```
 
 ## Properties
@@ -57,14 +84,8 @@ module _
   pr1 equiv-univalence = equiv-eq
   pr2 equiv-univalence = univalence A B
 
-  eq-equiv : A ≃ B → A ＝ B
-  eq-equiv = map-inv-is-equiv (univalence A B)
-
   abstract
-    is-section-eq-equiv : is-section equiv-eq eq-equiv
-    is-section-eq-equiv = is-section-map-inv-is-equiv (univalence A B)
-
-    is-retraction-eq-equiv : is-retraction equiv-eq eq-equiv
+    is-retraction-eq-equiv : is-retraction (equiv-eq {A = A} {B}) eq-equiv
     is-retraction-eq-equiv =
       is-retraction-map-inv-is-equiv (univalence A B)
 
@@ -72,8 +93,9 @@ module _
   {l : Level}
   where
 
-  is-equiv-eq-equiv : (A B : UU l) → is-equiv (eq-equiv)
-  is-equiv-eq-equiv A B = is-equiv-map-inv-is-equiv (univalence A B)
+  is-equiv-eq-equiv : (A B : UU l) → is-equiv (eq-equiv {A = A} {B})
+  is-equiv-eq-equiv A B =
+    is-equiv-is-invertible equiv-eq is-retraction-eq-equiv' is-section-eq-equiv
 
   compute-eq-equiv-id-equiv : (A : UU l) → eq-equiv {A = A} id-equiv ＝ refl
   compute-eq-equiv-id-equiv A = is-retraction-eq-equiv refl