delete funext muhahaha

UniMath · Oct 22, 2023 · af8d63a · af8d63a
1 parent cfa14d2
commit af8d63a
Show file tree

Hide file tree

Showing 6 changed files with 7 additions and 90 deletions.
diff --git a/src/foundation-core.lagda.md b/src/foundation-core.lagda.md
@@ -25,7 +25,6 @@ open import foundation-core.equality-dependent-pair-types public
 open import foundation-core.equivalence-relations public
 open import foundation-core.equivalences public
 open import foundation-core.fibers-of-maps public
-open import foundation-core.function-extensionality public
 open import foundation-core.function-types public
 open import foundation-core.functoriality-dependent-function-types public
 open import foundation-core.functoriality-dependent-pair-types public

diff --git a/src/foundation-core/function-extensionality.lagda.md b/src/foundation-core/function-extensionality.lagda.md
diff --git a/src/foundation/lifts-families-of-elements.lagda.md b/src/foundation/lifts-families-of-elements.lagda.md
@@ -13,6 +13,7 @@ open import foundation.commuting-triangles-of-maps
 open import foundation.function-extensionality
 open import foundation.functoriality-dependent-pair-types
 open import foundation.homotopies
+open import foundation.homotopy-induction
 open import foundation.transport-along-homotopies
 open import foundation.type-theoretic-principle-of-choice
 open import foundation.universe-levels
@@ -169,7 +170,7 @@ again constructed by homotopy induction.
 ```agda
 COHERENCE-TRIANGLE-PRECOMPOSE-LIFTS :
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4)
-  {f g : A → B} (H : f ~ g) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  {f g : A → B} (H : f ~ g) → UU ?
 COHERENCE-TRIANGLE-PRECOMPOSE-LIFTS {A = A} {B} {X} P {f} {g} H =
   (h : B → X) →
   ( triangle-precompose-lifts P H h) ~

diff --git a/src/foundation/negated-equality.lagda.md b/src/foundation/negated-equality.lagda.md
@@ -10,11 +10,11 @@ module foundation.negated-equality where
 open import foundation.action-on-identifications-functions
 open import foundation.binary-relations
 open import foundation.dependent-pair-types
+open import foundation.function-extensionality
 open import foundation.negation
 open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
-open import foundation-core.function-extensionality
 open import foundation-core.identity-types
 open import foundation-core.propositions
 ```

diff --git a/src/foundation/transport-along-higher-identifications.lagda.md b/src/foundation/transport-along-higher-identifications.lagda.md
@@ -13,9 +13,10 @@ open import foundation.dependent-pair-types
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.path-algebra
-open import foundation-core.transport-along-identifications
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies
+
+open import foundation-core.transport-along-identifications
 ```
 
 </details>

diff --git a/src/foundation/transport-along-homotopies.lagda.md b/src/foundation/transport-along-homotopies.lagda.md
@@ -10,6 +10,8 @@ module foundation.transport-along-homotopies where
 open import foundation.action-on-identifications-functions
 open import foundation.function-extensionality
 open import foundation.homotopies
+open import foundation.homotopy-induction
+open import foundation.transport-along-higher-identifications
 open import foundation.universe-levels
 
 open import foundation-core.identity-types