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

{-# OPTIONS --cubical-compatible --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 Extensionality eq
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 : Type a} {B : Type b} →
  A → Injective {B = A → B} const
const-is-injective x {x = y} {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 : Type a} {B : Type 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)  λ _ →
             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 (# ) →
  ¬ ({A : Type a} {B : Type (lsuc b)} →
     A → Is-embedding {B = A → B} const)
const-is-not-embedding {a} {b} ext univ univ₀ hyp =
  from-⊎ ( Nat.≟ ) 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 (# ) (# )
  ext₁ = lower-extensionality _ (lsuc b) ext

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

  emb : Is-embedding {B = ↑ a (Fin ) → Type b} const
  emb = hyp (lift true)

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