# Strongly extensional maps

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

Created on 2022-09-15.

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 = {!!}