Skip to content

Latest commit

 

History

History
778 lines (706 loc) · 54.7 KB

meeting20200822.md

File metadata and controls

778 lines (706 loc) · 54.7 KB

Summary

Questions from the video

  • characterization of abs on ℂ
    • one property could be iᶜ : ℝ → ℂ, |·|ᶜ : ℂ → ℝ is such that ∀(x : ℂ) → | x |ᶜ ≡ | | x |ᶜ |ʳ
    • but this is kind of weak and there have to be more properties
  • characterization of sqrt on ℝ₀⁺
    • √x · √x ≡ x and √(x · x) ≡ x
    • use eulers algorithm as an "implementation" (because it is simple)
  • disjointness does not need vice-versa, because P → ¬Q is equivalent to Q → ¬P
  • Q: definitions of "ℝ or ℂ"
    • A: using R-modules should already leverage this

immediate TODOs

  • proof of 0 ≤ x → x < y → 0 < x + y from sketch
  • turn the 10 direct inclusions into 4 chained inclusions ℕ↪ℤ, ℤ↪ℚ, ℚ↪ℝ, ℝ↪ℂ
    • this should give difficult preservation properties of how the abs function interacts with inclusion into the complex numbers a single spot of occurence in ℝ↪ℂ and we need not to care about ℤ↪ℂ or similar
  • since we want apartness _#_ and absolute value function abs on all algebraic structures that are "backing" the number hierarchy, it'd be more sound to rename the Semiring into ApartnessSemiring or ApartnessAbsSemiring
    • or even skip all this and name it ℕ-struct
  • the embedding from the standard library does not apply to types with structure but only to their carrier set
    • this becomes obvious, since a type with structure is a tuple and not a type
  • a constructive characterization for the complex numbers that would be "compatible" to state facts about the abs function could be
    • ?? ∀(x : ℂ) → x # 0ᶜ → Σ[ r ∈ ℝ₀⁺ ] → ∃[ φ ∈ ℝ ] → x ≡ r · exp (i · φ) ??
      • this is not a sufficient characterization because it does not chacacterize abs on all of ℂ
      • even if we'd add abs 0 = 0 to it, still this would require splitting ℂ into two parts (zero and nonzero) to make a complete characterization which is not possible constructively
      • so we might add a continuity-characterization to it (i.e. abs is ε-δ-continuous) from which should follow abs 0 = 0
      • but still this is likely not the most elegant characterization
      • pitfall: define a notion of continuity on ℂ without making use of the absolute value function is tricky
    • this would be a "continuous" formulation and it made x # 0ᶜ and φ ∈ ℝ necessary
    • ?? how to define exp? ??
  • Auke's chapter 8 gives metric spaces and pesudometric spaces
    • and complete metric spaces
    • the non-cubical standard library 1.4-rc1 "Added a hierarchy for metric spaces" 
      Function.Metric
Function.Metric.Core
Function.Metric.Definitions
Function.Metric.Structures
Function.Metric.Bundles
  • vector spaces can be formalized as R-modules
    • whith scalar multiplication being defined as a "ring over the space of linear endomorphisms of the carrier set"
    • and then we instance-proof an ℝ-module or a ℂ-module
    • it cannot be proven constructively that every finite dimenional vector space has a basis (i.e. we cannot constructively pick such a basis)
      • therefore we might add a VectorSpaceWithBasis that comes equipped with a basis already
  • apartness on normed vector spaces from the norm: x # 0ᵛ := || x ||ᵛ #ʳ 0ʳ for the underlying ring
    • similar x # y := || (x - y) ||ᵛ #ʳ 0ʳ
  • ?? are there "normed R-modules" then (for normed vector spaces)? ??
  • ‹ x , x ›ᶜ ∈ ℝ follows from conjugate symmetry of ‹_,_›ᶜ and a property of conjᶜ
    • ∀ z → z ≡ conjᶜ z → Σ[ r ∈ ℝ ] ℝ↪ℂ r ≡ z
      • and we should also have the back direction ∀ r → ℝ↪ℂ r ≡ conjᶜ (ℝ↪ℂ r) which follows from preservation of conj along ℝ↪ℂ and that congʳ = idʳ

facts and heuristics about constructive mathematics

  • cauchy convergence on function spaces could be difficult
  • there are several structure identity principles
  • that some structure identity principle applies for a mathematical structure is a property of that structure (i.e. the SIP does not generally apply)
    • e.g. for topological spaces (in the classical definition) it does not apply
    • e.g. for fields it is also difficult, since _¯¹ is only partially defined
  • when the SIP from the Σ-theory applies, then we have that "structure preserving bijections" make "the" equivalences between two mathematical structures
    • this also means that for the mathematical structures for which this applies, we have that one does not need to care about the properties
      • the question of "whether the properties are preserved automatically" does not typecheck, i.e. it does not direcly make sense
      • but what it means, could be "whether it is possible to add any new (!) information/properties to a bijected structure when using the bijection that were not derivable before on the bijected structure alone"
        • ?? for "types with structure" this should not be the case ??
    • ?? we had some point about a difference of sets and types ??
  • the "purpose" of SIP is to support the one-liner: "equality 'is' equivalence" (and vice-versa)
    • Univalence: For any two types X, Y, this map (X = Y) → (X ≃ Y) is an equivalence.
    • (Cubical.Foundations.Id) univalenceId : ∀ {ℓ} {A B : Type ℓ} → (A ≡ B) ≃ (A ≃ B)
  • subsets/subspaces
    • ?? embeddings "are" subspaces ??
    • ?? SIP minus one of the identities is an injection/embedding ??
    • "the" set theory is what we find in Cubical.Foundations.Logic
    • subsets are predicates (i.e. X → hProp where X isSet)
    • subspaces are spaces over subsets
  • what is meant by "structure preserving" is straight forward for n-ary operations and n-ary relations
  • constructive topology knows a multitude of different formalizations, where classical topology is relatively clear-cut
  • HITs are "an alternative to setoid-hell"
    • the "strategy" is to proof an eliminator on hProps first
    • in a way that we can make use of the base-cases of the HIT
    • and then use it to proof other properties like binary or ternary ones
  • there are three separate things
    • the carrier set
    • the structure on the carrier set
      • ?? structure = n-ary operations and n-ary relations ??
    • and axioms for these
  • we have ∀ x y → x # 0 → (x < y) ⨄ (y < x) on ℚ and ℝ
    • and we have ¬(x # y) → x ≡ y by tightness of #
    • and we have x ≡ y → ¬(x # y) by irreflexivity of #
  • we have trichotomy ∀(q r : ℚ) → (q < r) ⨄ (q ≡ r) ⨄ (r < q) on ℚ
    • therefore, we do have a linear order ∀ x → (x ≤ 0) ∨ (0 ≤ x) on ℚ
    • linear order gives ∀ x y → (max x y ≡ x) ∨ (max x y ≡ y)
    • without a linear order, we still have
      • ∀ x y z → (z < max x y) ⇔ (z < x) ∨ (z < y)
      • ∀ x y z → (min x y < z) ⇔ (x < z) ∨ (y < z)
  • we do NOT have trichotomy on ℝ
    • in particular, we do NOT have ∀ x → x # 0 ⨄ x ≡ 0
    • and we do NOT have a linear order on ℝ, since trichotomy implies the linear order
    • but we still have x # 0 → (0 < x) ⨄ (x < 0)
      • we do NOT have ∀ x → (abs x ≡ x) ∨ (abs x ≡ - x)
      • but maybe we have x # 0 → (abs x ≡ x) ⨄ (abs x ≡ - x)
    • and we have cotransitivity ∀ x y z → x < y → (x < z) ∨ (z < y)
      • which is similar in the sense that ∀ z ε → 0 < 0 + ε → (z < 0 + ε) ∨ (0 < z) follows from it
      • with x = 0 and y = ε we get ∀ ε z → 0 < ε → (0 < z) ∨ (z < ε)
        • which should be equivalent to ∀ z → (0 < z) ∨ (∀ ε → 0 < ε → (z < ε))
      • so ∀ ε → 0 < ε → (z < ε) which is ¬(ε < z) or z ≤ ε is somehow weaker than z ≤ 0 which is ¬(0 < z)
        • so we get ∀ z → z ≤ 0 → (∀ ε → 0 < ε → z ≤ ε)
        • which is similar to item R3.12 in [Bridges 1999] ∀ z → 0 ≤ z → ((z ≡ 0) ⇔ (∀ ε → 0 < ε → z < ε))
        • in particular ∀ z → 0 ≤ z → (∀ ε → 0 < ε → z < ε) → z ≡ 0
      • so we should have ∀ z → 0 ≤ z → (0 < z) ∨ z ≡ 0
    • and we have ∀ x → ¬(x < 0) → ¬(0 < x) → x ≡ 0 by antisymmetry of <
  • some classical properties (that do not assume any structure classically) come with an additional structure in their constructive form (if there is a constructive form)
    • assuming an additional structure is "weaker" than not doing so
  • we do not have just IsCauchy as a "property", we do have a ModulusOfCauchyConvergence as a "structure" for a given sequence
    • cauchy completeness then does not turn IsCauchy-sequences into limits, but sequence-modulus-pairs instead
  • an idiom seems to use ... ⇒ ¬(P ∧ Q) when we cannot use ... ⇒ (P ⊎ Q) (because we choose which one is which)
    • ¬(P ∧ Q) ⇔ (P ⇒ ¬ Q) ⇔ (Q ⇒ ¬ P) ⇔ (P × Q ⇒ ⊥)
  • literature
    • (famous for the development are: Brouwer, Bishop (1967) and Bridges (1985))
    • Bridges 1990 - Linear mappings are fairly well-behaved
      • in the presence of completeness linear maps are well-behaved in our formal sense and have certain other aspects of good behaviour as well.
      • Let us agree that a linear mapping T between normed spaces is well-behaved if T x ≠ 0 whenever x ∈ E is distinct from each element of ker (T), the kernel of T.
      • (Note that when we say that two elements x, y of a metric space (X, ρ) are distinct, and we write x ≠ y, we mean that ρ(x, y) > 0.)
      • It is perhaps surprising that we cannot prove constructively that every bounded linear mapping T : ℝ → ℝ, is well-behaved.
      • For if we could do this, then, by considering mappings of the form x ↦ ax where a ∈ ℝ and ¬(a = 0), we would be able to prove the statement ∀ x ∈ ℝ → (¬(x = 0) ⇒ x ≠ 0), which is equivalent to Markov's principle:
        • if (aₙ) is a binary sequence such that ¬ (∀ n → (aₙ = 0)), then there exists n such that aₙ = 1.
      • (Note, in passing, that Markov's principle implies constructively that every linear map between normed spaces is well-behaved.)
      • Although some constructive mathematicians are prepared to accept Markov's principle, most are not, and we remain unconvinced of the constructive validity of any proposition that entails it.
      • Theorem 1. A linear mapping of a normed space onto a Banach space is well-behaved.
      • A mapping f between metric spaces is said to be
        • one-one, if f(x) = f(y) ⇒ x = y
        • strongly one-one, if x ≠ y ⇒ f(x) ≠ f(y)
        • Corollary 0: A one-one linear map of a normed space onto a Banach space is strongly one-one
      • ... graph
      • ... some extensionality
      • linearly independent
      • metrically independent
    • Bridges 1999 - Constructive mathematics: a foundation for computable analysis has a section about "Constructive axioms for the real line"
      • (writes x ≠ y for x # y)
      • We identify the sets ℕ of natural numbers, ℕ⁺ of positive integers, ℤ of integers, and ℚ of rational numbers with the usual subsets of ℝ: for example we identify ℕ⁺ with {n1 : n ∈ ℕ⁺}
      • We assume that all relations and operations are extensional: for example, to say that the relation > is extensional means that if x > y, x = x', and y = y', then x' > y'.
      • x ≠ y iff (x > y or y > x)
      • x > y iff ∀ z → (y > z) ⇒ (x > z)
      • R1. R is a Heyting field ∀(x y z : R)
        • x + y = y + x
        • (x + y) + z = x + (y + z)
        • 0 + x = x
        • x + (- x) = 0
        • x · y = y · x
        • (x · y) · z = x · (y · z)
        • 1 · x = x
        • x · x ⁻¹ = 1 if x ≠ 0 (¬(x = 0) is not sufficient)
        • x · (y + z) = x · y + x · z
      • R2. Basic properties of > …
        • ¬((x < y) ∧ (y < x)) (irreflexivity, equivalent to x < y → ¬ y < x)
        • (x > y) ⇒ (∀ z → (x > z) ∨ (z > y)) (cotransitivity)
        • ¬(x ≠ y) ⇒ (x = y) (tightness)
        • (x > y) ⇒ (∀ z → (x + z) > (y + z)) (+-preserves-<)
        • (x > 0) ∧ (y > 0) ⇒ (x · y > 0)
          • ⇔ (x - z > 0) ∧ (y > 0) ⇒ ((x - z) · y > 0)
          • ⇔ (x > z) ∧ (y > 0) ⇒ (x · y > z · y)
          • ⇔ (y > 0) → (x > z) → (x · y > z · y) (·-preserves-<)
      • the notions bounded above, bounded below, and bounded are defined as in classical mathematics
        • e.g. if S is a nonempty subset of ℝ that is bounded above, then its least upper bound, if it exists, is the unique real number b such that
          • b is an upper bound of S, and
          • for each b' < b there exists s ∈ S such that s > b'.
          • ?? supremum S = Σ[ b ∈ S ] (IsUpperBound S b) × (∀ b' → b' < b → ∃[ s ∈ S ] b' < s) ??
        • (Note that nonempty means what the intuitionists call "inhabited"; that is, we can construct an element of the set in question.)
      • R3. Special properties of > …
        • ¬(x > x)
        • x ≥ x
        • (x > y) ∧ (y > z) ⇒ x > z
        • ¬((x > y) ∧ (y ≥ x))
        • (x > y ≥ z) ⇒ (x > z)
        • (x ≥ y > z) ⇒ (x > z)
        • ¬(x > y) ⇔ (y ≥ x)
        • ¬(x ≥ y) ⇔ ¬¬(y > x)
        • (x ≥ y ≥ z) ⇔ (x ≥ z)
        • (x ≥ y) ∧ (y ≥ x) ⇒ (x = y)
        • ¬((x > y) ∧ (x = y))
        • (x ≥ 0) ⇒ ((x = 0) ⇔ (∀(ε > 0) → (x < ε)))
        • (x + y > 0) ⇒ (x > 0) ∨ (y > 0)
        • (x > 0) ⇒ (- x < 0)
        • (x > y) ∧ (z < 0) ⇒ (y · z > x · z)
        • (x ≠ 0) ⇒ x² > 0
        • 1 > 0
        • x² ≥ 0
        • (0 < x < 1) ⇒ (x > x²)
        • (- 1 < x < 1) ⇒ ¬((x² > x) ∧ (x² > - x))
        • (x² > 0) ⇒ (x ≠ 0)
        • (x > 0) ⇒ (x ⁻¹ ≥ 0)
        • ∀ m m' n n' → 0 < n → 0 < n' → (m / n > m' / n') ⇔ (m · n' > m' · n)
        • ∀(n ∈ ℕ⁺) → (n ⁻¹ > 0)
        • x > 0 → y ≥ 0 → ∃[ n ∈ ℤ ] n · x > y
        • (x > 0) ⇒ (x ⁻¹ > 0)
        • (x · y > 0) ⇒ (x ≠ 0) ∧ (y ≠ 0)
        • ∀(x > 0) → ∃[ n ∈ ℕ⁺ ] x < n < x + 2
        • ∀ a b → a < b → ∃[ q ∈ ℚ ] a < r < b
    • Bridges 2006 - Techniques of Constructive Analysis seems to have a chapter about Hilbert spaces which also defines adjoints
    • Diener 2008 - Compactness Under Constructive Scrutiny has a chapter about "Differentiable manifolds"
    • Richman 2007 - Real numbers and other completions writes about
      • completeness of metric spaces,
      • axioms for the real numbers, and a construction of the real numbers that is appropriate for those axioms.
    • Seminar "Konstruktive Analysis 2019" von Helmut Schwichtenberg

recent commits on cubical master

My version of the standard library is "Ring structure on square matrices (#348)" from 04.07.2020 21:30:32 +0200 which is commit 76f647ddb58c61c88f2116197f3ad77cf198b8de. Since then there are some changes that'd affect an update:

further development and theory

  • assuming a lot of given structure to work with
    • e.g. multivalued piecewise continuous functions over a simplicial complex
      • this makes a functions argument into a tuple of a cell AND a coordinate within that cell
      • ?? we might then add a coincides relation that relates these points of different cells that "are" the same point ??
      • ?? what about the interior of a set? it could be in the theory that the cell complex is defined as mapping only the interior of a cell ??
      • ?? how to define interior if it becomes necessary ??
    • allowing set operations only on cell-granulariy (e.g. cutting a complex, splitting a complex)

next up

  • space hierarchy
    • vector space = R-module
    • normed vector space = normed R-module (assumes norm)
      • needs a "normed ring" as a backing algebraic structure
    • banach space = complete normed vector space
    • inner product space = vector space + inner product (gives norm and metric)
      • use inner product R-modules instead
      • see discussion
    • hilbert space = complete inner product space
    • euclidean space = finite-dimensional inner product space over the real numbers
      • Q: how to define "finite-dimensional space" ?
        • A: demand a given basis
      • use inner-product-R-module-with-Basis
    • ℝⁿ as an instance of euclidean space
  • formalizing chapter 3 of Arnold's book
    • and "Box 2.1." on p. 19

.

  • structure (structure in brackets () can be defined in terms of other structure)
    • struct = basic algebraic structure to start out
      • Semiring = _+_ + _·_
      • Ring = _+_ + _·_ + -_
      • Field = _+_ + _·_ + -_ + _⁻¹
    • apart = assume an apartness relation
    • abs = assume an absolute value function
    • order = assume an order (linear or partial)
    • cauchy = assume limits of sequence-modulus pairs (from a sequence-modulus pair (x, M), we can compute a limit of x.)
    • sqrt₀⁺ = assume a square root function on nonnegative numbers
    • exp = assume an exponential function
name struct apart abs order cauchy sqrt₀⁺ exp final name
ℕ Semiring (✓) (✓) lin. (on x²) LinearlyOrderedSemiring
ℤ Ring (✓) (✓) lin. (on x²) LinearlyOrderedRing
ℚ Field (✓) (✓) lin. (on x²) (✓) LinearlyOrderedField
ℝ Field (✓) (✓) part. ✓ ✓ (✓) CompletePartiallyOrderedFieldWithSqrt
ℂ euclidean 2-Product (✓) (✓) (✓) ? EuclideanTwoProductOfCompletePartiallyOrderedFieldWithSqrt
R Ring ✓ ✓ ? ApartnessRingWithAbs
G Group ✓ ✓ ? ApartnessGroupWithAbs
K Field ✓ ✓ ✓ ? CompleteApartnessFieldWithAbs
  • numbers
    • (Ordered ⇒ Apartness and WithAbs)
    • (order ⇒ (trichotomy ⇔ linear order))
    • (A Heyting field ... is essentially a field with an apartness relation)
      • A commutative ring is a Heyting field if ¬(0 ≡ 1), either a or 1 - a is invertible for every a, and each noninvertible element is zero.
      • The first two conditions say that the ring is local; the first and third conditions say that it is a field in the classical sense.
      • The apartness relation is defined by writing a # b if a - b is invertible.
      • This relation is often now written as a ≠ b with the warning that it is not equivalent to ¬(a ≡ b).
      • For example, the assumption ¬(a ≡ 0) is not generally sufficient to construct the inverse of a, but a ≠ 0 is.
    • (Crvenković 2013 - Semigroups with apartness)
    • d(q,r) = | q - r | = max (q - r) (r - q) = sqrt ((q - r) ²)
    • ℕ isa LinearlyOrderedSemiring (has sqrt on squares of nonnegative numbers)
    • ℤ isa LinearlyOrderedRing (has sqrt on squares of nonnegative numbers)
    • ℚ isa LinearlyOrderedField (has sqrt on squares of nonnegative numbers)
    • ℝ isa CompletePartiallyOrderedField (has sqrt on nonnegative numbers)
    • ℂ isa CompleteApartnessFieldWithAbs
    • ℂ isa EuclideanTwoProductOfCompletePartiallyOrderedField (with euclidean metric)
    • ℕ↪ℂ works on ApartnessSemiringWithAbs
    • ℤ↪ℂ works on ApartnessRingWithAbs
    • ℚ↪ℂ works on ApartnessFieldWithAbs
    • ℝ↪ℂ works on CompleteApartnessFieldWithAbs
  • spaces
    • basic algebraic (use standard library)
      • Semiring
      • Ring
      • Field
    • modules
      • R-module
      • G-module = R-module + R is also a Group
      • K-module = K-module + R is a complete field (ℝ or ℂ)
      • normed K-module = K-module + norm
    • spaces on-top of K-modules (over a complete field)
      • (inner product ⇒ euclidean metric)
      • vector space = K-module
      • finite-dimensional vector space = K-module + basis
      • normed vector space = K-module + norm
      • finite-dimensional normed vector space = K-module + norm + basis
      • complete normed vector space (banach) = K-module + norm + modulus of cauchy convergence
      • inner product space = K-module + inner product
      • complete inner product space (hilbert) = K-module + inner product + modulus of cauchy convergence
      • finite dimensional inner product space
    • other spaces
      • metric space = set + metric
      • affine space = set + vector space + free action of the additive group of the vector space on the set

.

  • notions
    • ε-δ-continuity
    • cauchy convergence
    • cauchy completeness = Σ-limit (we can pick a limit)
      • is not only a property, but comes with a structure: modulus of cauchy convergence
    • limit of a cauchy sequence
    • compact = cauchy complete + totally bounded
    • closed (subset) = closed under limits (contains its limits)

.

  • structure (structure in brackets () can be defined in terms of other structure)
    • (metric ⇒ notion of ε-δ-continuity)
    • (notion of continuity ⇒)
    • carrier = type that isSet
    • module = which module to use over the carrier
    • metric = assume a metric
    • norm = assume a norm
    • inner = assume an inner product
    • basis = assume a finite dimensional basis
    • cauchy = assume limits of sequence-modulus pairs (from a sequence-modulus pair (x, M), we can compute a limit of x.)
name carrier module metric norm inner basis cauchy
VectorSpace any K
FiniteDimVectorSpace any K ✓
NormedVectorSpace any K (✓) ✓
FiniteDimNormedVectorSpace any K (✓) ✓ ✓
CompleteNormedVectorSpace any K (✓) ✓ ✓
FiniteDimCompleteNormedVectorSpace any K (✓) ✓ ✓ ✓
InnerProductSpace any K (✓) (✓) ✓
FiniteDimInnerProductSpace any K (✓) (✓) ✓ ✓
CompleteInnerProductSpace any K (✓) (✓) ✓ ✓
FiniteDimCompleteInnerProductSpace any K (✓) (✓) ✓ ✓ ✓
FiniteDimCompleteInnerProductSpaceOverℝ ℝ ℝ (✓) (✓) ✓ ✓ ✓
  • EuclideanSpace = FiniteDimCompleteInnerProductSpaceOverℝ
  • BanachSpace = CompleteNormedVectorSpace
  • FiniteDimBanachSpace = FiniteDimCompleteNormedVectorSpace
  • HilbertSpace = CompleteInnerProductSpace
  • FiniteDimHilbertSpace = FiniteDimCompleteInnerProductSpace

.

  • Isabelle's (abs_le_iff) means that abs is defined as max(x, -x)
  • replace ≤ with < for constructive assumption
  • take [Booij 2020] definition of metric space
  • there is an article about (archimedean) absolute value functions on the nLab
    • we cannot constructively prove that (| x | ≡ x) ∨ (| x | ≡ - x)
    • we have x # 0 → 0 < x ⨄ x < 0, so maybe we have x # 0 → (| x | ≡ x) ∨ (| x | ≡ - x)
    • tightness of # gives ¬(x # 0) → x ≡ 0
    • ?? we do not have (x # 0) ⨄ ¬(x # 0) i.e. apartness is not decidable ??
      • that might be why x # 0 is a "strong" property already
      • Ruitenburg 1991 - Inequality in Constructive Mathematics writes:
        • There are different versions of constructive inequality that only in classical mathematics are equal to the one standard inequality.
        • Examples are: denial inequality, where x ≠ y if and only if it is not true that x = y that is, ¬(x = y);
        • and tight apartness, whose axiomatization we will present later on.
        • The natural inequality on the set of real numbers R, defined by r ≠ s if and only | r - s | > 1 / n for some natural number n, is a tight apartness.
        • Tight apartness and denial inequality are independent; a tight apartness need not be a denial inequality, a denial inequality need not be a tight apartness.
      • Ciaffaglione - A Tour with Constructive Real Numbers
        • "the apartness relation (#) [...] is a semi-decidable version of the inequality (≠) [...] it is definable in terms of the order relation"
      • and I found this Github discussion
        • equality is not decidable on the real numbers [so I guess apartness then is also not decidable]
        • univalent foundations are a "non-setoid approach"
        • "to compute digit expansions requires deciding an inequality (in the above example, to decide x<1), which cannot be done for arbitrary reals" (the example was 3/3 being 1.000... or 0.999...)
        • "if you can decide inequalities, you can decide equalities (modulo getting the exact statement of this claim right)"
        • "One solution is to work instead with signed digit expansions, as is often done in computable and constructive analysis"
        • "In signed digit expansions, the digits of the (decimal, say) digit expansion range from -9 to +9, rather than from 0 to +9."
        • "if x<y is decidable for all x,y, then apartness is decidable, which iin particular implies that equality is decidable (since the negation of apartness is equality, and apartness implies the negation of equality)"
          • so I guess that none of _<_, _#_ and _≡_ are decidable then
          • that's (for me) some intuitive heuristic for what properties we have and what we do not have on ℝ
          • the only "sources" of inhabitants of _<_, _#_ and _≡_ are
            • 0ʳ, 1ʳ and everything we can make out of them (which amounts to ℕ, ℤ and ℚ)
            • and sqrt
  • there is an article about archimedean valued fields on the nLab
  • there is an article about square roots on the nLab
    • what about abs x = max x (- x) = sqrt (x · x) ?
  • for rings (ℤ), there seems to be a hierarchy
    • rngs
    • ⊃ rings
    • ⊃ commutative rings
    • ⊃ integral domains
    • ⊃ integrally closed domains
    • ⊃ GCD domains
    • ⊃ unique factorization domains
    • ⊃ principal ideal domains
    • ⊃ Euclidean domains
    • ⊃ fields
    • ⊃ algebraically closed fields
  • A rig is a ring ‘without negatives'
  • The term "rng" (pronounced rung) is meant to suggest that it is a "ring" without "i", i.e. without the requirement for an "identity element".

Pathes (PathP, Path, _≡_), Identity (Id), two kinds of Equivalences (_≃_) and Isomorphisms (Iso)

  • there is an article about Cubical Agda by Anders Mörtberg
    • it seems that the identity type Id is not yet "ready" for pattern matching (WIP) but its "purpose" is to make "pattern-matching" possible (I guess)
    • "Note that the cubical identity types are not an inductive family like in HoTT which means that we cannot use Agda’s pattern-matching to match on them. Furthermore Cubical Agda doesn’t support inductive families yet, but it should be possible to adapt the techniques of Cavallo/Harper presented in [...] in order to extend it with inductive families. The traditional identity types could then be defined as in HoTT and pattern-matching should work as expected."
    • Proper support for inductive families in Cubical Agda #3733
      • Jesper Cockx writes papers about pattern matching "the theory of pattern matching in my papers does not support recursion on dot patterns"
    • there is not a single use of rewrite in the --cubical standard library ... why?
      • find ~/agda/cubical/ -iname "*.agda" -exec grep --color=always -A 1 -Hni "rewrite" {} \;
      • "(N.B.: Agda’s rewrite keyword should not be confused with rewrite rules, which are added by a REWRITE pragma.)"
  • these four notions are binary "operations" on types that come in constant / homogeneous variants and depenedent / heterogeneous variants
    • "The central notion of equality in Cubical Agda is hence heterogeneous equality (in the sense of PathOver in HoTT)." (see manual)
    • heterogeneous equality is already available in non-cubical agda
notion homogeneous heterogeneous Agda module
PathP _≡_ {A = A} = PathP (λ i → A) postulate PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ Agda.Builtin.Cubical.Path
Identity postulate Id : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ Agda.Builtin.Cubical.Id
Equivalence1 A ≃ B = Σ[ f ∈ (A → B) ] isEquiv f⁽¹⁾ Agda.Builtin.Cubical.Glue
Isomorphism Iso = f + f⁻¹ + (section f f⁻¹) + (retraction f f⁻¹) Cubical.Foundations.Isomorphism
Equivalence2 A ≃ B = Σ[ f ∈ (A → B) ] isEquiv f Cubical.Foundations.Id
  • ⁽¹⁾ Σ-syntax is not yet defined in (Agda.Builtin.Cubical.Glue) therefore this is really the unsugared version
    • also it seems that all (Agda.Builtin.*) modules still work on Set instead of Type (which is just a renamed Set from (Agda.Primitive))
  • (Cubical.Core.Primitives) defines Path A a b = PathP (λ _ → A) a b which is almost _≡_ from (Agda.Builtin.Cubical.Path)
  • pathes cannot cross universes (therefore we need to Lift one side to the other) but _⇔_ on hProps can (i.e. it can operate on two different universes)
    • it seems that _⇔_ might be the "preferred" / "most performant" / "least cluttered" way to "store" a path when hProps are available
      • ⇔toPath results in a very long normal form and terms/clauses using it can be made abstract
  • there are explanations of transp given by Thorsten Altenkirch, John Leo and Andreas Mörtberg as an answer to an email "Question about transport and cubical" (03.09.20, 19:51) by Manuel Bärenz on the agda mailing list
  • there is a short 2011 blogpost of Mike Shulman "An Interval Type Implies Function Extensionality"

.

  • there is also "definitional equality" of "canonical terms" (normalized terms)
    • and there is "definitional equality" of non-normalized / un-normalizable terms to some degree
    • "the purpose of rewrite rules [is] [...] to allow the user of the language to extend the language’s notion of definitional equality with additional computation rules." (see blogpost)
    • "[...] given a proof (or a postulate) p : ∀ x₁ ... xₙ → f u₁ ... uₙ ≡ v, you can register it as a rewrite rule with a pragma {-# REWRITE p #-}"
    • "From this point on, Agda will automatically reduce instances of the left-hand side f u₁ ... uₙ (i.e. for specific values of x₁ ... xₙ) to the corresponding instance of v. "
    • rewrite rules do not break soundness, but may break "confluence of reduction" or "type preservation"
    • "The idea of extending existing functions with new computation rules [...] [allows to] add new computation rules to classic functions on lists such as map, _++_, and fold. In Agda, we can prove these rules and then add them as rewrite rules"
    • "One of the well-known weak spots of intentional type theory is the poor handling of quotient types."
    • "One of the more promising attempts at adding quotients to Agda is by Guillaume Brunerie in the initiality project, which uses a combination of rewrite rules and Agda’s new (strict) Prop universe"
    • "type constructors that compute according to the type they are applied to [...] is the core concept of observational type theory (OTT)"
    • extending definitional equality seems to be the source for very powerful mechanism
    • cites: Sterling 2019 - Cubical Syntax for Reflection-Free Extensional Equality
    • "To be able to actually reason about equality, OTT also has two more notions: coercion and cohesion. Coercion allows us to cast an element from one type to the other when we know both types are equal, and cohesion allows us to prove that coercion is computationally a no-op."
  • notions of equality come with eliminators, but to some extent we have pattern matching for non-cubical refl
    • do we have a similar thing in cubical agda?
  • Pathes and Id are somehow builtin, where Isomorphisms and Equivalences are defined on-top
    • are they all isProp?
    • PathP (λ i → A) x y gets printed as x ≡ y when A does not mention i (Cubical.Core.Primitives)
    • postulate Id : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ (Agda.Builtin.Cubical.Id)
    • A ≃ B = Σ[ f ∈ (A → B) ] isEquiv f (a function and an equivalence-proof of it) (Cubical.Foundations.Id)
      • both, (Agda.Builtin.Cubical.Glue) and (Cubical.Foundations.Id) define _≃_, (but in a definitionally equal way ?)
        • (Cubical.Foundations.Id) is "on-top" of (Cubical.Foundations.Equiv)
        • this might be for better Have/Goal normalization (?)
        • _≃_ from (Cubical.Foundations.Equiv) is called EquivPath in (Cubical.Foundations.Id)
      • isEquiv f = ∀ y → isContr (fiber f y) (all fibers are contractible) (Cubical.Foundations.Id)
      • isContr A = Σ[ x ∈ A ] ∀ y → x ≡ y (there exists a point that is equal to all other points) (Cubical.Foundations.Id)
      • fiber {A = A} f y = Σ[ x ∈ A ] f x ≡ y (the "fiber over y" is the "inverse image of a singleton {y}" (because "inverse image" is defined also for non-singleton sets)) (Cubical.Foundations.Id)
    • Iso = f + f⁻¹ + (section f f⁻¹) + (retraction f f⁻¹) (f is a section and f⁻¹ is a retraction) (Cubical.Foundations.Isomorphism)
      • section f f⁻¹ = ∀ b → f (f⁻¹ b) ≡ b (f is a section of f⁻¹) (Cubical.Foundations.Isomorphism)
      • retract f f⁻¹ = ∀ a → f⁻¹ (f a) ≡ a (f⁻¹ is a retraction of f) (Cubical.Foundations.Isomorphism)
  • one can convert all (?) of them into each other
    • isoToEquiv : Iso A B → A ≃ B (Cubical.Foundations.Isomorphism)
    • equivToIso : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → A ≃ B → Iso A B (Cubical.Foundations.Equiv)
    • isoToPath : Iso A B → A ≡ B (Cubical.Foundations.Isomorphism)
    • pathToIso : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → Iso A B (Cubical.Foundations.Transport)
    • pathToEquiv : {ℓ : I → Level} (P : (i : I) → Set (ℓ i)) → A ≃ B (Cubical.Foundations.Isomorphism)
    • transportEquiv : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → A ≃ B (Cubical.Foundations.Transport)
    • ua : ∀ {A B : Type ℓ} → A ≃ B → A ≡ B (Cubical.Foundations.Univalence)
    • idToPath : ∀ {x y : A} → Id x y → Path _ x y (Cubical.Foundations.Id)
    • pathToId : ∀ {x y : A} → Path _ x y → Id x y (Cubical.Foundations.Id)
    • logic
      • ⇔toPath : [ P ⇒ Q ] → [ Q ⇒ P ] → P ≡ Q (Cubical.Foundations.Logic)
      • pathTo⇒ : P ≡ Q → [ P ⇒ Q ] (Cubical.Foundations.Logic)
      • pathTo⇐ : P ≡ Q → [ Q ⇒ P ] (Cubical.Foundations.Logic)
      • [ P ] ≡ [ Q ] → [ P ⇒ Q ] is "just" transport
      • propositional extensionality
        • prop≃ : isProp A → isProp B → (A → B) → (B → A) → A ≃ B
        • prop≃ pA pB f g = isoToEquiv (iso f g (λ _ → pB _ _) (λ _ → pA _ _))
  • Univalence
    • path≡Id : ∀ {ℓ} {A B : Type ℓ} → Path _ (Path _ A B) (Id A B) (Cubical.Foundations.Id)
    • equivPath≡Equiv : ∀ {ℓ} {A B : Type ℓ} → Path _ (EquivPath A B) (A ≃ B) (Cubical.Foundations.Id)
    • univalenceId : ∀ {ℓ} {A B : Type ℓ} → (A ≡ B) ≃ (A ≃ B) (Cubical.Foundations.Id)

Angiuli, Cavallo, Mörtberg, Zeuner 2020 - Internalizing Representation Independence with Univalence

isEquiv f is always a proposition (by isPropΠ and the fact that isContr is a proposition), and thus two elements of A ≃ B are equal if and only if their underlying functions are equal (because their isEquiv proofs must agree). In contrast, the property of a function f : A → B being an isomorphism (i.e., the triple of a function B → A and proofs that it is left and right inverse to f ) is not a proposition [Univalent Foundations Program 2013, Theorem 4.1.3]. A subtle consequence of this fact is that if one replaces ≃ in the statement of univalence with Iso, the resulting statement is actually inconsistent

"Performance"

Disclaimer: Performance claims always need to be accompanied by (runtime-)measurements and not be based on pure speculation. Since I do not know much about how Agda works internally, the following speculations should be taken with a grain of salt. The current, very dangerous, metric is "term-length": i.e. reducing the length of normalized terms. This can be achieved with the use of abstract to block unfolding of terms (unless this blocking causes to block another, more efficient, unfolding which would reduce the term length) or by keeping the terms short already in the first place. Therefore, since pathes, equivalences and isomorphisms provide basically the same "mechanism" (i.e. to use them for substitutions), the question arises which one might be the "simplest" in terms of "normalized term-length".

NOTE: there is an email from Guillaume Brunerie "Re: [Agda] Identifying inefficiency" (26.03.19, 16:01) on the agda mailing list, elaborating how to do performance "measurements"

You can turn on interactive highlighting (setting the variable "agda2-highlight-level" to "interactive"), and then when loading a file in emacs you can see where the highlighting gets "stuck".

Another option is to run agda from the command line with the options "-v profile:7 ", and you will get a breakdown of which part of Agda took a long time (e.g. LHS checking, positivity, termination checking, and so on), which might help to identify different sources of inefficiency.

The comment of Wolfram Kahl on issue 1625 has an attached log which shows agda's command line arguments and its corresponding output

$ rm $(agdai)
$ time agda --sharing -v profile:7 +RTS -S -K256M -H11G -M11G -A1G -RTS -i . -i $(agdalib) Data/SUList/ListSetMap/FinRel/NatSumProps.lagda

there is

Use copattern-matching when instantiating records for efficiency. This seems especially important when constructing Iso's.

in Agda.Builtin.Cubical.Glue it is written that copatterns don't get unfolded unless a projection is applied

pathTo⇒ p x = subst fst  p x
pathTo⇐ p x = subst fst (sym p) x

subst B p pa = transport (λ i → B (p i)) pa

⇒∶_⇐∶_ = ⇔toPath

-- NOTE: this is also what I often do `hProp≡ (isoToPath (iso ...))`
⇔toPath {P = P} {Q = Q} P⇒Q Q⇒P =
  hProp≡ (isoToPath (iso P⇒Q Q⇒P (λ b → isProp[] Q (P⇒Q (Q⇒P b)) b) λ a → isProp[] P (Q⇒P (P⇒Q a)) a))

hProp≡ p = Σ≡Prop (\ _ → isPropIsProp) p

isPropΣ : isProp A → ((x : A) → isProp (B x)) → isProp (Σ A B)
isPropΣ pA pB t u = Σ≡Prop pB (pA (t .fst) (u .fst))

Σ≡Prop : ((x : A) → isProp (B x)) → {u v : Σ A B} → (p : u .fst ≡ v .fst) → u ≡ v
Σ≡Prop pB {u} {v} p i = (p i) , isProp→PathP (λ i → pB (p i)) (u .snd) (v .snd) i

isProp→PathP : ∀ {B : I → Type ℓ} → ((i : I) → isProp (B i))
               → (b0 : B i0) (b1 : B i1)
               → PathP (λ i → B i) b0 b1
isProp→PathP hB b0 b1 = toPathP (hB _ _ _)

toPathP : transp A i0 x ≡ y → PathP A x y
toPathP p i = hcomp
              (λ j → λ { (i = i0) → x ; (i = i1) → p j })
              (transp (λ j → A (i ∧ j)) (~ i) x)

fromPathP : PathP A x y → transp A i0 x ≡ y
fromPathP p i = transp (λ j → A (i ∨ j)) i (p i)

transp = primTransp
hcomp  = primHComp

primitive primTransp : ∀ {ℓ} (A : (i : I) → Set (ℓ i)) (φ : I) (a : A i0) → A i1
primitive primHComp  : ∀ {ℓ} {A : Set ℓ} {φ : I} (u : ∀ i → Partial φ A) (a : A) → A

isoToPath : Iso A B → A ≡ B
isoToPath {A = A} {B = B} f i =
  Glue B (λ { (i = i0) → (A , isoToEquiv f)
            ; (i = i1) → (B , idEquiv B) })

Glue : (A : Type ℓ) {φ : I}
       → (Te : Partial φ (Σ[ T ∈ Type ℓ' ] T ≃ A))
       → Type ℓ'
Glue A Te = primGlue A (λ x → Te x .fst) (λ x → Te x .snd)

primitive primGlue : ∀ {ℓ ℓ'} (A : Set ℓ) {φ : I}
            → (T : Partial φ (Set ℓ')) → (e : PartialP φ (λ o → T o ≃ A))
            → Set ℓ'

A ≃ B = Σ (A → B) λ f → (isEquiv f)

record isEquiv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) : Set (ℓ ⊔ ℓ') where
  no-eta-equality
  field
    equiv-proof : (y : B) → isContr (fiber f y)
open isEquiv public

isoToEquiv : Iso A B → A ≃ B
isoToEquiv i .fst = _
isoToEquiv i .snd = isoToIsEquiv i

-- NOTE: this makes mixed use of patterns and copatterns (see NOTES.md for an example)
isoToIsEquiv : isEquiv f
isoToIsEquiv .equiv-proof y .fst .fst = g y
isoToIsEquiv .equiv-proof y .fst .snd = s y
isoToIsEquiv .equiv-proof y .snd z = lemIso y (g y) (fst z) (s y) (snd z)

-- this is equivalent to
isoToIsEquiv : isEquiv f
(fst (fst ((equiv-proof isoToIsEquiv) y))   ) = g y
(snd (fst ((equiv-proof isoToIsEquiv) y))   ) = s y
(    (snd ((equiv-proof isoToIsEquiv) y)) z ) = lemIso y (g y) (fst z) (s y) (snd z)

isPropIsProp : isProp (isProp A)
isPropIsProp f g i a b = isProp→isSet f a b (f a b) (g a b) i

isProp→isSet : isProp A → isSet A
isProp→isSet h a b p q j i =
  hcomp (λ k → λ { (i = i0) → h a a k
                 ; (i = i1) → h a b k
                 ; (j = i0) → h a (p i) k
                 ; (j = i1) → h a (q i) k }) a

Maybe we can make a similar use copatterns to split our formulation of algebraic properties and proofs in MorePropAlgebra and this already helps to eliminate parts in long normalizations of some terms (see NOTES.md → 'example of "cluttered" normalized term').

isPropΣ might be a source of "long" normal forms, because it does expand to a lot of unreducible primitives

λ pA pB t u i →
  ( pA (t .fst) (u .fst) i
  , hcomp
      (λ { j (i = i0) → t .snd
         ; j (i = i1) → pB (u .fst) (transp (λ z → z₁ (pA (t .fst) (u .fst) z)) i0 (t .snd)) (u .snd) j
      }  )
      (transp (λ j → z₁ (pA (t .fst) (u .fst) (i ∧ j))) (~ i) (t .snd))
  )

Well, I think that ⇔toPath is the reason for my long normalized terms, so it might be a good idea to make everything using it abstract by default. ⇔toPath expands into a very long normal form (originally 207 lines) of the following shape:

λ {P = P₁} {Q} P⇒Q Q⇒P i →
  ( Agda.Builtin.Cubical.Glue.primGlue (fst Q)                                                 -- this seems to be
    (λ .x₁ → (λ { (i = i0) → fst P₁ , isoToEquiv ? ; (i = i1) → fst Q , idEquiv ? } ) _ .fst ) -- `isoToPath`
    (λ .x₁ → (λ { (i = i0) → fst P₁ , isoToEquiv ? ; (i = i1) → fst Q , idEquiv ? } ) _ .snd ) --
  , hcomp -- this is from `toPathP`
    (λ { j (i = i0) → P₁ .snd         -- this is `isPropIsProp`
       ; j (i = i1) → λ a b i₁ →      --
           hcomp (λ { k (i₁ = i0) → ? -- it is the first argument of `toPathP`
                    ; k (i₁ = i1) → ? -- because it is the first argument of `isProp→PathP`
                    ; k (j  = i0) → ? -- because it is the first argument of `Σ≡Prop`
                    ; k (j  = i1) → ? -- which is applied in the following way:
                    }                 --   `hProp≡ p = Σ≡Prop (\ _ → isPropIsProp) p`
                 ) a                  --
       })                             --
    (transp (λ j → (x₁ y₁ : Agda.Builtin.Cubical.Glue.primGlue (fst Q)
                            (λ .x₂ → (λ { ((i ∧ j) = i0) → fst P₁ , isoToEquiv ? ; ((i ∧ j) = i1) → fst Q , idEquiv ? } ) _ .fst)
                            (λ .x₂ → (λ { ((i ∧ j) = i0) → fst P₁ , isoToEquiv ? ; ((i ∧ j) = i1) → fst Q , idEquiv ? } ) _ .snd)
                    ) → x₁ ≡ y₁)
     (~ i) (P₁ .snd)
    )
  )

in its full (but reformatted) form this becomes

λ {P = P₁} {Q} P⇒Q Q⇒P i →
  Agda.Builtin.Cubical.Glue.primGlue (fst Q)
  (λ .x₁ → (λ { (i = i0) → fst P₁ , isoToEquiv (iso P⇒Q Q⇒P (λ b → snd Q (P⇒Q (Q⇒P b)) b) (λ a → snd P₁ (Q⇒P (P⇒Q a)) a))
              ; (i = i1) → fst Q , idEquiv (fst Q)
              }
           ) _ .fst
  )
  (λ .x₁ → (λ { (i = i0) → fst P₁ , isoToEquiv (iso P⇒Q Q⇒P (λ b → snd Q (P⇒Q (Q⇒P b)) b) (λ a → snd P₁ (Q⇒P (P⇒Q a)) a))
              ; (i = i1) → fst Q , idEquiv (fst Q)
              }
           ) _ .snd
  )
  ,
  hcomp
  (λ { j (i = i0) → P₁ .snd
     ; j (i = i1) → λ a b i₁ → hcomp
             (λ { k (i₁ = i0) → transp
                    (λ z →
                      (x₁ y₁ : Agda.Builtin.Cubical.Glue.primGlue (fst Q)
                               (λ .x₂ → (λ { (z = i0) → fst P₁ , isoToEquiv (iso P⇒Q Q⇒P (λ b₁ → snd Q (P⇒Q (Q⇒P b₁)) b₁) (λ a₁ → snd P₁ (Q⇒P (P⇒Q a₁)) a₁))
                                           ; (z = i1) → fst Q , idEquiv (fst Q)
                                           }
                                        ) _ .fst)
                               (λ .x₂ → (λ { (z = i0) → fst P₁ , isoToEquiv (iso P⇒Q Q⇒P (λ b₁ → snd Q (P⇒Q (Q⇒P b₁)) b₁) (λ a₁ → snd P₁ (Q⇒P (P⇒Q a₁)) a₁))
                                           ; (z = i1) → fst Q , idEquiv (fst Q)
                                           }
                                        ) _ .snd)
                      ) → x₁ ≡ y₁
                    ) i0 (P₁ .snd) a a k
                ; k (i₁ = i1) → transp
                      (λ z → (x₁ y₁ : Agda.Builtin.Cubical.Glue.primGlue (fst Q)
                                      (λ .x₂ → (λ { (z = i0) → fst P₁ , isoToEquiv (iso P⇒Q Q⇒P (λ b₁ → snd Q (P⇒Q (Q⇒P b₁)) b₁) (λ a₁ → snd P₁ (Q⇒P (P⇒Q a₁)) a₁))
                                                  ; (z = i1) → fst Q , idEquiv (fst Q)
                                                  }
                                               ) _ .fst)
                                      (λ .x₂ → (λ { (z = i0) → fst P₁ , isoToEquiv (iso P⇒Q Q⇒P (λ b₁ → snd Q (P⇒Q (Q⇒P b₁)) b₁) (λ a₁ → snd P₁ (Q⇒P (P⇒Q a₁)) a₁))
                                                  ; (z = i1) → fst Q , idEquiv (fst Q)
                                                  }
                                               ) _ .snd)
                              ) → x₁ ≡ y₁)
                      i0 (P₁ .snd) a b k
                ; k (j = i0) → transp
                      (λ z → (x₁ y₁ : Agda.Builtin.Cubical.Glue.primGlue (fst Q)
                                      (λ .x₂ → (λ { (z = i0) → fst P₁ , isoToEquiv (iso P⇒Q Q⇒P (λ b₁ → snd Q (P⇒Q (Q⇒P b₁)) b₁) (λ a₁ → snd P₁ (Q⇒P (P⇒Q a₁)) a₁))
                                                  ; (z = i1) → fst Q , idEquiv (fst Q)
                                                  }
                                               ) _ .fst)
                                      (λ .x₂ → (λ { (z = i0) → fst P₁ , isoToEquiv (iso P⇒Q Q⇒P (λ b₁ → snd Q (P⇒Q (Q⇒P b₁)) b₁) (λ a₁ → snd P₁ (Q⇒P (P⇒Q a₁)) a₁))
                                                  ; (z = i1) → fst Q , idEquiv (fst Q)
                                                  }
                                               ) _ .snd)
                              ) → x₁ ≡ y₁
                       ) i0 (P₁ .snd) a
                      (transp
                       (λ i₂ →
                          transp
                          (λ j₁ →
                             Agda.Builtin.Cubical.Glue.primGlue (fst Q)
                             (λ .x₁ → (λ { ((i₂ ∨ ~ j₁) = i0) → fst P₁ , isoToEquiv (iso P⇒Q Q⇒P (λ b₁ → snd Q (P⇒Q (Q⇒P b₁)) b₁) (λ a₁ → snd P₁ (Q⇒P (P⇒Q a₁)) a₁))
                                         ; ((i₂ ∨ ~ j₁) = i1) → fst Q , idEquiv (fst Q)
                                         }
                                       ) _ .fst)
                             (λ .x₁ → (λ { ((i₂ ∨ ~ j₁) = i0) → fst P₁ , isoToEquiv (iso P⇒Q Q⇒P (λ b₁ → snd Q (P⇒Q (Q⇒P b₁)) b₁) (λ a₁ → snd P₁ (Q⇒P (P⇒Q a₁)) a₁))
                                         ; ((i₂ ∨ ~ j₁) = i1) → fst Q , idEquiv (fst Q)
                                         }
                                       ) _ .snd))
                          i₂ a
                          ≡
                          transp
                          (λ j₁ →
                             Agda.Builtin.Cubical.Glue.primGlue (fst Q)
                             (λ .x₁ → (λ { ((i₂ ∨ ~ j₁) = i0) → fst P₁ , isoToEquiv (iso P⇒Q Q⇒P (λ b₁ → snd Q (P⇒Q (Q⇒P b₁)) b₁) (λ a₁ → snd P₁ (Q⇒P (P⇒Q a₁)) a₁))
                                         ; ((i₂ ∨ ~ j₁) = i1) → fst Q , idEquiv (fst Q)
                                         }
                                       ) _ .fst)
                             (λ .x₁ → (λ { ((i₂ ∨ ~ j₁) = i0) → fst P₁ , isoToEquiv (iso P⇒Q Q⇒P (λ b₁ → snd Q (P⇒Q (Q⇒P b₁)) b₁) (λ a₁ → snd P₁ (Q⇒P (P⇒Q a₁)) a₁))
                                         ; ((i₂ ∨ ~ j₁) = i1) → fst Q , idEquiv (fst Q)
                                         }
                                       ) _ .snd))
                          i₂ b)
                       i0
                       (P₁ .snd (Q⇒P (transp (λ i₂ → fst Q) i0 a))
                        (Q⇒P (transp (λ i₂ → fst Q) i0 b)))
                       i₁)
                      k
                ; k (j = i1) → transp
                      (λ z → (x₁ y₁ : Agda.Builtin.Cubical.Glue.primGlue (fst Q)
                                      (λ .x₂ → (λ { (z = i0) → fst P₁ , isoToEquiv (iso P⇒Q Q⇒P (λ b₁ → snd Q (P⇒Q (Q⇒P b₁)) b₁) (λ a₁ → snd P₁ (Q⇒P (P⇒Q a₁)) a₁))
                                                  ; (z = i1) → fst Q , idEquiv (fst Q)
                                                  }
                                               ) _ .fst)
                                      (λ .x₂ → (λ { (z = i0) → fst P₁ , isoToEquiv (iso P⇒Q Q⇒P (λ b₁ → snd Q (P⇒Q (Q⇒P b₁)) b₁) (λ a₁ → snd P₁ (Q⇒P (P⇒Q a₁)) a₁))
                                                  ; (z = i1) → fst Q , idEquiv (fst Q)
                                                  }
                                               ) _ .snd)
                              ) → x₁ ≡ y₁
                       ) i0 (P₁ .snd) a (Q .snd a b i₁) k
                })
             a
     })
  (transp (λ j → (x₁ y₁ : Agda.Builtin.Cubical.Glue.primGlue (fst Q)
                          (λ .x₂ → (λ { ((i ∧ j) = i0) → fst P₁ , isoToEquiv (iso P⇒Q Q⇒P (λ b → snd Q (P⇒Q (Q⇒P b)) b) (λ a → snd P₁ (Q⇒P (P⇒Q a)) a))
                                      ; ((i ∧ j) = i1) → fst Q , idEquiv (fst Q)
                                      }
                                   ) _ .fst)
                          (λ .x₂ → (λ { ((i ∧ j) = i0) → fst P₁ , isoToEquiv (iso P⇒Q Q⇒P (λ b → snd Q (P⇒Q (Q⇒P b)) b) (λ a → snd P₁ (Q⇒P (P⇒Q a)) a))
                                      ; ((i ∧ j) = i1) → fst Q , idEquiv (fst Q)
                                      }
                                   ) _ .snd)
                  ) → x₁ ≡ y₁)
   (~ i)
   (P₁ .snd)
   )