Strongly extensional maps

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-09-15.
Last modified on 2024-01-17.

module foundation.strongly-extensional-maps where
Imports 
open import foundation.apartness-relations
open import foundation.universe-levels

Idea

Consider a function f : A → B between types equipped with apartness relations. Then we say that f is strongly extensional if

  f x # f y → x # y

Definition

strongly-extensional :
  {l1 l2 l3 l4 : Level} (A : Type-With-Apartness l1 l2)
  (B : Type-With-Apartness l3 l4) →
  (type-Type-With-Apartness A → type-Type-With-Apartness B) → UU (l1 ⊔ l2 ⊔ l4)
strongly-extensional A B f =
  (x y : type-Type-With-Apartness A) →
  apart-Type-With-Apartness B (f x) (f y) → apart-Type-With-Apartness A x y

Properties

is-strongly-extensional :
  {l1 l2 l3 l4 : Level} (A : Type-With-Apartness l1 l2)
  (B : Type-With-Apartness l3 l4) →
  (f : type-Type-With-Apartness A → type-Type-With-Apartness B) →
  strongly-extensional A B f
is-strongly-extensional A B f x y H = {!!}

Recent changes