GSaha567/seq_level_training_data
052
1text,length,is_long_context,metric_val,label_metric2"module Esterel.Lang.CanFunction.Plug where3 4open import Data.Nat using (_+_ ; suc)5open import Function using (_∋_ ; _∘_ ; id ; _$_)6open import Data.Nat.Properties.Simple using ( +-comm ; +-assoc)7open import utility8open import Esterel.Lang9open import Esterel.Lang.Properties10open import Esterel.Lang.CanFunction11open import Esterel.Environment as Env12open import Esterel.Context13open import Esterel.Context.Properties14open import Data.Product15open import Data.Sum16open import Data.Bool17open import Data.List using ([] ; [_] ; _∷_ ; List ; _++_)18open import Relation.Nullary19open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; subst ; cong ; trans ; module ≡-Reasoning ; cong₂ ; subst₂ ; inspect)20open import Data.Empty21open import Esterel.Lang.Binding22open import Data.Maybe using ( nothing ; just )23open import Data.List.Any24open import Data.List.Any.Properties25 renaming (++⁺ˡ to ++ˡ ; ++⁺ʳ to ++ʳ )26open import Esterel.Lang.CanFunction.SetSigMonotonic27 28open ≡-Reasoning using (_≡⟨_⟩_ ; _≡⟨⟩_ ; _∎)29 30open import Relation.Nullary.Decidable31 using (⌊_⌋)32open import Data.FiniteMap33import Data.OrderedListMap as OMap34open import Data.Nat as Nat using (ℕ)35open import Esterel.Variable.Signal as Signal36 using (Signal ; _ₛ ; _≟ₛₜ_)37open import Esterel.Variable.Shared as SharedVar38 using (SharedVar ; _ₛₕ)39open import Esterel.Variable.Sequential as SeqVar40 using (SeqVar ; _ᵥ)41open import Esterel.CompletionCode as Code renaming (CompletionCode to Code)42 43open import Data.OrderedListMap Signal Signal.unwrap Signal.Status as SigM44open import Data.OrderedListMap SharedVar SharedVar.unwrap (Σ SharedVar.Status (λ _ → ℕ)) as ShrM45open import Data.OrderedListMap SeqVar SeqVar.unwrap ℕ as SeqM46open ListSet Code._≟_47module NSet = ListSet Nat._≟_48 49canθₖ-plug : ∀ S' sigs → ∀ C p q50 → (Canₖq⊆Canₖp : ∀ θ k → k ∈ (Canₖ q θ) → k ∈ (Canₖ p θ))51 → (Canₛq⊆Canₛp : ∀ θ S → S ∈ (Canₛ q θ) → S ∈ (Canₛ p θ))52 → (∀ θ k → k ∈ (Canθₖ sigs S' (C ⟦ q ⟧c) θ) → k ∈ (Canθₖ sigs S' (C ⟦ p ⟧c) θ))53 54canθₛ-plug : ∀ S' sigs → ∀ C p q55 → (Canₛq⊆Canₛp : ∀ θ S → S ∈ (Canₛ q θ) → S ∈ (Canₛ p θ))56 → (Canₖq⊆Canₖp : ∀ θ k → k ∈ (Canₖ q θ) → k ∈ (Canₖ p θ))57 → (∀ θ k → k ∈ (Canθₛ sigs S' (C ⟦ q ⟧c) θ) → k ∈ (Canθₛ sigs S' (C ⟦ p ⟧c) θ))58canθₛₕ-plug : ∀ S' sigs → ∀ C p q59 → (Canₛₕq⊆Canₛₕp : ∀ θ → (Canₛₕ q θ) ⊆¹ (Canₛₕ p θ))60 → (Canₛq⊆Canₛp : ∀ θ k → k ∈ (Canₖ q θ) → k ∈ (Canₖ p θ))61 → (Canₖq⊆Canₖp : ∀ θ S → S ∈ (Canₛ q θ) → S ∈ (Canₛ p θ))62 → (∀ θ k → k ∈ (Canθₛₕ sigs S' (C ⟦ q ⟧c) θ) → k ∈ (Canθₛₕ sigs S' (C ⟦ p ⟧c) θ))63 64 65 66canₛₕ-plug : ∀ C p q67 → (Canₛₕq⊆Canₛₕp : ∀ θ → (Canₛₕ q θ) ⊆¹ (Canₛₕ p θ))68 → (∀ θ k → k ∈ (Canₖ q θ) → k ∈ (Canₖ p θ))69 → (Canₛq⊆Canₛp : ∀ θ → (Canₛ q θ) ⊆¹ (Canₛ p θ))70 → (∀ θ → (Canₛₕ (C ⟦ q ⟧c) θ) ⊆¹ (Canₛₕ (C ⟦ p ⟧c) θ))71 72canₖ-plug : ∀ C p q73 → (Canₖq⊆Canₖp : ∀ θ k → k ∈ (Canₖ q θ) → k ∈ (Canₖ p θ))74 → (Canₛq⊆Canₛp : ∀ θ S → S ∈ (Canₛ q θ) → S ∈ (Canₛ p θ))75 → (∀ θ k → k ∈ (Canₖ (C ⟦ q ⟧c) θ) → k ∈ (Canₖ (C ⟦ p ⟧c) θ))76canₛ-plug : ∀ C p q77 → (Canₛq⊆Canₛp : ∀ θ → (Canₛ q θ) ⊆¹ (Canₛ p θ))78 → (∀ θ k → k ∈ (Canₖ q θ) → k ∈ (Canₖ p θ))79 → (∀ θ → (Canₛ (C ⟦ q ⟧c) θ) ⊆¹ (Canₛ (C ⟦ p ⟧c) θ))80 81canθₖ-plug S' [] C p q Canₖq⊆Canₖp Canₛq⊆Canₛp = canₖ-plug C p q Canₖq⊆Canₖp Canₛq⊆Canₛp82canθₖ-plug S' (just Signal.present ∷ sigs) C p q Canₖq⊆Canₖp Canₛq⊆Canₛp θ = canθₖ-plug (suc S') sigs C p q Canₖq⊆Canₖp Canₛq⊆Canₛp (θ ← _)83canθₖ-plug S' (just Signal.absent ∷ sigs) C p q Canₖq⊆Canₖp Canₛq⊆Canₛp θ = canθₖ-plug (suc S') sigs C p q Canₖq⊆Canₖp Canₛq⊆Canₛp (θ ← _)84canθₖ-plug S' (nothing ∷ sigs) C p q Canₖq⊆Canₖp Canₛq⊆Canₛp = canθₖ-plug (suc S') sigs C p q Canₖq⊆Canₖp Canₛq⊆Canₛp85canθₖ-plug S' (just Signal.unknown ∷ sigs) C p q Canₖq⊆Canₖp Canₛq⊆Canₛp θ86 with any (Nat._≟_ S') (Canθₛ sigs (suc S') (C ⟦ p ⟧c) (θ ← ([S]-env (S' ₛ))))87 | any (Nat._≟_ S') (Canθₛ sigs (suc S') (C ⟦ q ⟧c) (θ ← ([S]-env (S' ₛ))))88canθₖ-plug S' (just Signal.unknown ∷ sigs) C p q Canₖq⊆Canₖp Canₛq⊆Canₛp θ | yes p₁ | (yes p₂) = canθₖ-plug (suc S') sigs C p q Canₖq⊆Canₖp Canₛq⊆Canₛp (θ ← _)89canθₖ-plug S' (just Signal.unknown ∷ sigs) C p q Canₖq⊆Canₖp Canₛq⊆Canₛp θ | yes p₁ | (no ¬p)90 with sig-←-monoʳ (S' ₛ) ([S]-env (S' ₛ)) θ (sig-∈-single (S' ₛ) Signal.unknown)91... | S'∈θ←[S]env92 rewrite ((θ ← [S]-env-absent (S' ₛ)) ≡ (set-sig{S' ₛ} (θ ← [S]-env (S' ₛ)) S'∈θ←[S]env Signal.absent)93 ∋94 (θ ← [S]-env-absent (S' ₛ))95 ≡⟨ cong (θ ←_) (sym (←-single-overwrite-sig (S' ₛ) Signal.unknown96 ([S]-env-absent (S' ₛ)) ((sig-∈-single (S' ₛ) Signal.absent)))) ⟩97 (θ ← (([S]-env (S' ₛ)) ← [S]-env-absent (S' ₛ)))98 ≡⟨ ←-assoc θ ([S]-env (S' ₛ)) ([S]-env-absent (S' ₛ)) ⟩99 ((θ ← ([S]-env (S' ₛ))) ← ([S]-env-absent (S' ₛ)))100 ≡⟨ sym (sig-set=← (θ ← [S]-env (S' ₛ)) (S' ₛ) Signal.absent S'∈θ←[S]env) ⟩101 (set-sig{S' ₛ} (θ ← [S]-env (S' ₛ)) S'∈θ←[S]env Signal.absent) ∎)102 103 with canθₖ-set-sig-monotonic sigs (suc S') (C ⟦ q ⟧c) (S' ₛ) (θ ← [S]-env (S' ₛ))104 S'∈θ←[S]env Signal.absent105 (trans (sig-stats-←-right-irr' (S' ₛ) θ ([S]-env (S' ₛ)) (sig-∈-single (S' ₛ) Signal.unknown) S'∈θ←[S]env) (sig-stats-1map' (S' ₛ) Signal.unknown ((sig-∈-single (S' ₛ) Signal.unknown))))106 (n∉map-suc-n-+ S' (SigM.Dom' sigs))107... | Canabsq⊂Canunq108 = λ k x → (canθₖ-plug (suc S') sigs C p q Canₖq⊆Canₖp Canₛq⊆Canₛp (θ ← _)) k (Canabsq⊂Canunq k x)109canθₖ-plug S' (just Signal.unknown ∷ sigs) C p q Canₖq⊆Canₖp Canₛq⊆Canₛp θ | no ¬p | (yes p₁)110 = ⊥-elim (¬p ((canθₛ-plug (suc S') sigs C p q Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)) _ p₁ ))111canθₖ-plug S' (just Signal.unknown ∷ sigs) C p q Canₖq⊆Canₖp Canₛq⊆Canₛp θ | no ¬p | (no ¬p₁) = canθₖ-plug (suc S') sigs C p q Canₖq⊆Canₖp Canₛq⊆Canₛp (θ ← _)112 113canθₛ-plug S' [] C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ = canₛ-plug C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ114canθₛ-plug S' (nothing ∷ sigs) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ = canθₛ-plug (suc S') sigs C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ115canθₛ-plug S' (just Signal.present ∷ sigs) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ = canθₛ-plug (suc S') sigs C p q Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)116canθₛ-plug S' (just Signal.absent ∷ sigs) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ = canθₛ-plug (suc S') sigs C p q Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)117canθₛ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ118 with any (Nat._≟_ S') (Canθₛ sigs (suc S') (C ⟦ p ⟧c) (θ ← ([S]-env (S' ₛ))))119 | any (Nat._≟_ S') (Canθₛ sigs (suc S') (C ⟦ q ⟧c) (θ ← ([S]-env (S' ₛ))))120canθₛ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ | yes p₁ | (yes p₂) = canθₛ-plug (suc S') sigs C p q Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)121canθₛ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ | yes p₁ | (no ¬p)122 with sig-←-monoʳ (S' ₛ) ([S]-env (S' ₛ)) θ (sig-∈-single (S' ₛ) Signal.unknown)123... | S'∈θ←[S]env124 rewrite ((θ ← [S]-env-absent (S' ₛ)) ≡ (set-sig{S' ₛ} (θ ← [S]-env (S' ₛ)) S'∈θ←[S]env Signal.absent)125 ∋126 (θ ← [S]-env-absent (S' ₛ))127 ≡⟨ cong (θ ←_) (sym (←-single-overwrite-sig (S' ₛ) Signal.unknown128 ([S]-env-absent (S' ₛ)) ((sig-∈-single (S' ₛ) Signal.absent)))) ⟩129 (θ ← (([S]-env (S' ₛ)) ← [S]-env-absent (S' ₛ)))130 ≡⟨ ←-assoc θ ([S]-env (S' ₛ)) ([S]-env-absent (S' ₛ)) ⟩131 ((θ ← ([S]-env (S' ₛ))) ← ([S]-env-absent (S' ₛ)))132 ≡⟨ sym (sig-set=← (θ ← [S]-env (S' ₛ)) (S' ₛ) Signal.absent S'∈θ←[S]env) ⟩133 (set-sig{S' ₛ} (θ ← [S]-env (S' ₛ)) S'∈θ←[S]env Signal.absent) ∎)134 with canθₛ-set-sig-monotonic sigs (suc S') (C ⟦ q ⟧c) (S' ₛ) (θ ← [S]-env (S' ₛ))135 S'∈θ←[S]env Signal.absent136 (trans (sig-stats-←-right-irr' (S' ₛ) θ ([S]-env (S' ₛ)) (sig-∈-single (S' ₛ) Signal.unknown) S'∈θ←[S]env) (sig-stats-1map' (S' ₛ) Signal.unknown ((sig-∈-single (S' ₛ) Signal.unknown))))137 (n∉map-suc-n-+ S' (SigM.Dom' sigs))138... | Canabsq⊂Canunq139 = λ k x → (canθₛ-plug (suc S') sigs C p q Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)) k (Canabsq⊂Canunq k x)140 141canθₛ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ | no ¬p | (yes p₁)142 = ⊥-elim (¬p ((canθₛ-plug (suc S') sigs) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _) _ p₁))143canθₛ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ | no ¬p | (no ¬p₁) = canθₛ-plug (suc S') sigs C p q Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)144 145canθₛₕ-plug S' [] C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ = canₛₕ-plug C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ146canθₛₕ-plug S' (nothing ∷ sigs) C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ = canθₛₕ-plug (suc S') sigs C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ147canθₛₕ-plug S' (just Signal.present ∷ sigs) C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ = canθₛₕ-plug (suc S') sigs C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)148canθₛₕ-plug S' (just Signal.absent ∷ sigs) C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ = canθₛₕ-plug (suc S') sigs C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)149canθₛₕ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ150 with any (Nat._≟_ S') (Canθₛ sigs (suc S') (C ⟦ p ⟧c) (θ ← ([S]-env (S' ₛ))))151 | any (Nat._≟_ S') (Canθₛ sigs (suc S') (C ⟦ q ⟧c) (θ ← ([S]-env (S' ₛ))))152canθₛₕ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ | yes p₁ | (yes p₂) = canθₛₕ-plug (suc S') sigs C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)153canθₛₕ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp Canₛq⊆Canₛp θ | yes p₁ | (no ¬p)154 with sig-←-monoʳ (S' ₛ) ([S]-env (S' ₛ)) θ (sig-∈-single (S' ₛ) Signal.unknown)155... | S'∈θ←[S]env156 rewrite ((θ ← [S]-env-absent (S' ₛ)) ≡ (set-sig{S' ₛ} (θ ← [S]-env (S' ₛ)) S'∈θ←[S]env Signal.absent)157 ∋158 (θ ← [S]-env-absent (S' ₛ))159 ≡⟨ cong (θ ←_) (sym (←-single-overwrite-sig (S' ₛ) Signal.unknown160 ([S]-env-absent (S' ₛ)) ((sig-∈-single (S' ₛ) Signal.absent)))) ⟩161 (θ ← (([S]-env (S' ₛ)) ← [S]-env-absent (S' ₛ)))162 ≡⟨ ←-assoc θ ([S]-env (S' ₛ)) ([S]-env-absent (S' ₛ)) ⟩163 ((θ ← ([S]-env (S' ₛ))) ← ([S]-env-absent (S' ₛ)))164 ≡⟨ sym (sig-set=← (θ ← [S]-env (S' ₛ)) (S' ₛ) Signal.absent S'∈θ←[S]env) ⟩165 (set-sig{S' ₛ} (θ ← [S]-env (S' ₛ)) S'∈θ←[S]env Signal.absent) ∎)166 with canθₛₕ-set-sig-monotonic sigs (suc S') (C ⟦ q ⟧c) (S' ₛ) (θ ← [S]-env (S' ₛ))167 S'∈θ←[S]env Signal.absent168 (trans (sig-stats-←-right-irr' (S' ₛ) θ ([S]-env (S' ₛ)) (sig-∈-single (S' ₛ) Signal.unknown) S'∈θ←[S]env) (sig-stats-1map' (S' ₛ) Signal.unknown ((sig-∈-single (S' ₛ) Signal.unknown))))169 (n∉map-suc-n-+ S' (SigM.Dom' sigs))170... | Canabsq⊂Canunq171 = λ k x → (canθₛₕ-plug (suc S') sigs C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp Canₛq⊆Canₛp (θ ← _)) k (Canabsq⊂Canunq k x)172 173canθₛₕ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ | no ¬p | (yes p₁)174 = ⊥-elim (¬p (canθₛ-plug (suc S') sigs C p q Canₖq⊆Canₖp Canₛq⊆Canₛp (θ ← _) _ p₁))175canθₛₕ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ | no ¬p | (no ¬p₁) = canθₛₕ-plug (suc S') sigs C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)176 177 178canₖ-plug [] p q Canₖq⊆Canₖp _ = Canₖq⊆Canₖp179canₖ-plug (ceval (epar₁ q) ∷ C) p q₁ Canₖq⊆Canₖp ⊂s θ = map-mono² Code._⊔_ (canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ) (λ x y → y)180canₖ-plug (ceval (epar₂ p) ∷ C) p₁ q Canₖq⊆Canₖp ⊂s θ = map-mono²{xs = Canₖ p θ} Code._⊔_ (λ x y → y) (canₖ-plug C p₁ q Canₖq⊆Canₖp ⊂s θ)181canₖ-plug (ceval (eloopˢ q) ∷ C) p q₁ Canₖq⊆Canₖp ⊂s θ = canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ182canₖ-plug (ceval (eseq q) ∷ C) p q₁ Canₖq⊆Canₖp ⊂s θ with any (Code.nothin Code.≟_) (Canₖ (C ⟦ p ⟧c) θ) | any (Code.nothin Code.≟_) (Canₖ (C ⟦ q₁ ⟧c) θ)183... | yes 0∈CanC⟦p⟧ | yes 0∈CanC⟦q⟧ = codesub++both ((codesub- Code.nothin (canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ))) (λ x y → y)184... | yes 0∈CanC⟦p⟧ | no 0∉CanC⟦q⟧ = λ k x → ++ˡ (set-remove-not-removed{Code.nothin}{k} (λ {refl → 0∉CanC⟦q⟧ x}) (canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ _ x))185... | no 0∉CanC⟦p⟧ | yes 0∈CanC⟦q⟧ = ⊥-elim (0∉CanC⟦p⟧ (canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ _ 0∈CanC⟦q⟧))186... | no 0∉CanC⟦p⟧ | no 0∉CanC⟦q⟧ = canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ187canₖ-plug (ceval (esuspend S) ∷ C) p q Canₖq⊆Canₖp ⊂s = canₖ-plug C p q Canₖq⊆Canₖp ⊂s188canₖ-plug (ceval etrap ∷ C) p q Canₖq⊆Canₖp ⊂s = λ θ → map-mono Code.↓* (canₖ-plug C p q Canₖq⊆Canₖp ⊂s θ)189canₖ-plug (csignl S ∷ C) p q Canₖq⊆Canₖp ⊂s θ = canθₖ-plug 0 (sig ([S]-env S)) C p q Canₖq⊆Canₖp ⊂s θ190canₖ-plug (cpresent₁ S q ∷ C) p q₁ Canₖq⊆Canₖp ⊂s θ with Sig∈ S θ191... | no S∉Domθ = codesub++both (canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ) (λ x y → y)192... | yes S∈Domθ with (Signal.present ≟ₛₜ (sig-stats{S} θ S∈Domθ))193... | yes _ = canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ194... | no _ with (Signal.absent ≟ₛₜ (sig-stats{S} θ S∈Domθ))195... | yes _ = λ k z → z196... | no _ = codesub++both (canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ) (λ x y → y)197canₖ-plug (cpresent₂ S p₁ ∷ C) p q Canₖq⊆Canₖp ⊂s θ with Sig∈ S θ198... | no S∉Domθ = codesub++both{a = Canₖ p₁ θ} (λ x y → y) (canₖ-plug C p q Canₖq⊆Canₖp ⊂s θ)199... | yes S∈Domθ with (Signal.present ≟ₛₜ (sig-stats{S} θ S∈Domθ))200... | yes _ = λ x y → y201... | no _ with (Signal.absent ≟ₛₜ (sig-stats{S} θ S∈Domθ))202... | yes _ = canₖ-plug C p q Canₖq⊆Canₖp ⊂s θ203... | no _ = codesub++both{a = Canₖ p₁ θ} (λ x y → y) (canₖ-plug C p q Canₖq⊆Canₖp ⊂s θ)204canₖ-plug (cloop ∷ C) p q Canₖq⊆Canₖp ⊂s = (canₖ-plug C p q Canₖq⊆Canₖp ⊂s)205canₖ-plug (cloopˢ₂ p ∷ C) p₁ q Canₖq⊆Canₖp ⊂s θ = λ k z → z 206canₖ-plug (cseq₂ p ∷ C) p₁ q Canₖq⊆Canₖp ⊂s θ with any (Code.nothin Code.≟_) (Canₖ p θ)207... | yes 0∈Canp = codesub++both{a = set-remove (Canₖ p θ) Code.nothin } (λ x y → y) (canₖ-plug C p₁ q Canₖq⊆Canₖp ⊂s θ)208... | no 0∉Canp = λ x y → y209canₖ-plug (cshared s e ∷ C) p q Canₖq⊆Canₖp ⊂s = (canₖ-plug C p q Canₖq⊆Canₖp ⊂s)210canₖ-plug (cvar x e ∷ C) p q Canₖq⊆Canₖp ⊂s = (canₖ-plug C p q Canₖq⊆Canₖp ⊂s)211canₖ-plug (cif₁ x q ∷ C) p q₁ Canₖq⊆Canₖp ⊂s θ = codesub++both (canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ) (λ x y → y)212canₖ-plug (cif₂ x p ∷ C) p₁ q Canₖq⊆Canₖp ⊂s θ = codesub++both{a = Canₖ p θ} (λ x y → y) (canₖ-plug C p₁ q Canₖq⊆Canₖp ⊂s θ)213canₖ-plug (cenv θ₁ A ∷ C) p q Canₖq⊆Canₖp ⊂s θ = canθₖ-plug 0 (sig θ₁) C p q Canₖq⊆Canₖp ⊂s θ214 215canₛ-plug [] p q Canₛq⊆Canₛp Canₖq⊆Canₖp = Canₛq⊆Canₛp216canₛ-plug (ceval (epar₁ q) ∷ C) p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ = ∪¹-respect-⊆¹-left (canₛ-plug C p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ)217canₛ-plug (ceval (epar₂ p) ∷ C) p₁ q Canₛq⊆Canₛp Canₖq⊆Canₖp θ = ∪¹-respect-⊆¹-right (Canₛ p θ) (canₛ-plug C p₁ q Canₛq⊆Canₛp Canₖq⊆Canₖp θ)218canₛ-plug (ceval (eloopˢ q) ∷ C) p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ = canₛ-plug C p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ219canₛ-plug (ceval (eseq q) ∷ C) p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ with any (Code.nothin Code.≟_) (Canₖ (C ⟦ p ⟧c) θ) | any (Code.nothin Code.≟_) (Canₖ (C ⟦ q₁ ⟧c) θ)220... | yes 0∈CanC⟦p⟧ | yes 0∈CanC⟦q⟧ = ∪¹-respect-⊆¹-left (canₛ-plug C p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ)221... | yes 0∈CanC⟦p⟧ | no 0∉CanC⟦q⟧ = λ S x → (++ˡ (canₛ-plug C p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ S x))222... | no 0∉CanC⟦p⟧ | yes 0∈CanC⟦q⟧ = ⊥-elim (0∉CanC⟦p⟧ (canₖ-plug C p q₁ Canₖq⊆Canₖp Canₛq⊆Canₛp θ _ 0∈CanC⟦q⟧))223... | no 0∉CanC⟦p⟧ | no 0∉CanC⟦q⟧ = (canₛ-plug C p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ)224 225-- set-subtract-merge : ∀ {xs ys z} → z ∈ set-subtract xs ys → (z ∈ xs) × (z ∉ ys)226 227canₛ-plug (ceval (esuspend S) ∷ C) p q Canₛq⊆Canₛp Canₖq⊆Canₖp = (canₛ-plug C p q Canₛq⊆Canₛp Canₖq⊆Canₖp)228canₛ-plug (ceval etrap ∷ C) p q Canₛq⊆Canₛp Canₖq⊆Canₖp = (canₛ-plug C p q Canₛq⊆Canₛp Canₖq⊆Canₖp)229canₛ-plug (csignl (S ₛ) ∷ C) p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ S' S'∈CanC⟦q⟧230 = NSet.set-remove-not-removed ((¬ S ≡ S') ∋ NSet.set-remove-not-eq{S'}{S}{Canθₛ (sig ([S]-env (S ₛ))) 0 (C ⟦ q ⟧c) θ} S'∈CanC⟦q⟧)231 ((canθₛ-plug 0 (sig ([S]-env (S ₛ))) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ) S' ( (NSet.set-remove-mono-∈ S S'∈CanC⟦q⟧) ))232 233 234canₛ-plug (cpresent₁ S q ∷ C) p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ with Sig∈ S θ235... | no S∉Domθ = ∪¹-respect-⊆¹-left (canₛ-plug C p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ)236... | yes S∈Domθ with (Signal.present ≟ₛₜ (sig-stats{S} θ S∈Domθ))237... | yes _ = (canₛ-plug C p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ)238... | no _ with (Signal.absent ≟ₛₜ (sig-stats{S} θ S∈Domθ))239... | yes _ = λ k z → z240... | no _ = ∪¹-respect-⊆¹-left (canₛ-plug C p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ)241canₛ-plug (cpresent₂ S p₁ ∷ C) p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ with Sig∈ S θ242... | no S∉Domθ = ∪¹-respect-⊆¹-right (Canₛ p₁ θ) (canₛ-plug C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ)243... | yes S∈Domθ with (Signal.present ≟ₛₜ (sig-stats{S} θ S∈Domθ))244... | yes _ = λ x y → y245... | no _ with (Signal.absent ≟ₛₜ (sig-stats{S} θ S∈Domθ))246... | yes _ = (canₛ-plug C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ)247... | no _ = ∪¹-respect-⊆¹-right (Canₛ p₁ θ) (canₛ-plug C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ)248canₛ-plug (cloop ∷ C) p q Canₛq⊆Canₛp Canₖq⊆Canₖp = (canₛ-plug C p q Canₛq⊆Canₛp Canₖq⊆Canₖp)249canₛ-plug (cloopˢ₂ p ∷ C) p₁ q Canₛq⊆Canₛp Canₖq⊆Canₖp θ = λ x z → z250canₛ-plug (cseq₂ p ∷ C) p₁ q Canₛq⊆Canₛp Canₖq⊆Canₖp θ with any (Code.nothin Code.≟_) (Canₖ p θ)251... | yes 0∈Canp = ∪¹-respect-⊆¹-right (Canₛ p θ) (canₛ-plug C p₁ q Canₛq⊆Canₛp Canₖq⊆Canₖp θ)252... | no 0∉Canp = λ x y → y253canₛ-plug (cshared s e ∷ C) p q Canₛq⊆Canₛp Canₖq⊆Canₖp = (canₛ-plug C p q Canₛq⊆Canₛp Canₖq⊆Canₖp)254canₛ-plug (cvar x e ∷ C) p q Canₛq⊆Canₛp Canₖq⊆Canₖp = (canₛ-plug C p q Canₛq⊆Canₛp Canₖq⊆Canₖp)255canₛ-plug (cif₁ x q ∷ C) p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ = ∪¹-respect-⊆¹-left (canₛ-plug C p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ)256canₛ-plug (cif₂ x p ∷ C) p₁ q Canₛq⊆Canₛp Canₖq⊆Canₖp θ = ∪¹-respect-⊆¹-right (Canₛ p θ) (canₛ-plug C p₁ q Canₛq⊆Canₛp Canₖq⊆Canₖp θ)257canₛ-plug (cenv θ₁ A ∷ C) p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ = ⊆¹-respect-|¹ (fst $ Dom θ₁) (canθₛ-plug 0 (sig θ₁) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ)258 259canₛₕ-plug [] p q Canₛₕq⊆Canₛₕp Canₖₕq⊆Canₖₕp ⊂S = Canₛₕq⊆Canₛₕp260canₛₕ-plug (ceval (epar₁ q) ∷ C) p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ = ∪¹-respect-⊆¹-left (canₛₕ-plug C p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)261canₛₕ-plug (ceval (epar₂ p) ∷ C) p₁ q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ = ∪¹-respect-⊆¹-right (Canₛₕ p θ) (canₛₕ-plug C p₁ q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)262canₛₕ-plug (ceval (eloopˢ q) ∷ C) p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ = canₛₕ-plug C p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ263canₛₕ-plug (ceval (eseq q) ∷ C) p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ with any (Code.nothin Code.≟_) (Canₖ (C ⟦ p ⟧c) θ) | any (Code.nothin Code.≟_) (Canₖ (C ⟦ q₁ ⟧c) θ)264... | yes 0∈CanC⟦p⟧ | yes 0∈CanC⟦q⟧ = ∪¹-respect-⊆¹-left (canₛₕ-plug C p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)265... | yes 0∈CanC⟦p⟧ | no 0∉CanC⟦q⟧ = λ S x → (++ˡ (canₛₕ-plug C p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ S x))266... | no 0∉CanC⟦p⟧ | yes 0∈CanC⟦q⟧ = ⊥-elim (0∉CanC⟦p⟧ (canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂S θ _ 0∈CanC⟦q⟧))267... | no 0∉CanC⟦p⟧ | no 0∉CanC⟦q⟧ = (canₛₕ-plug C p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)268 269canₛₕ-plug (ceval (esuspend S) ∷ C) p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S = (canₛₕ-plug C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S)270canₛₕ-plug (ceval etrap ∷ C) p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S = (canₛₕ-plug C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S)271canₛₕ-plug (csignl S ∷ C) p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ = canθₛₕ-plug 0 (sig ([S]-env S)) C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ272canₛₕ-plug (cpresent₁ S q ∷ C) p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ with Sig∈ S θ273... | no S∉Domθ = ∪¹-respect-⊆¹-left (canₛₕ-plug C p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)274... | yes S∈Domθ with (Signal.present ≟ₛₜ (sig-stats{S} θ S∈Domθ))275... | yes _ = (canₛₕ-plug C p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)276... | no _ with (Signal.absent ≟ₛₜ (sig-stats{S} θ S∈Domθ))277... | yes _ = λ k z → z278... | no _ = ∪¹-respect-⊆¹-left (canₛₕ-plug C p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)279canₛₕ-plug (cpresent₂ S p₁ ∷ C) p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ with Sig∈ S θ280... | no S∉Domθ = ∪¹-respect-⊆¹-right (Canₛₕ p₁ θ) (canₛₕ-plug C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)281... | yes S∈Domθ with (Signal.present ≟ₛₜ (sig-stats{S} θ S∈Domθ))282... | yes _ = λ x y → y283... | no _ with (Signal.absent ≟ₛₜ (sig-stats{S} θ S∈Domθ))284... | yes _ = (canₛₕ-plug C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)285... | no _ = ∪¹-respect-⊆¹-right (Canₛₕ p₁ θ) (canₛₕ-plug C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)286canₛₕ-plug (cloop ∷ C) p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S = (canₛₕ-plug C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S)287canₛₕ-plug (cloopˢ₂ p ∷ C) p₁ q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ = λ x z → z288canₛₕ-plug (cseq₂ p ∷ C) p₁ q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ with any (Code.nothin Code.≟_) (Canₖ p θ)289... | yes 0∈Canp = ∪¹-respect-⊆¹-right (Canₛₕ p θ) (canₛₕ-plug C p₁ q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)290... | no 0∉Canp = λ x y → y291canₛₕ-plug (cshared (s ₛₕ) e ∷ C) p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ s' s'∈CanC⟦q⟧292 = NSet.set-remove-not-removed ((¬ s ≡ s') ∋ NSet.set-remove-not-eq{s'}{s}{Canₛₕ (C ⟦ q ⟧c) θ} s'∈CanC⟦q⟧) (canₛₕ-plug C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ s' (NSet.set-remove-mono-∈ s s'∈CanC⟦q⟧))293canₛₕ-plug (cvar x e ∷ C) p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S = (canₛₕ-plug C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S)294canₛₕ-plug (cif₁ x q ∷ C) p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ = ∪¹-respect-⊆¹-left (canₛₕ-plug C p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)295canₛₕ-plug (cif₂ x p ∷ C) p₁ q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ = ∪¹-respect-⊆¹-right (Canₛₕ p θ) (canₛₕ-plug C p₁ q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)296canₛₕ-plug (cenv θ₁ A ∷ C) p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ = ⊆¹-respect-|¹ (snd $ Dom θ₁) (canθₛₕ-plug 0 (sig θ₁) C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)297 298canθₖ-plugE : ∀ S' sigs → ∀ E p q299 → (Canₖq⊆Canₖp : ∀ θ k → k ∈ (Canₖ q θ) → k ∈ (Canₖ p θ))300 → (Canₛq⊆Canₛp : ∀ θ S → S ∈ (Canₛ q θ) → S ∈ (Canₛ p θ))301 → (∀ θ k → k ∈ (Canθₖ sigs S' (E ⟦ q ⟧e) θ) → k ∈ (Canθₖ sigs S' (E ⟦ p ⟧e) θ))302canθₖ-plugE S' sigs E p q303 with canθₖ-plug S' sigs (Data.List.map ceval E) p q304... | r rewrite unplugc (⟦⟧e-to-⟦⟧c (Erefl{E}{q}))305 | unplugc (⟦⟧e-to-⟦⟧c (Erefl{E}{p}))306 = r307 308canθₛ-plugE : ∀ S' sigs → ∀ E p q309 → (Canₛq⊆Canₛp : ∀ θ S → S ∈ (Canₛ q θ) → S ∈ (Canₛ p θ))310 → (Canₖq⊆Canₖp : ∀ θ k → k ∈ (Canₖ q θ) → k ∈ (Canₖ p θ))311 → (∀ θ k → k ∈ (Canθₛ sigs S' (E ⟦ q ⟧e) θ) → k ∈ (Canθₛ sigs S' (E ⟦ p ⟧e) θ))312canθₛ-plugE S' sigs E p q313 with canθₛ-plug S' sigs (Data.List.map ceval E) p q314... | r rewrite unplugc (⟦⟧e-to-⟦⟧c (Erefl{E}{q}))315 | unplugc (⟦⟧e-to-⟦⟧c (Erefl{E}{p}))316 = r317 318 319canθₛₕ-plugE : ∀ S' sigs → ∀ E p q320 → (Canₛₕq⊆Canₛₕp : ∀ θ → (Canₛₕ q θ) ⊆¹ (Canₛₕ p θ))321 → (Canₛq⊆Canₛp : ∀ θ k → k ∈ (Canₖ q θ) → k ∈ (Canₖ p θ))322 → (Canₖq⊆Canₖp : ∀ θ S → S ∈ (Canₛ q θ) → S ∈ (Canₛ p θ))323 → (∀ θ k → k ∈ (Canθₛₕ sigs S' (E ⟦ q ⟧e) θ) → k ∈ (Canθₛₕ sigs S' (E ⟦ p ⟧e) θ))324canθₛₕ-plugE S' sigs E p q325 with canθₛₕ-plug S' sigs (Data.List.map ceval E) p q326... | r rewrite unplugc (⟦⟧e-to-⟦⟧c (Erefl{E}{q}))327 | unplugc (⟦⟧e-to-⟦⟧c (Erefl{E}{p}))328 = r329",12421,True,3008.0102386974067,median330"------------------------------------------------------------------------331-- A variant of the propositional truncation operator with an erased332-- truncation constructor333------------------------------------------------------------------------334 335-- Partly following the HoTT book, but adapted for erasure.336 337{-# OPTIONS --erased-cubical --safe #-}338 339-- The module is parametrised by a notion of equality. The higher340-- constructor of the HIT defining the propositional truncation341-- operator uses path equality, but the supplied notion of equality is342-- used for many other things.343 344import Equality.Path as P345 346module H-level.Truncation.Propositional.Erased347 {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where348 349open P.Derived-definitions-and-properties eq hiding (elim)350 351open import Prelude as P352open import Logical-equivalence using (_⇔_)353 354open import Bijection equality-with-J as Bijection using (_↔_)355import Colimit.Sequential.Very-erased eq as C356open import Embedding equality-with-J as Emb using (Is-embedding)357open import Equality.Decidable-UIP equality-with-J358open import Equality.Path.Isomorphisms eq359open import Equivalence equality-with-J as Eq360 using (_≃_; Is-equivalence)361open import Equivalence.Erased equality-with-J as EEq362 using (_≃ᴱ_; Is-equivalenceᴱ)363open import Equivalence.Erased.Contractible-preimages equality-with-J364 as ECP using (Contractibleᴱ; _⁻¹ᴱ_)365open import Equivalence-relation equality-with-J366open import Erased.Cubical eq as Er367 using (Erased; [_]; erased; Very-stableᴱ-≡; Erased-singleton)368open import Function-universe equality-with-J as F hiding (id; _∘_)369open import H-level equality-with-J as H-level370open import H-level.Closure equality-with-J371open import H-level.Truncation.Propositional.One-step eq as O372 using (∥_∥¹-out-^)373import H-level.Truncation.Propositional.Non-recursive.Erased eq as N374open import Monad equality-with-J375open import Preimage equality-with-J using (_⁻¹_)376open import Surjection equality-with-J as S377 using (_↠_; Split-surjective)378 379private380 variable381 a b ℓ p r : Level382 A A₁ A₂ B B₁ B₂ C : Type a383 P Q : A → Type p384 R : A → A → Type r385 f g k x y : A386 387------------------------------------------------------------------------388-- The type former389 390-- A propositional truncation operator with an erased higher391-- constructor.392 393data ∥_∥ᴱ (A : Type a) : Type a where394 ∣_∣ : A → ∥ A ∥ᴱ395 @0 truncation-is-propositionᴾ : P.Is-proposition ∥ A ∥ᴱ396 397-- The truncation produces propositions (in erased contexts).398 399@0 truncation-is-proposition : Is-proposition ∥ A ∥ᴱ400truncation-is-proposition =401 _↔_.from (H-level↔H-level 1) truncation-is-propositionᴾ402 403------------------------------------------------------------------------404-- Eliminators405 406-- A dependent eliminator, expressed using paths.407 408record Elimᴾ′ {A : Type a} (P : ∥ A ∥ᴱ → Type p) : Type (a ⊔ p) where409 no-eta-equality410 field411 ∣∣ʳ : (x : A) → P ∣ x ∣412 413 @0 truncation-is-propositionʳ :414 (p : P x) (q : P y) →415 P.[ (λ i → P (truncation-is-propositionᴾ x y i)) ] p ≡ q416 417open Elimᴾ′ public418 419elimᴾ′ : Elimᴾ′ P → (x : ∥ A ∥ᴱ) → P x420elimᴾ′ {A = A} {P = P} e = helper421 where422 module E = Elimᴾ′ e423 424 helper : (x : ∥ A ∥ᴱ) → P x425 helper ∣ x ∣ = E.∣∣ʳ x426 helper (truncation-is-propositionᴾ x y i) =427 E.truncation-is-propositionʳ (helper x) (helper y) i428 429-- A possibly more useful dependent eliminator, expressed using paths.430 431record Elimᴾ {A : Type a} (P : ∥ A ∥ᴱ → Type p) : Type (a ⊔ p) where432 no-eta-equality433 field434 ∣∣ʳ : (x : A) → P ∣ x ∣435 436 @0 truncation-is-propositionʳ :437 (x : ∥ A ∥ᴱ) → P.Is-proposition (P x)438 439open Elimᴾ public440 441elimᴾ : Elimᴾ P → (x : ∥ A ∥ᴱ) → P x442elimᴾ e = elimᴾ′ λ where443 .∣∣ʳ → E.∣∣ʳ444 .truncation-is-propositionʳ _ _ →445 P.heterogeneous-irrelevance E.truncation-is-propositionʳ446 where447 module E = Elimᴾ e448 449-- A non-dependent eliminator, expressed using paths.450 451record Recᴾ (A : Type a) (B : Type b) : Type (a ⊔ b) where452 no-eta-equality453 field454 ∣∣ʳ : A → B455 @0 truncation-is-propositionʳ : P.Is-proposition B456 457open Recᴾ public458 459recᴾ : Recᴾ A B → ∥ A ∥ᴱ → B460recᴾ r = elimᴾ λ where461 .∣∣ʳ → R.∣∣ʳ462 .truncation-is-propositionʳ _ → R.truncation-is-propositionʳ463 where464 module R = Recᴾ r465 466-- A dependently typed eliminator.467 468record Elim {A : Type a} (P : ∥ A ∥ᴱ → Type p) : Type (a ⊔ p) where469 no-eta-equality470 field471 ∣∣ʳ : (x : A) → P ∣ x ∣472 473 @0 truncation-is-propositionʳ :474 (x : ∥ A ∥ᴱ) → Is-proposition (P x)475 476open Elim public477 478elim : Elim P → (x : ∥ A ∥ᴱ) → P x479elim e = elimᴾ λ where480 .∣∣ʳ → E.∣∣ʳ481 .truncation-is-propositionʳ →482 _↔_.to (H-level↔H-level 1) ∘ E.truncation-is-propositionʳ483 where484 module E = Elim e485 486-- Primitive ""recursion"".487 488record Rec (A : Type a) (B : Type b) : Type (a ⊔ b) where489 no-eta-equality490 field491 ∣∣ʳ : A → B492 @0 truncation-is-propositionʳ : Is-proposition B493 494open Rec public495 496rec : Rec A B → ∥ A ∥ᴱ → B497rec r = recᴾ λ where498 .∣∣ʳ → R.∣∣ʳ499 .truncation-is-propositionʳ →500 _↔_.to (H-level↔H-level 1) R.truncation-is-propositionʳ501 where502 module R = Rec r503 504------------------------------------------------------------------------505-- Conversion functions506 507-- ∥_∥ᴱ is pointwise equivalent to N.∥_∥ᴱ.508 509∥∥ᴱ≃∥∥ᴱ : ∥ A ∥ᴱ ≃ N.∥ A ∥ᴱ510∥∥ᴱ≃∥∥ᴱ = Eq.↔→≃511 (rec λ where512 .∣∣ʳ → N.∣_∣513 .truncation-is-propositionʳ → N.∥∥ᴱ-proposition)514 (N.elim λ where515 .N.∣∣ʳ → ∣_∣516 .N.is-propositionʳ _ → truncation-is-proposition)517 (N.elim λ where518 .N.∣∣ʳ _ → refl _519 .N.is-propositionʳ _ → mono₁ 1 N.∥∥ᴱ-proposition)520 (elim λ where521 .∣∣ʳ _ → refl _522 .truncation-is-propositionʳ _ → mono₁ 1 truncation-is-proposition)523 524------------------------------------------------------------------------525-- Some preservation lemmas and related results526 527-- A map function.528 529∥∥ᴱ-map : (A → B) → ∥ A ∥ᴱ → ∥ B ∥ᴱ530∥∥ᴱ-map f = rec λ where531 .∣∣ʳ → ∣_∣ ∘ f532 .truncation-is-propositionʳ → truncation-is-proposition533 534mutual535 536 -- If A and B are logically equivalent, then there is an equivalence537 -- with erased proofs between ∥ A ∥ᴱ and ∥ B ∥ᴱ.538 539 ∥∥ᴱ-cong-⇔ : A ⇔ B → ∥ A ∥ᴱ ≃ᴱ ∥ B ∥ᴱ540 ∥∥ᴱ-cong-⇔ A⇔B = ∥∥ᴱ-cong-⇔′ (∣_∣ ∘ _⇔_.to A⇔B) (∣_∣ ∘ _⇔_.from A⇔B)541 542 -- A variant of the previous result.543 544 ∥∥ᴱ-cong-⇔′ : (A → ∥ B ∥ᴱ) → (B → ∥ A ∥ᴱ) → ∥ A ∥ᴱ ≃ᴱ ∥ B ∥ᴱ545 ∥∥ᴱ-cong-⇔′ A→∥B∥ B→∥A∥ = EEq.⇔→≃ᴱ546 truncation-is-proposition547 truncation-is-proposition548 (rec λ where549 .∣∣ʳ → A→∥B∥550 .truncation-is-propositionʳ → truncation-is-proposition)551 (rec λ where552 .∣∣ʳ → B→∥A∥553 .truncation-is-propositionʳ → truncation-is-proposition)554 555-- If there is a split surjection from A to B, then there is a split556-- surjection from ∥ A ∥ᴱ to ∥ B ∥ᴱ.557 558∥∥ᴱ-cong-↠ : A ↠ B → ∥ A ∥ᴱ ↠ ∥ B ∥ᴱ559∥∥ᴱ-cong-↠ A↠B = record560 { logical-equivalence = record561 { to = ∥∥ᴱ-map (_↠_.to A↠B)562 ; from = ∥∥ᴱ-map (_↠_.from A↠B)563 }564 ; right-inverse-of = elim λ where565 .∣∣ʳ x →566 ∣ _↠_.to A↠B (_↠_.from A↠B x) ∣ ≡⟨ cong ∣_∣ (_↠_.right-inverse-of A↠B x) ⟩∎567 ∣ x ∣ ∎568 .truncation-is-propositionʳ _ →569 mono₁ 1 truncation-is-proposition570 }571 572private573 574 ∥∥ᴱ-cong-↔ : A ↔ B → ∥ A ∥ᴱ ↔ ∥ B ∥ᴱ575 ∥∥ᴱ-cong-↔ A↔B = record576 { surjection = ∥∥ᴱ-cong-↠ (_↔_.surjection A↔B)577 ; left-inverse-of = elim λ where578 .∣∣ʳ x →579 ∣ _↔_.from A↔B (_↔_.to A↔B x) ∣ ≡⟨ cong ∣_∣ (_↔_.left-inverse-of A↔B x) ⟩∎580 ∣ x ∣ ∎581 .truncation-is-propositionʳ _ →582 mono₁ 1 truncation-is-proposition583 }584 585-- The truncation operator preserves ""symmetric"" functions.586 587∥∥ᴱ-cong : A ↝[ ⌊ k ⌋-sym ] B → ∥ A ∥ᴱ ↝[ ⌊ k ⌋-sym ] ∥ B ∥ᴱ588∥∥ᴱ-cong {k = logical-equivalence} = _≃ᴱ_.logical-equivalence ∘589 ∥∥ᴱ-cong-⇔590∥∥ᴱ-cong {k = bijection} = ∥∥ᴱ-cong-↔591∥∥ᴱ-cong {k = equivalence} = from-isomorphism ∘ ∥∥ᴱ-cong-↔ ∘592 from-isomorphism593∥∥ᴱ-cong {k = equivalenceᴱ} = ∥∥ᴱ-cong-⇔ ∘594 _≃ᴱ_.logical-equivalence595 596------------------------------------------------------------------------597-- Some bijections/erased equivalences598 599-- If the underlying type is a proposition, then truncations of the600-- type are isomorphic to the type itself.601 602∥∥ᴱ↔ : @0 Is-proposition A → ∥ A ∥ᴱ ↔ A603∥∥ᴱ↔ A-prop = record604 { surjection = record605 { logical-equivalence = record606 { to = rec λ where607 .∣∣ʳ → id608 .truncation-is-propositionʳ → A-prop609 ; from = ∣_∣610 }611 ; right-inverse-of = λ _ → refl _612 }613 ; left-inverse-of = elim λ where614 .∣∣ʳ _ → refl _615 .truncation-is-propositionʳ _ → mono₁ 1 truncation-is-proposition616 }617 618-- If A is merely inhabited, then the truncation of A is equivalent619-- (with erased proofs) to the unit type.620 621inhabited⇒∥∥ᴱ≃ᴱ⊤ : ∥ A ∥ᴱ → ∥ A ∥ᴱ ≃ᴱ ⊤622inhabited⇒∥∥ᴱ≃ᴱ⊤ ∥a∥ =623 EEq.inhabited→Is-proposition→≃ᴱ⊤ ∥a∥ truncation-is-proposition624 625-- If A is not inhabited, then the propositional truncation of A is626-- isomorphic to the empty type.627 628not-inhabited⇒∥∥ᴱ↔⊥ : ¬ A → ∥ A ∥ᴱ ↔ ⊥ {ℓ = ℓ}629not-inhabited⇒∥∥ᴱ↔⊥ {A = A} =630 ¬ A ↝⟨ (λ ¬a → rec λ where631 .∣∣ʳ → ¬a632 .truncation-is-propositionʳ → ⊥-propositional) ⟩633 ¬ ∥ A ∥ᴱ ↝⟨ inverse ∘ Bijection.⊥↔uninhabited ⟩□634 ∥ A ∥ᴱ ↔ ⊥ □635 636-- The negation of the truncation of A is isomorphic to the negation637-- of A.638 639¬∥∥ᴱ↔¬ : ¬ ∥ A ∥ᴱ ↔ ¬ A640¬∥∥ᴱ↔¬ {A = A} = record641 { surjection = record642 { logical-equivalence = record643 { to = λ f → f ∘ ∣_∣644 ; from = λ ¬A → rec λ where645 .∣∣ʳ → ¬A646 .truncation-is-propositionʳ → ⊥-propositional647 }648 ; right-inverse-of = λ _ → ¬-propositional ext _ _649 }650 ; left-inverse-of = λ _ → ¬-propositional ext _ _651 }652 653-- A form of idempotence for binary sums.654 655idempotent : ∥ A ⊎ A ∥ᴱ ≃ᴱ ∥ A ∥ᴱ656idempotent = ∥∥ᴱ-cong-⇔ (record { to = P.[ id , id ]; from = inj₁ })657 658------------------------------------------------------------------------659-- The universal property, and some related results660 661mutual662 663 -- The propositional truncation operator's universal property.664 --665 -- See also Quotient.Erased.Σ→Erased-Constant≃∥∥ᴱ→.666 667 universal-property :668 @0 Is-proposition B →669 (∥ A ∥ᴱ → B) ≃ (A → B)670 universal-property B-prop = universal-property-Π (λ _ → B-prop)671 672 -- A generalisation of the universal property.673 674 universal-property-Π :675 @0 (∀ x → Is-proposition (P x)) →676 ((x : ∥ A ∥ᴱ) → P x) ≃ ((x : A) → P ∣ x ∣)677 universal-property-Π {A = A} {P = P} P-prop =678 ((x : ∥ A ∥ᴱ) → P x) ↝⟨ Eq.↔⇒≃ (record679 { surjection = record680 { logical-equivalence = record681 { to = λ f → ∣ f ∘ ∣_∣ ∣682 ; from = rec λ where683 .∣∣ʳ f → elim λ where684 .∣∣ʳ → f685 .truncation-is-propositionʳ → P-prop686 .truncation-is-propositionʳ →687 Π-closure ext 1 λ _ → P-prop _688 }689 ; right-inverse-of = elim λ where690 .∣∣ʳ _ → refl _691 .truncation-is-propositionʳ _ →692 mono₁ 1 truncation-is-proposition693 }694 ; left-inverse-of = λ f → ⟨ext⟩ $ elim λ where695 .∣∣ʳ _ → refl _696 .truncation-is-propositionʳ _ →697 mono₁ 1 (P-prop _)698 }) ⟩699 ∥ ((x : A) → P ∣ x ∣) ∥ᴱ ↔⟨ ∥∥ᴱ↔ (Π-closure ext 1 λ _ → P-prop _) ⟩□700 ((x : A) → P ∣ x ∣) □701 702-- The universal property computes in the ""right"" way.703 704_ :705 (@0 B-prop : Is-proposition B)706 (f : ∥ A ∥ᴱ → B) →707 _≃_.to (universal-property B-prop) f ≡ f ∘ ∣_∣708_ = λ _ _ → refl _709 710_ :711 (@0 B-prop : Is-proposition B)712 (f : A → B) (x : A) →713 _≃_.from (universal-property B-prop) f ∣ x ∣ ≡ f x714_ = λ _ _ _ → refl _715 716-- Functions from ∥ A ∥ᴱ can be expressed as functions from A along717-- with some erased data.718 719∥∥ᴱ→≃ :720 (∥ A ∥ᴱ → B)721 ≃722 (∃ λ (f : A → B) →723 Erased (∃ λ (g : ∀ n → ∥ A ∥¹-out-^ (suc n) → B) →724 (∀ x → g zero O.∣ x ∣ ≡ f x) ×725 (∀ n x → g (suc n) O.∣ x ∣ ≡ g n x)))726∥∥ᴱ→≃ {A = A} {B = B} =727 (∥ A ∥ᴱ → B) ↝⟨ →-cong ext ∥∥ᴱ≃∥∥ᴱ F.id ⟩728 729 (N.∥ A ∥ᴱ → B) ↝⟨ C.universal-property ⟩□730 731 (∃ λ (f : A → B) →732 Erased (∃ λ (g : ∀ n → ∥ A ∥¹-out-^ (suc n) → B) →733 (∀ x → g zero O.∣ x ∣ ≡ f x) ×734 (∀ n x → g (suc n) O.∣ x ∣ ≡ g n x))) □735 736-- A function of type (x : ∥ A ∥ᴱ) → P x, along with an erased proof737-- showing that the function is equal to some erased function, is738-- equivalent to a function of type (x : A) → P ∣ x ∣, along with an739-- erased equality proof.740 741Σ-Π-∥∥ᴱ-Erased-≡-≃ :742 {@0 g : (x : ∥ A ∥ᴱ) → P x} →743 (∃ λ (f : (x : ∥ A ∥ᴱ) → P x) → Erased (f ≡ g)) ≃744 (∃ λ (f : (x : A) → P ∣ x ∣) → Erased (f ≡ g ∘ ∣_∣))745Σ-Π-∥∥ᴱ-Erased-≡-≃ {A = A} {P = P} {g = g} =746 (∃ λ (f : (x : ∥ A ∥ᴱ) → P x) → Erased (f ≡ g)) ↝⟨ (Σ-cong lemma λ _ → Er.Erased-cong (inverse $ Eq.≃-≡ lemma)) ⟩747 748 (∃ λ (f : (x : N.∥ A ∥ᴱ) → P (_≃_.from ∥∥ᴱ≃∥∥ᴱ x)) →749 Erased (f ≡ g ∘ _≃_.from ∥∥ᴱ≃∥∥ᴱ)) ↝⟨ N.Σ-Π-∥∥ᴱ-Erased-≡-≃ ⟩□750 751 (∃ λ (f : (x : A) → P ∣ x ∣) → Erased (f ≡ g ∘ ∣_∣)) □752 where753 lemma = Π-cong-contra ext (inverse ∥∥ᴱ≃∥∥ᴱ) λ _ → Eq.id754 755------------------------------------------------------------------------756-- Some results based on ""Generalizations of Hedberg's Theorem"" by757-- Kraus, Escardó, Coquand and Altenkirch758 759-- Types with constant endofunctions are ""h-stable"" (meaning that760-- ""mere inhabitance"" implies inhabitance).761 762constant-endofunction⇒h-stable :763 {f : A → A} → @0 Constant f → ∥ A ∥ᴱ → A764constant-endofunction⇒h-stable {A = A} {f = f} c =765 ∥ A ∥ᴱ ↝⟨ (rec λ where766 .∣∣ʳ x → f x , [ c (f x) x ]767 .truncation-is-propositionʳ → prop) ⟩768 (∃ λ (x : A) → Erased (f x ≡ x)) ↝⟨ proj₁ ⟩□769 A □770 where771 @0 prop : _772 prop = $⟨ fixpoint-lemma f c ⟩773 Is-proposition (∃ λ x → f x ≡ x) ↝⟨ H-level-cong _ 1 (∃-cong λ _ → inverse $ Er.erased Er.Erased↔) ⦂ (_ → _) ⟩□774 Is-proposition (∃ λ x → Erased (f x ≡ x)) □775 776-- Having a constant endofunction is logically equivalent to being777-- h-stable.778 779constant-endofunction⇔h-stable :780 (∃ λ (f : A → A) → Erased (Constant f)) ⇔ (∥ A ∥ᴱ → A)781constant-endofunction⇔h-stable = record782 { to = λ (_ , [ c ]) → constant-endofunction⇒h-stable c783 ; from = λ f → f ∘ ∣_∣784 , [ (λ x y →785 f ∣ x ∣ ≡⟨ cong f $ truncation-is-proposition _ _ ⟩∎786 f ∣ y ∣ ∎)787 ]788 }789 790------------------------------------------------------------------------791-- Some results related to _×_792 793-- The cartesian product of the truncation of A and A is equivalent794-- (with erased ""proofs"") to A.795 796∥∥ᴱ×≃ᴱ : (∥ A ∥ᴱ × A) ≃ᴱ A797∥∥ᴱ×≃ᴱ = EEq.↔→≃ᴱ798 proj₂799 (λ x → ∣ x ∣ , x)800 refl801 (λ _ → cong (_, _) (truncation-is-proposition _ _))802 803-- The application _≃ᴱ_.right-inverse-of ∥∥ᴱ×≃ᴱ x computes in a804-- certain way.805 806_ : _≃ᴱ_.right-inverse-of ∥∥ᴱ×≃ᴱ x ≡ refl _807_ = refl _808 809-- ∥_∥ᴱ commutes with _×_.810 811∥∥ᴱ×∥∥ᴱ↔∥×∥ᴱ : (∥ A ∥ᴱ × ∥ B ∥ᴱ) ↔ ∥ A × B ∥ᴱ812∥∥ᴱ×∥∥ᴱ↔∥×∥ᴱ = record813 { surjection = record814 { logical-equivalence = record815 { from = λ p → ∥∥ᴱ-map proj₁ p , ∥∥ᴱ-map proj₂ p816 ; to = uncurry $ rec λ where817 .∣∣ʳ x → rec λ where818 .∣∣ʳ y → ∣ x , y ∣819 .truncation-is-propositionʳ →820 truncation-is-proposition821 .truncation-is-propositionʳ →822 Π-closure ext 1 λ _ →823 truncation-is-proposition824 }825 ; right-inverse-of = elim λ where826 .∣∣ʳ _ → refl _827 .truncation-is-propositionʳ _ →828 mono₁ 1 truncation-is-proposition829 }830 ; left-inverse-of = uncurry $ elim λ where831 .∣∣ʳ _ → elim λ where832 .∣∣ʳ _ → refl _833 .truncation-is-propositionʳ _ →834 mono₁ 1 $835 ×-closure 1 truncation-is-proposition836 truncation-is-proposition837 .truncation-is-propositionʳ _ →838 Π-closure ext 1 λ _ →839 mono₁ 1 $840 ×-closure 1 truncation-is-proposition841 truncation-is-proposition842 }843 844------------------------------------------------------------------------845-- Some results related to h-levels846 847-- Variants of proj₁-closure.848 849private850 851 H-level-×₁-lemma :852 (A → ∥ B ∥ᴱ) →853 ∀ n → H-level (suc n) (A × B) → H-level (suc n) A854 H-level-×₁-lemma inhabited n h =855 [inhabited⇒+]⇒+ n λ a →856 flip rec (inhabited a) λ where857 .∣∣ʳ b →858 proj₁-closure (λ _ → b) (suc n) h859 .truncation-is-propositionʳ →860 H-level-propositional ext (suc n)861 862H-level-×₁ :863 (A → ∥ B ∥ᴱ) →864 ∀ n → H-level n (A × B) → H-level n A865H-level-×₁ inhabited zero h =866 propositional⇒inhabited⇒contractible867 (H-level-×₁-lemma inhabited 0 (mono₁ 0 h))868 (proj₁ (proj₁ h))869H-level-×₁ inhabited (suc n) =870 H-level-×₁-lemma inhabited n871 872H-level-×₂ :873 (B → ∥ A ∥ᴱ) →874 ∀ n → H-level n (A × B) → H-level n B875H-level-×₂ {B = B} {A = A} inhabited n =876 H-level n (A × B) ↝⟨ H-level.respects-surjection (from-bijection ×-comm) n ⟩877 H-level n (B × A) ↝⟨ H-level-×₁ inhabited n ⟩□878 H-level n B □879 880------------------------------------------------------------------------881-- Flattening882 883-- A generalised flattening lemma.884 885flatten′ :886 (F : (Type ℓ → Type ℓ) → Type f)887 (map : ∀ {G H} → (∀ {A} → G A → H A) → F G → F H)888 (f : F ∥_∥ᴱ → ∥ F id ∥ᴱ) →889 (∀ x → f (map ∣_∣ x) ≡ ∣ x ∣) →890 (∀ x → ∥∥ᴱ-map (map ∣_∣) (f x) ≡ ∣ x ∣) →891 ∥ F ∥_∥ᴱ ∥ᴱ ↔ ∥ F id ∥ᴱ892flatten′ _ map f f-map map-f = record893 { surjection = record894 { logical-equivalence = record895 { to = rec λ where896 .∣∣ʳ → f897 .truncation-is-propositionʳ → truncation-is-proposition898 ; from = ∥∥ᴱ-map (map ∣_∣)899 }900 ; right-inverse-of = elim λ where901 .∣∣ʳ → f-map902 .truncation-is-propositionʳ _ →903 mono₁ 1 truncation-is-proposition904 }905 ; left-inverse-of = elim λ where906 .∣∣ʳ → map-f907 .truncation-is-propositionʳ _ →908 mono₁ 1 truncation-is-proposition909 }910 911-- Nested truncations can be flattened.912 913flatten : ∥ ∥ A ∥ᴱ ∥ᴱ ↔ ∥ A ∥ᴱ914flatten {A = A} = flatten′915 (λ F → F A)916 (λ f → f)917 id918 (λ _ → refl _)919 (elim λ where920 .∣∣ʳ _ → refl _921 .truncation-is-propositionʳ _ → mono₁ 1 truncation-is-proposition)922 923private924 925 -- Another flattening lemma, given as an example of how flatten′ can926 -- be used.927 928 ∥∃∥∥ᴱ∥ᴱ↔∥∃∥ᴱ : ∥ ∃ (∥_∥ᴱ ∘ P) ∥ᴱ ↔ ∥ ∃ P ∥ᴱ929 ∥∃∥∥ᴱ∥ᴱ↔∥∃∥ᴱ {P = P} = flatten′930 (λ F → ∃ (F ∘ P))931 (λ f → Σ-map id f)932 (uncurry λ x → ∥∥ᴱ-map (x ,_))933 (λ _ → refl _)934 (uncurry λ _ → elim λ where935 .∣∣ʳ _ → refl _936 .truncation-is-propositionʳ _ →937 mono₁ 1 truncation-is-proposition)938 939-- A variant of flatten′ with _≃ᴱ_ instead of _↔_.940 941flatten-≃ᴱ :942 (F : (Type ℓ → Type ℓ) → Type f)943 (map : ∀ {G H} → (∀ {A} → G A → H A) → F G → F H)944 (f : F ∥_∥ᴱ → ∥ F id ∥ᴱ) →945 @0 (∀ x → f (map ∣_∣ x) ≡ ∣ x ∣) →946 @0 (∀ x → ∥∥ᴱ-map (map ∣_∣) (f x) ≡ ∣ x ∣) →947 ∥ F ∥_∥ᴱ ∥ᴱ ≃ᴱ ∥ F id ∥ᴱ948flatten-≃ᴱ _ map f f-map map-f = EEq.↔→≃ᴱ949 (rec λ where950 .∣∣ʳ → f951 .truncation-is-propositionʳ → truncation-is-proposition)952 (∥∥ᴱ-map (map ∣_∣))953 (elim λ @0 where954 .∣∣ʳ → f-map955 .truncation-is-propositionʳ _ →956 mono₁ 1 truncation-is-proposition)957 (elim λ @0 where958 .∣∣ʳ → map-f959 .truncation-is-propositionʳ _ →960 mono₁ 1 truncation-is-proposition)961 962------------------------------------------------------------------------963-- The propositional truncation operator is a monad964 965-- A universe-polymorphic variant of bind.966 967infixl 5 _>>=′_968 969_>>=′_ : ∥ A ∥ᴱ → (A → ∥ B ∥ᴱ) → ∥ B ∥ᴱ970x >>=′ f = _↔_.to flatten (∥∥ᴱ-map f x)971 972-- The universe-polymorphic variant of bind is associative.973 974>>=′-associative :975 (x : ∥ A ∥ᴱ) →976 x >>=′ (λ x → f x >>=′ g) ≡ x >>=′ f >>=′ g977>>=′-associative = elim λ where978 .∣∣ʳ _ → refl _979 .truncation-is-propositionʳ _ → ⇒≡ 1 truncation-is-proposition980 981instance982 983 -- The propositional truncation operator is a monad.984 985 raw-monad : Raw-monad (∥_∥ᴱ {a = a})986 Raw-monad.return raw-monad = ∣_∣987 Raw-monad._>>=_ raw-monad = _>>=′_988 989 monad : Monad (∥_∥ᴱ {a = a})990 Monad.raw-monad monad = raw-monad991 Monad.left-identity monad _ _ = refl _992 Monad.associativity monad x _ _ = >>=′-associative x993 Monad.right-identity monad = elim λ where994 .∣∣ʳ _ → refl _995 .truncation-is-propositionʳ _ → ⇒≡ 1 truncation-is-proposition996 997------------------------------------------------------------------------998-- Surjectivity999 1000-- A variant of surjectivity with ""erased proofs"".1001 1002Surjectiveᴱ :1003 {A : Type a} {B : Type b} →1004 (A → B) → Type (a ⊔ b)1005Surjectiveᴱ f = ∀ y → ∥ f ⁻¹ᴱ y ∥ᴱ1006 1007-- The property Surjectiveᴱ f is a proposition (in erased contexts).1008 1009@0 Surjectiveᴱ-propositional : Is-proposition (Surjectiveᴱ f)1010Surjectiveᴱ-propositional =1011 Π-closure ext 1 λ _ →1012 truncation-is-proposition1013 1014-- The function ∣_∣ is surjective (with erased proofs).1015 1016∣∣-surjective : Surjectiveᴱ (∣_∣ {A = A})1017∣∣-surjective = elim λ where1018 .∣∣ʳ x → ∣ x , [ refl _ ] ∣1019 .truncation-is-propositionʳ _ → truncation-is-proposition1020 1021-- Split surjective functions are surjective (with erased proofs).1022 1023Split-surjective→Surjectiveᴱ :1024 Split-surjective f → Surjectiveᴱ f1025Split-surjective→Surjectiveᴱ s = λ y → ∣ ECP.⁻¹→⁻¹ᴱ (s y) ∣1026 1027-- Being both surjective (with erased proofs) and an embedding1028-- (completely erased) is equivalent to being an equivalence (with1029-- erased proofs).1030--1031-- This result, without erasure, is Corollary 4.6.4 from the first1032-- edition of the HoTT book.1033 1034Surjectiveᴱ×Erased-Is-embedding≃ᴱIs-equivalenceᴱ :1035 (Surjectiveᴱ f × Erased (Is-embedding f)) ≃ᴱ Is-equivalenceᴱ f1036Surjectiveᴱ×Erased-Is-embedding≃ᴱIs-equivalenceᴱ {f = f} = EEq.⇔→≃ᴱ1037 (×-closure 11038 Surjectiveᴱ-propositional1039 (Er.H-level-Erased 11040 (Emb.Is-embedding-propositional ext)))1041 (EEq.Is-equivalenceᴱ-propositional ext f)1042 (λ (is-surj , is-emb) →1043 _⇔_.from EEq.Is-equivalenceᴱ⇔Is-equivalenceᴱ-CP $ λ y →1044 $⟨ is-surj y ⟩1045 ∥ f ⁻¹ᴱ y ∥ᴱ ↝⟨ (rec λ where1046 .∣∣ʳ p → ECP.inhabited→Is-proposition→Contractibleᴱ p1047 (H-level-cong _ 11048 ECP.⁻¹≃⁻¹ᴱ1049 (Emb.embedding→⁻¹-propositional (Er.erased is-emb) _))1050 .truncation-is-propositionʳ →1051 ECP.Contractibleᴱ-propositional ext) ⟩□1052 Contractibleᴱ (f ⁻¹ᴱ y) □)1053 (λ is-eq@(inv , [ r-inv , _ ]) →1054 (λ y → $⟨ inv y , [ r-inv y ] ⟩1055 f ⁻¹ᴱ y ↝⟨ ∣_∣ ⟩1056 ∥ f ⁻¹ᴱ y ∥ᴱ □)1057 1058 , ($⟨ is-eq ⟩1059 Is-equivalenceᴱ f ↝⟨ Er.[_]→ ⟩1060 Erased (Is-equivalenceᴱ f) ↝⟨ Er.map EEq.Is-equivalenceᴱ→Is-equivalence ⟩1061 Erased (Is-equivalence f) ↝⟨ Er.map Emb.Is-equivalence→Is-embedding ⟩□1062 Erased (Is-embedding f) □))1063 1064------------------------------------------------------------------------1065-- Another lemma1066 1067-- The function λ R x y → ∥ R x y ∥ᴱ preserves Is-equivalence-relation.1068 1069∥∥ᴱ-preserves-Is-equivalence-relation :1070 Is-equivalence-relation R →1071 Is-equivalence-relation (λ x y → ∥ R x y ∥ᴱ)1072∥∥ᴱ-preserves-Is-equivalence-relation R-equiv = record1073 { reflexive = ∣ reflexive ∣1074 ; symmetric = symmetric ⟨$⟩_1075 ; transitive = λ p q → transitive ⟨$⟩ p ⊛ q1076 }1077 where1078 open Is-equivalence-relation R-equiv1079 1080------------------------------------------------------------------------1081-- Definitions related to truncated binary sums1082 1083-- Truncated binary sums.1084 1085infixr 1 _∥⊎∥ᴱ_1086 1087_∥⊎∥ᴱ_ : Type a → Type b → Type (a ⊔ b)1088A ∥⊎∥ᴱ B = ∥ A ⊎ B ∥ᴱ1089 1090-- Introduction rules.1091 1092∣inj₁∣ : A → A ∥⊎∥ᴱ B1093∣inj₁∣ = ∣_∣ ∘ inj₁1094 1095∣inj₂∣ : B → A ∥⊎∥ᴱ B1096∣inj₂∣ = ∣_∣ ∘ inj₂1097 1098-- In erased contexts _∥⊎∥ᴱ_ is pointwise propositional.1099 1100@0 ∥⊎∥ᴱ-propositional : Is-proposition (A ∥⊎∥ᴱ B)1101∥⊎∥ᴱ-propositional = truncation-is-proposition1102 1103-- The _∥⊎∥ᴱ_ operator preserves ""symmetric"" functions.1104 1105infixr 1 _∥⊎∥ᴱ-cong_1106 1107_∥⊎∥ᴱ-cong_ :1108 A₁ ↝[ ⌊ k ⌋-sym ] A₂ → B₁ ↝[ ⌊ k ⌋-sym ] B₂ →1109 (A₁ ∥⊎∥ᴱ B₁) ↝[ ⌊ k ⌋-sym ] (A₂ ∥⊎∥ᴱ B₂)1110A₁↝A₂ ∥⊎∥ᴱ-cong B₁↝B₂ = ∥∥ᴱ-cong (A₁↝A₂ ⊎-cong B₁↝B₂)1111 1112-- _∥⊎∥ᴱ_ is commutative.1113 1114∥⊎∥ᴱ-comm : A ∥⊎∥ᴱ B ↔ B ∥⊎∥ᴱ A1115∥⊎∥ᴱ-comm = ∥∥ᴱ-cong ⊎-comm1116 1117-- If one truncates the types to the left or right of _∥⊎∥ᴱ_, then one1118-- ends up with an isomorphic type.1119 1120truncate-left-∥⊎∥ᴱ : A ∥⊎∥ᴱ B ↔ ∥ A ∥ᴱ ∥⊎∥ᴱ B1121truncate-left-∥⊎∥ᴱ =1122 inverse $1123 flatten′1124 (λ F → F _ ⊎ _)1125 (λ f → ⊎-map f id)1126 P.[ ∥∥ᴱ-map inj₁ , ∣inj₂∣ ]1127 P.[ (λ _ → refl _) , (λ _ → refl _) ]1128 P.[ (elim λ where1129 .∣∣ʳ _ → refl _1130 .truncation-is-propositionʳ _ →1131 mono₁ 1 ∥⊎∥ᴱ-propositional)1132 , (λ _ → refl _)1133 ]1134 1135truncate-right-∥⊎∥ᴱ : A ∥⊎∥ᴱ B ↔ A ∥⊎∥ᴱ ∥ B ∥ᴱ1136truncate-right-∥⊎∥ᴱ {A = A} {B = B} =1137 A ∥⊎∥ᴱ B ↝⟨ ∥⊎∥ᴱ-comm ⟩1138 B ∥⊎∥ᴱ A ↝⟨ truncate-left-∥⊎∥ᴱ ⟩1139 ∥ B ∥ᴱ ∥⊎∥ᴱ A ↝⟨ ∥⊎∥ᴱ-comm ⟩□1140 A ∥⊎∥ᴱ ∥ B ∥ᴱ □1141 1142-- _∥⊎∥ᴱ_ is associative.1143 1144∥⊎∥ᴱ-assoc : A ∥⊎∥ᴱ (B ∥⊎∥ᴱ C) ↔ (A ∥⊎∥ᴱ B) ∥⊎∥ᴱ C1145∥⊎∥ᴱ-assoc {A = A} {B = B} {C = C} =1146 ∥ A ⊎ ∥ B ⊎ C ∥ᴱ ∥ᴱ ↝⟨ inverse truncate-right-∥⊎∥ᴱ ⟩1147 ∥ A ⊎ B ⊎ C ∥ᴱ ↝⟨ ∥∥ᴱ-cong ⊎-assoc ⟩1148 ∥ (A ⊎ B) ⊎ C ∥ᴱ ↝⟨ truncate-left-∥⊎∥ᴱ ⟩□1149 ∥ ∥ A ⊎ B ∥ᴱ ⊎ C ∥ᴱ □1150 1151-- ⊥ is a left and right identity of _∥⊎∥ᴱ_ if the other argument is a1152-- proposition.1153 1154∥⊎∥ᴱ-left-identity : @0 Is-proposition A → ⊥ {ℓ = ℓ} ∥⊎∥ᴱ A ↔ A1155∥⊎∥ᴱ-left-identity {A = A} A-prop =1156 ∥ ⊥ ⊎ A ∥ᴱ ↝⟨ ∥∥ᴱ-cong ⊎-left-identity ⟩1157 ∥ A ∥ᴱ ↝⟨ ∥∥ᴱ↔ A-prop ⟩□1158 A □1159 1160∥⊎∥ᴱ-right-identity : @0 Is-proposition A → A ∥⊎∥ᴱ ⊥ {ℓ = ℓ} ↔ A1161∥⊎∥ᴱ-right-identity {A = A} A-prop =1162 A ∥⊎∥ᴱ ⊥ ↔⟨ ∥⊎∥ᴱ-comm ⟩1163 ⊥ ∥⊎∥ᴱ A ↔⟨ ∥⊎∥ᴱ-left-identity A-prop ⟩□1164 A □1165 1166-- _∥⊎∥ᴱ_ is idempotent for propositions (up to equivalences with1167-- erased proofs).1168 1169∥⊎∥ᴱ-idempotent : @0 Is-proposition A → (A ∥⊎∥ᴱ A) ≃ᴱ A1170∥⊎∥ᴱ-idempotent {A = A} A-prop =1171 ∥ A ⊎ A ∥ᴱ ↝⟨ idempotent ⟩1172 ∥ A ∥ᴱ ↔⟨ ∥∥ᴱ↔ A-prop ⟩□1173 A □1174 1175-- Sometimes a truncated binary sum is equivalent (with erased proofs)1176-- to one of its summands.1177 1178drop-left-∥⊎∥ᴱ :1179 @0 Is-proposition B → (A → B) → (A ∥⊎∥ᴱ B) ≃ᴱ B1180drop-left-∥⊎∥ᴱ B-prop A→B = EEq.⇔→≃ᴱ1181 ∥⊎∥ᴱ-propositional1182 B-prop1183 (rec λ where1184 .∣∣ʳ → P.[ A→B , id ]1185 .truncation-is-propositionʳ → B-prop)1186 ∣inj₂∣1187 1188drop-right-∥⊎∥ᴱ :1189 @0 Is-proposition A → (B → A) → (A ∥⊎∥ᴱ B) ≃ᴱ A1190drop-right-∥⊎∥ᴱ {A = A} {B = B} A-prop B→A =1191 A ∥⊎∥ᴱ B ↔⟨ ∥⊎∥ᴱ-comm ⟩1192 B ∥⊎∥ᴱ A ↝⟨ drop-left-∥⊎∥ᴱ A-prop B→A ⟩□1193 A □1194 1195-- Sometimes a truncated binary sum is isomorphic to one of its1196-- summands.1197 1198drop-⊥-right-∥⊎∥ᴱ :1199 @0 Is-proposition A → ¬ B → A ∥⊎∥ᴱ B ↔ A1200drop-⊥-right-∥⊎∥ᴱ A-prop ¬B = record