{-# OPTIONS --guardedness #-}
module README.Compiling-Programs-with-Erased-Univalence where
import Coherently-constant
import Colimit.Sequential
import Colimit.Sequential.Very-erased
import Equality.Path
import Equality.Path.Univalence
import Equivalence
import Equivalence.Erased
import Equivalence.Erased.Basics
import Equivalence.Erased.Contractible-preimages
import Equivalence.Half-adjoint
import Erased.Basics
import Erased.Cubical
import Erased.Level-1
import Erased.Stability
import H-level.Truncation.Propositional
import H-level.Truncation.Propositional.Completely-erased
import H-level.Truncation.Propositional.Erased
import H-level.Truncation.Propositional.Non-recursive
import H-level.Truncation.Propositional.Non-recursive.Erased
import H-level.Truncation.Propositional.One-step
import Preimage
import Univalence-axiom
import Lens.Non-dependent.Higher
import Lens.Non-dependent.Higher.Erased
import Lens.Non-dependent.Higher.Capriotti.Variant.Erased.Variant
import Lens.Non-dependent.Higher.Coinductive
import Lens.Non-dependent.Higher.Coinductive.Erased
import Lens.Non-dependent.Higher.Coinductive.Small
import Lens.Non-dependent.Higher.Coinductive.Small.Erased
import README.Fst-snd
cong = Equality.Path.cong
ext = Equality.Path.⟨ext⟩
@0 ∥_∥ : _
∥_∥ = H-level.Truncation.Propositional.∥_∥
@0 map : _
map = H-level.Truncation.Propositional.∥∥-map
∥_∥ᴱ = H-level.Truncation.Propositional.Erased.∥_∥ᴱ
Is-equivalence = Equivalence.Half-adjoint.Is-equivalence
_≃_ = Equivalence._≃_
Univalence = Univalence-axiom.Univalence
@0 univ : _
univ = Equality.Path.Univalence.univ
Erased = Erased.Basics.Erased
[]-cong = Erased.Cubical.[]-cong-Path
Is-equivalenceᴱ = Equivalence.Erased.Basics.Is-equivalenceᴱ
_≃ᴱ_ = Equivalence.Erased.Basics._≃ᴱ_
to = Equivalence.Erased.Basics._≃ᴱ_.to
from = Equivalence.Erased.Basics._≃ᴱ_.from
@0 to-from : _
to-from = Equivalence.Erased.Basics._≃ᴱ_.right-inverse-of
@0 from-to : _
from-to = Equivalence.Erased.Basics._≃ᴱ_.left-inverse-of
Erased≃ = Erased.Level-1.Erased↔
Lemma-41 = Erased.Level-1.[]-cong₁.Erased-cong-≃
Lemma-42 = Equivalence.Erased.[]-cong.Σ-cong-≃ᴱ-Erased
substᴱ = Erased.Level-1.[]-cong₁.substᴱ
subst = Equality.Path.subst
Lemma-45 = Equivalence.Erased.[]-cong.drop-⊤-left-Σ-≃ᴱ-Erased
Lemma-46 = Equivalence.Erased.Σ-cong-≃ᴱ
Lemma-47 = Equivalence.Erased.drop-⊤-left-Σ-≃ᴱ
@0 ∥_∥¹ : _
∥_∥¹ = H-level.Truncation.Propositional.One-step.∥_∥¹
@0 Colimit : _
Colimit = Colimit.Sequential.Colimit
@0 Lemma-50 : _
Lemma-50 = Colimit.Sequential.universal-property
@0 ∥_∥¹-out : _
∥_∥¹-out = H-level.Truncation.Propositional.One-step.∥_∥¹-out-^
@0 ∥_∥ᴺ : _
∥_∥ᴺ = H-level.Truncation.Propositional.Non-recursive.∥_∥
@0 ∥∥ᴺ≃∥∥ : _
∥∥ᴺ≃∥∥ = H-level.Truncation.Propositional.Non-recursive.∥∥≃∥∥
Colimitᴱ = Colimit.Sequential.Very-erased.Colimitᴱ
Lemma-54 = Colimit.Sequential.Very-erased.universal-property
∥_∥ᴺᴱ = H-level.Truncation.Propositional.Non-recursive.Erased.∥_∥ᴱ
Lemma-56 = H-level.Truncation.Propositional.Erased.∥∥ᴱ≃∥∥ᴱ
@0 Lensᴱ : _
Lensᴱ = Lens.Non-dependent.Higher.Lens
@0 get : _
get = Lens.Non-dependent.Higher.Lens.get
@0 set : _
set = Lens.Non-dependent.Higher.Lens.set
Lensᴱᴱ = Lens.Non-dependent.Higher.Erased.Lens
_⁻¹_ = Preimage._⁻¹_
@0 Lens^C : _
Lens^C = Lens.Non-dependent.Higher.Coinductive.Small.Lens
@0 Coherently-constant^C : _
Coherently-constant^C =
Lens.Non-dependent.Higher.Coinductive.Small.Coherently-constant
Lens^CE = Lens.Non-dependent.Higher.Coinductive.Small.Erased.Lens
Lemma-65 =
Lens.Non-dependent.Higher.Coinductive.Small.Erased.Lens≃ᴱLensᴱ
@0 Lemma-65-preserves-getters-and-setters : _
Lemma-65-preserves-getters-and-setters =
Lens.Non-dependent.Higher.Coinductive.Small.Erased.Lens≃ᴱLensᴱ-preserves-getters-and-setters
Lens₁ᴱ = Lens.Non-dependent.Higher.Capriotti.Variant.Erased.Variant.Lens
Lens₂ᴱ = Lens.Non-dependent.Higher.Coinductive.Erased.Lens
_⁻¹ᴱ_ = Equivalence.Erased.Contractible-preimages._⁻¹ᴱ_
Coherently-constant₁ᴱ =
Lens.Non-dependent.Higher.Capriotti.Variant.Erased.Variant.Coherently-constant
@0 Coherently-constant : _
Coherently-constant = Coherently-constant.Coherently-constant
Coherently-constant₂ᴱ =
Lens.Non-dependent.Higher.Coinductive.Erased.Coherently-constant
@0 Coherently-constant₂^C : _
Coherently-constant₂^C =
Lens.Non-dependent.Higher.Coinductive.Coherently-constant
@0 constant : _
constant = Lens.Non-dependent.Higher.Coinductive.constant
Lemma-74 = Erased.Stability.[]-cong.Erased-other-singleton≃ᴱ⊤
Lemma-75 = Lens.Non-dependent.Higher.Coinductive.Erased.∥∥ᴱ→≃
Lemma-76 = Equivalence.Erased.other-singleton-with-Π-≃ᴱ-≃ᴱ-⊤
Lemma-77 = H-level.Truncation.Propositional.Erased.Σ-Π-∥∥ᴱ-Erased-≡-≃
sndᴱ = Lens.Non-dependent.Higher.Erased.snd
Lemma-79 =
H-level.Truncation.Propositional.Completely-erased.Erased-∥∥×≃
snd^C = README.Fst-snd.snd-with-space-leak
Lemma-81 =
Lens.Non-dependent.Higher.Coinductive.Small.Erased.with-other-setter
snd^C-with-changed-setter = README.Fst-snd.snd