Left cancellable maps.

The definition is given in UF.Base. Here we prove things about them.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}

module UF.LeftCancellable where

open import MLTT.Spartan
open import UF.Base
open import UF.Subsingletons
open import UF.Retracts
open import UF.Equiv

left-cancellable-reflects-is-prop : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                                 β†’ left-cancellable f β†’ is-prop Y β†’ is-prop X
left-cancellable-reflects-is-prop f lc i x x' = lc (i (f x) (f x'))

section-lc : {X : 𝓀 Μ‡ } {A : π“₯ Μ‡ } (s : X β†’ A) β†’ is-section s β†’ left-cancellable s
section-lc {𝓀} {π“₯} {X} {Y} s (r , rs) {x} {y} p = (rs x)⁻¹ βˆ™ ap r p βˆ™ rs y

is-equiv-lc : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) β†’ is-equiv f β†’ left-cancellable f
is-equiv-lc f (_ , hasr) = section-lc f hasr

left-cancellable-closed-under-∘ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } (f : X β†’ Y) (g : Y β†’ Z)
                                β†’ left-cancellable f β†’ left-cancellable g β†’ left-cancellable (g ∘ f)
left-cancellable-closed-under-∘ f g lcf lcg = lcf ∘ lcg

NatΞ£-lc : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {B : X β†’ 𝓦 Μ‡ } (f : Nat A B)
        β†’ ((x : X) β†’ left-cancellable(f x))
        β†’ left-cancellable (NatΞ£ f)
NatΞ£-lc {𝓀} {π“₯} {𝓦} {X} {A} {B} f flc {x , a} {x' , a'} p = to-Ξ£-＝ (ap pr₁ p , Ξ³)
 where
  Ξ³ : transport A (ap pr₁ p) a ＝ a'
  Ξ³ = flc x' (f x' (transport A (ap pr₁ p) a) ＝⟨ nat-transport f (ap pr₁ p) ⟩
              transport B (ap pr₁ p) (f x a)  ＝⟨ from-Ξ£-＝' p ⟩
              f x' a'                         ∎)

NatΞ -lc : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {B : X β†’ 𝓦 Μ‡ } (f : Nat A B)
        β†’ ((x : X) β†’ left-cancellable(f x))
        β†’ {g g' : Ξ  A} β†’ NatΞ  f g ＝ NatΞ  f g' β†’ g ∼ g'
NatΞ -lc f flc {g} {g'} p x = flc x (happly p x)

\end{code}

Sometimes the type of left cancellable maps is useful (but more often
the type of embeddings, defined elsewhere, is useful).

\begin{code}

_↣_ : 𝓀 Μ‡ β†’ π“₯ Μ‡ β†’ 𝓀 βŠ” π“₯ Μ‡
X ↣ Y =  Ξ£ f κž‰ (X β†’ Y) , left-cancellable f

⌈_βŒ‰ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ X ↣ Y β†’ X β†’ Y
⌈ f , _ βŒ‰ = f

infix 0 _↣_

\end{code}