------------------------------------------------------------------------
-- 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                                      )