open import Equality.Path as P hiding (Is-proposition; Is-set)
module README.Not-a-set
{e⁺} (eq : ∀ {a p} → Equality-with-paths a p e⁺) where
private
open module D = Derived-definitions-and-properties eq
using (Is-proposition; Is-set)
open import Equality.Path.Univalence
open import Prelude
open import Bijection equality-with-J as Bijection using (_↔_)
import Bijection D.equality-with-J as DB
import Bool equality-with-J as B
open import Equality.Decision-procedures equality-with-J
import Equality.Path.Isomorphisms eq as I
import Erased.Cubical eq as E
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J as F hiding (id; _∘_)
import H-level D.equality-with-J as H-level
open import H-level.Closure D.equality-with-J
open import Surjection D.equality-with-J using (_↠_)
private
variable
A B C : Type
Printable : Type₁
Printable = ∃ λ (A : Type) → A × (A → String)
¬-Printable-set : ¬ Is-set Printable
¬-Printable-set =
E.Stable-¬
E.[ Is-set Printable ↝⟨ DB._↔_.to (I.H-level↔H-level 2) ⟩
P.Is-set Printable ↝⟨ (λ h → h _ _) ⟩
refl ≡ q ↝⟨ cong (cong proj₁) ⟩
refl ≡ cong proj₁ q ↝⟨ flip trans (proj₁-Σ-≡,≡→≡ {B = λ A → A × (A → String)} {y₁ = proj₂ x} _ refl) ⟩
refl ≡ q′ ↝⟨ cong (λ eq → subst id eq (just true)) ⟩
just true ≡ just false ↝⟨ Bool.true≢false ∘ ⊎.cancel-inj₂ ⟩□
⊥ □
]
where
x : Printable
x = Maybe Bool , nothing , λ _ → ""
@0 q′ : Maybe Bool ≡ Maybe Bool
q′ = ≃⇒≡ (F.id ⊎-cong Eq.↔⇒≃ B.swap)
@0 q : x ≡ x
q = Σ-≡,≡→≡ q′ refl
data Step (A S : Type) : Type where
done : Step A S
yield : A → S → Step A S
skip : S → Step A S
Stream : Type → Type₁
Stream A = ∃ λ (S : Type) → (S → Step A S) × S
¬-Stream-set : ¬ Is-set (Stream A)
¬-Stream-set {A = A} =
E.Stable-¬
E.[ Is-set (Stream A) ↝⟨ DB._↔_.to (I.H-level↔H-level 2) ⟩
P.Is-set (Stream A) ↝⟨ (λ h → h _ _) ⟩
refl ≡ p ↝⟨ cong (cong proj₁) ⟩
refl ≡ cong proj₁ p ↝⟨ flip trans (proj₁-Σ-≡,≡→≡ {B = F} {y₁ = proj₂ t} _ refl) ⟩
refl ≡ q ↝⟨ cong (λ eq → subst id eq (just true)) ⟩
just true ≡ just false ↝⟨ Bool.true≢false ∘ ⊎.cancel-inj₂ ⟩□
⊥ □
]
where
F : Type → Type
F S = (S → Step A S) × S
t : Stream A
t = Maybe Bool
, const done
, nothing
@0 q : Maybe Bool ≡ Maybe Bool
q = ≃⇒≡ (F.id ⊎-cong Eq.↔⇒≃ B.swap)
@0 p : t ≡ t
p = Σ-≡,≡→≡ q refl
Streamˢ : Type → Type₁
Streamˢ A = ∃ λ (S : Type) → Is-set S × (S → Step A S) × S
¬-Streamˢ-set : ¬ Is-set (Streamˢ A)
¬-Streamˢ-set {A = A} =
E.Stable-¬
E.[ Is-set (Streamˢ A) ↝⟨ DB._↔_.to (I.H-level↔H-level 2) ⟩
P.Is-set (Streamˢ A) ↝⟨ (λ h → h _ _) ⟩
refl ≡ p ↝⟨ cong (cong proj₁) ⟩
refl ≡ cong proj₁ p ↝⟨ flip trans (proj₁-Σ-≡,≡→≡ {B = F} {y₁ = proj₂ t} _ refl) ⟩
refl ≡ q ↝⟨ cong (λ eq → subst id eq (inj₂ true)) ⟩
just true ≡ just false ↝⟨ Bool.true≢false ∘ ⊎.cancel-inj₂ ⟩□
⊥ □
]
where
F : Type → Type
F S = Is-set S × (S → Step A S) × S
t : Streamˢ A
t = Maybe Bool
, Maybe-closure 0 Bool-set
, const done
, nothing
@0 q : Maybe Bool ≡ Maybe Bool
q = ≃⇒≡ (F.id ⊎-cong Eq.↔⇒≃ B.swap)
@0 p : t ≡ t
p =
Σ-≡,≡→≡ q $
cong₂ _,_
(DB._↔_.to D.≡↔≡ (H-level-propositional I.ext 2 _ _))
refl
module Tm-with-predicate
(P : Type → Type)
(P-Maybe-Bool : P (Maybe Bool))
(P-Maybe-Bool-propositional : Is-proposition (P (Maybe Bool)))
where
data Tm (A : Type) : Type₁ where
literal : A → Tm A
map : {B : Type} → P B → Tm (B → A) → Tm B → Tm A
Tm≃ : Tm A ≃ (A ⊎ ∃ λ (B : Type) → P B × Tm (B → A) × Tm B)
Tm≃ = Eq.↔→≃
(λ where
(literal x) → inj₁ x
(map p f t) → inj₂ (_ , p , f , t))
[ literal , (λ (_ , p , f , t) → map p f t) ]
[ (λ _ → refl) , (λ _ → refl) ]
(λ where
(literal _) → refl
(map _ _ _) → refl)
¬-Tm-set : A → ¬ Is-set (Tm A)
¬-Tm-set {A = A} a =
E.Stable-¬
E.[ Is-set (Tm A) ↝⟨ DB._↔_.to (I.H-level↔H-level 2) ⟩
P.Is-set (Tm A) ↝⟨ (λ h → h _ _) ⟩
refl ≡ p ↝⟨ cong map-injective ⟩
refl ≡ map-injective p ↝⟨ flip trans lemma ⟩
refl ≡ p₁ ↝⟨ cong (λ eq → subst id eq (just true)) ⟩
just true ≡ just false ↝⟨ Bool.true≢false ∘ ⊎.cancel-inj₂ ⟩□
⊥ □
]
where
F : Type → Type₁
F B = P B × Tm (B → A) × Tm B
t : Tm A
t = map P-Maybe-Bool (literal λ _ → a) (literal nothing)
t′ : F (Maybe Bool)
t′ = P-Maybe-Bool
, literal (const a)
, literal nothing
@0 p₁ : Maybe Bool ≡ Maybe Bool
p₁ = ≃⇒≡ (F.id ⊎-cong Eq.↔⇒≃ B.swap)
@0 p₂ : subst F p₁ t′ ≡ t′
p₂ =
cong₂ _,_
(DB._↔_.to (I.H-level↔H-level 1) P-Maybe-Bool-propositional _ _)
(cong (_, literal nothing)
(subst (λ B → Tm (B → A)) p₁ (literal (const a)) ≡⟨⟩
literal (subst (λ B → B → A) p₁ (const a)) ≡⟨ (cong literal $ ⟨ext⟩ λ b → subst-→-domain id p₁ {u = b}) ⟩∎
literal (const a) ∎))
@0 p : t ≡ t
p = _≃_.to (Eq.≃-≡ Tm≃) $ cong inj₂ $ Σ-≡,≡→≡ p₁ p₂
map-injective :
{p : P B} {f : Tm (B → C)} {t : Tm B} →
map p f t ≡ map p f t → B ≡ B
map-injective {B = B} {p = p} {f = f} {t = t} =
map p f t ≡ map p f t ↔⟨ inverse $ Eq.≃-≡ Tm≃ ⟩
_≃_.to Tm≃ (map p f t) ≡ _≃_.to Tm≃ (map p f t) ↔⟨⟩
inj₂ (B , p , f , t) ≡ inj₂ (B , p , f , t) ↔⟨ inverse Bijection.≡↔inj₂≡inj₂ ⟩
(B , p , f , t) ≡ (B , p , f , t) ↝⟨ cong proj₁ ⟩□
B ≡ B □
@0 lemma : map-injective p ≡ p₁
lemma =
map-injective p ≡⟨⟩
cong proj₁ (⊎.cancel-inj₂
(_≃_.from (Eq.≃-≡ Tm≃) (_≃_.to (Eq.≃-≡ Tm≃)
(cong inj₂ (Σ-≡,≡→≡ p₁ p₂))))) ≡⟨ cong (cong proj₁ ∘ ⊎.cancel-inj₂) $
_≃_.left-inverse-of (Eq.≃-≡ Tm≃) (cong inj₂ (Σ-≡,≡→≡ p₁ p₂)) ⟩
cong (proj₁ {B = F})
(⊎.cancel-inj₂ {A = ⊤ ⊎ ⊤} (cong inj₂
(Σ-≡,≡→≡ {p₁ = _ , t′} p₁ p₂))) ≡⟨ cong (cong (proj₁ {B = F})) $
_↔_.left-inverse-of (Bijection.≡↔inj₂≡inj₂ {A = ⊤ ⊎ ⊤}) (Σ-≡,≡→≡ {p₁ = _ , t′} _ refl) ⟩
cong (proj₁ {B = F})
(Σ-≡,≡→≡ {p₁ = _ , t′} p₁ p₂) ≡⟨ proj₁-Σ-≡,≡→≡ {B = F} {y₁ = t′} _ refl ⟩∎
p₁ ∎
data Tm (A : Type) : Type₁ where
literal : A → Tm A
map : {B : Type} → Tm (B → A) → Tm B → Tm A
¬-Tm-set : A → ¬ Is-set (Tm A)
¬-Tm-set {A = A} a =
Is-set (Tm A) ↝⟨ H-level.respects-surjection Tm↠Tm 2 ⟩
Is-set (T.Tm A) ↝⟨ T.¬-Tm-set a ⟩□
⊥ □
where
module T = Tm-with-predicate (λ _ → ⊤) _ (λ _ _ → D.refl _)
to : Tm B → T.Tm B
to (literal x) = T.literal x
to (map f t) = T.map _ (to f) (to t)
from : T.Tm B → Tm B
from (T.literal x) = literal x
from (T.map _ f t) = map (from f) (from t)
to-from : (t : T.Tm B) → to (from t) D.≡ t
to-from (T.literal x) = D.refl _
to-from (T.map _ f t) = D.cong₂ (T.map _) (to-from f) (to-from t)
Tm↠Tm : Tm B ↠ T.Tm B
Tm↠Tm = record
{ logical-equivalence = record
{ to = to
; from = from
}
; right-inverse-of = to-from
}
data Tmˢ (A : Type) : Type₁ where
literal : A → Tmˢ A
map : {B : Type} → Is-set B → Tmˢ (B → A) → Tmˢ B → Tmˢ A
¬-Tmˢ-set : A → ¬ Is-set (Tmˢ A)
¬-Tmˢ-set {A = A} a =
Is-set (Tmˢ A) ↝⟨ H-level.respects-surjection Tmˢ↠Tm 2 ⟩
Is-set (T.Tm A) ↝⟨ T.¬-Tm-set a ⟩□
⊥ □
where
module T = Tm-with-predicate
Is-set
(Maybe-closure 0 Bool-set)
(H-level-propositional I.ext 2)
to : Tmˢ B → T.Tm B
to (literal x) = T.literal x
to (map s f t) = T.map s (to f) (to t)
from : T.Tm B → Tmˢ B
from (T.literal x) = literal x
from (T.map s f t) = map s (from f) (from t)
to-from : (t : T.Tm B) → to (from t) D.≡ t
to-from (T.literal x) = D.refl _
to-from (T.map s f t) = D.cong₂ (T.map s) (to-from f) (to-from t)
Tmˢ↠Tm : Tmˢ B ↠ T.Tm B
Tmˢ↠Tm = record
{ logical-equivalence = record
{ to = to
; from = from
}
; right-inverse-of = to-from
}