------------------------------------------------------------------------
-- Some properties related to the const function
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Equality

module Const
{reflexive} (eq :  {a p}  Equality-with-J a p reflexive) where

open import Logical-equivalence using (_⇔_)
open import Prelude

import Bijection eq as Bijection
open Derived-definitions-and-properties eq
open import Embedding eq
open import Equivalence eq as Eq using (_≃_)
open import Fin eq
open import Function-universe eq
open import H-level eq
open import H-level.Closure eq
open import Injection eq using (Injective)
import Nat eq as Nat
open import Univalence-axiom eq

-- If A is inhabited, then the function const : B → (A → B) is
-- injective.

const-is-injective :
{a b}
{A : Set a} {B : Set b}
A  Injective {B = A  B} const
const-is-injective x {y} {z} =
const y  const z  ↝⟨ cong (_\$ x) ⟩□
y  z

-- Thus, if B is a set, then const is also an embedding (assuming
-- extensionality).

const-is-embedding :
{a b}
Extensionality (a  b) (a  b)
{A : Set a} {B : Set b}
Is-set B
A  Is-embedding {B = A  B} const
const-is-embedding {a} {b} ext B-set x =
_≃_.to (Injective≃Is-embedding
ext B-set
(Π-closure (lower-extensionality b a ext) 2 λ _
B-set)
const)
(const-is-injective x)

-- However, if B is not a set, then one can construct a counterexample
-- (assuming extensionality and univalence).
--
-- This example is due to Thierry Coquand. (His proof was not
-- identical to the one below.)

const-is-not-embedding :
{a b}
Extensionality (a  b) (lsuc b)
Univalence b
Univalence (# 0)
¬ ({A : Set a} {B : Set (lsuc b)}
A  Is-embedding {B = A  B} const)
const-is-not-embedding {a} {b} ext univ univ₀ hyp =
from-⊎ (2 Nat.≟ 4) 2≡4
where
ext-b : Extensionality b b
ext-b = lower-extensionality a (lsuc b) ext

ext-ab₊ : Extensionality a (lsuc b)
ext-ab₊ = lower-extensionality b lzero ext

ext₁ : Extensionality (# 0) (# 1)
ext₁ = lower-extensionality _ (lsuc b) ext

ext₀ : Extensionality (# 0) (# 0)
ext₀ = lower-extensionality _ _ ext

emb : Is-embedding {B =  a (Fin 2)  Set b} const
emb = hyp (lift true)

2≡4 : 2  4
2≡4 = _⇔_.to isomorphic-same-size (
Fin 2                                      ↝⟨ inverse \$ [Fin≡Fin]↔Fin! ext₀ univ₀ 2
Fin 2  Fin 2                              ↔⟨ inverse \$ ≡-preserves-≃ ext-b univ univ₀ (Eq.↔⇒≃ Bijection.↑↔) (Eq.↔⇒≃ Bijection.↑↔)
b (Fin 2)   b (Fin 2)                  ↔⟨ Eq.⟨ _ , emb ( b (Fin 2)) ( b (Fin 2))
const ( b (Fin 2))  const ( b (Fin 2))  ↔⟨ inverse \$ Eq.extensionality-isomorphism ext-ab₊
( a (Fin 2)   b (Fin 2)   b (Fin 2))  ↔⟨ →-cong ext-ab₊ (Eq.↔⇒≃ Bijection.↑↔)
(≡-preserves-≃ ext-b univ univ₀ (Eq.↔⇒≃ Bijection.↑↔) (Eq.↔⇒≃ Bijection.↑↔))
(Fin 2  Fin 2  Fin 2)                    ↝⟨ ∀-cong ext₁  _  [Fin≡Fin]↔Fin! ext₀ univ₀ 2)
(Fin 2  Fin 2)                            ↝⟨ [Fin→Fin]↔Fin^ ext₀ 2 2 ⟩□
Fin 4                                      )