text:
{-# OPTIONS --cubical --no-import-sorts #-}

module Number.Instances.QuoQ.Instance where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)
open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Foundations.Logic renaming (inl to inlᵖ; inr to inrᵖ)

open import Cubical.Relation.Nullary.Base renaming (¬_ to ¬ᵗ_)
open import Cubical.Relation.Binary.Base
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Sigma
open import Cubical.Data.Bool as Bool using (Bool; not; true; false)
open import Cubical.Data.Empty renaming (elim to ⊥-elim; ⊥ to ⊥⊥) -- `⊥` and `elim`
open import Cubical.Foundations.Logic renaming (¬_ to ¬ᵖ_; inl to inlᵖ; inr to inrᵖ)
open import Function.Base using (it; _∋_; _$_)
open import Cubical.Foundations.Isomorphism

open import Cubical.HITs.PropositionalTruncation renaming (elim to ∣∣-elim)

open import Utils using (!_; !!_)
open import MoreLogic.Reasoning
open import MoreLogic.Definitions
open import MoreLogic.Properties
open import MorePropAlgebra.Definitions hiding (_≤''_)
open import MorePropAlgebra.Structures
open import MorePropAlgebra.Bundles
open import MorePropAlgebra.Consequences
open import Number.Structures2
open import Number.Bundles2

open import Cubical.Data.NatPlusOne using (HasFromNat; 1+_; ℕ₊₁; ℕ₊₁→ℕ) renaming
  ( _*₊₁_         to _·₊₁_
  ; *₊₁-comm      to ·₊₁-comm
  ; *₊₁-assoc     to ·₊₁-assoc
  ; *₊₁-identityˡ to ·₊₁-identityˡ
  ; *₊₁-identityʳ to ·₊₁-identityʳ
  )
open import Cubical.HITs.SetQuotients as SetQuotient using () renaming (_/_ to _//_)

open import Cubical.Data.Nat.Literals
open import Cubical.Data.Bool
open import Number.Prelude.Nat
open import Number.Prelude.QuoInt
open import Cubical.HITs.Ints.QuoInt using (HasFromNat)
open import Number.Instances.QuoQ.Definitions
open import Cubical.HITs.Rationals.QuoQ using
  ( ℚ
  ; HasFromNat
  ; isSetℚ
  ; onCommonDenom
  ; onCommonDenomSym
  ; eq/
  ; eq/⁻¹
  ; _//_
  ; _∼_
  ; [_/_]
  ) renaming
  ( [_] to [_]ᶠ
  ; ℕ₊₁→ℤ to [1+_ⁿ]ᶻ
  ; _*_ to _·_
  ; *-comm to ·-comm
  ; *-assoc to ·-assoc
  )

{-# DISPLAY [_/_] (pos 1) (1+ 0) = 1 #-}
{-# DISPLAY [_/_] (pos 0) (1+ 0) = 0 #-}

private
  ·ᶻ-commʳ : ∀ a b c → (a ·ᶻ b) ·ᶻ c ≡ (a ·ᶻ c) ·ᶻ b
  ·ᶻ-commʳ a b c = (a ·ᶻ  b) ·ᶻ c  ≡⟨ sym $ ·ᶻ-assoc a b c ⟩
                    a ·ᶻ (b  ·ᶻ c) ≡⟨ (λ i → a ·ᶻ ·ᶻ-comm b c i) ⟩
                    a ·ᶻ (c  ·ᶻ b) ≡⟨ ·ᶻ-assoc a c b ⟩
                   (a ·ᶻ  c) ·ᶻ b  ∎

  ·ᶻ-commˡ : ∀ a b c → a ·ᶻ (b ·ᶻ c) ≡ b ·ᶻ (a ·ᶻ c)
  ·ᶻ-commˡ a b c = ·ᶻ-comm a (b ·ᶻ c) ∙ sym (·ᶻ-commʳ b a c) ∙ sym (·ᶻ-assoc b a c)

  is-0<ⁿᶻ : ∀{aⁿ} → [ 0 <ᶻ [1+ aⁿ ⁿ]ᶻ ]
  is-0<ⁿᶻ {aⁿ} = ℕ₊₁.n aⁿ , +ⁿ-comm (ℕ₊₁.n aⁿ) 1

  is-0≤ⁿᶻ : ∀{aⁿ} → [ 0 ≤ᶻ [1+ aⁿ ⁿ]ᶻ ]
  is-0≤ⁿᶻ (k , p) = snotzⁿ $ sym (+ⁿ-suc k _) ∙ p

<-irrefl : ∀ a → [ ¬(a < a) ]
<-irrefl = SetQuotient.elimProp {R = _∼_} (λ a → isProp[] (¬(a < a))) γ where
  γ : (a : ℤ × ℕ₊₁) → [ ¬([ a ]ᶠ < [ a ]ᶠ) ]
  γ a@(aᶻ , aⁿ) = κ where
    aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
    κ : [ ¬((aᶻ ·ᶻ aⁿᶻ) <ᶻ (aᶻ ·ᶻ aⁿᶻ)) ]
    κ = <ᶻ-irrefl (aᶻ ·ᶻ aⁿᶻ)

<-trans : (a b c : ℚ) → [ a < b ] → [ b < c ] → [ a < c ]
<-trans = SetQuotient.elimProp3 {R = _∼_} (λ a b c → isProp[] ((a < b) ⇒ (b < c) ⇒ (a < c))) γ where
  γ : (a b c : ℤ × ℕ₊₁) → [ [ a ]ᶠ < [ b ]ᶠ ] → [ [ b ]ᶠ < [ c ]ᶠ ] → [ [ a ]ᶠ < [ c ]ᶠ ]
  γ a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) c@(cᶻ , cⁿ) = κ where
    aⁿᶻ   = [1+ aⁿ ⁿ]ᶻ
    bⁿᶻ   = [1+ bⁿ ⁿ]ᶻ
    cⁿᶻ   = [1+ cⁿ ⁿ]ᶻ
    0<aⁿᶻ = [ 0 <ᶻ aⁿᶻ ] ∋ is-0<ⁿᶻ
    0<bⁿᶻ = [ 0 <ᶻ bⁿᶻ ] ∋ is-0<ⁿᶻ
    0<cⁿᶻ = [ 0 <ᶻ cⁿᶻ ] ∋ is-0<ⁿᶻ
    κ : [ (aᶻ ·ᶻ bⁿᶻ) <ᶻ (bᶻ ·ᶻ aⁿᶻ) ] → [ (bᶻ ·ᶻ cⁿᶻ) <ᶻ (cᶻ ·ᶻ bⁿᶻ) ] → [ (aᶻ ·ᶻ cⁿᶻ) <ᶻ (cᶻ ·ᶻ aⁿᶻ) ]
    -- strategy: multiply with xⁿᶻ and then use <ᶻ-trans
    κ p₁ p₂ = ·ᶻ-reflects-<ᶻ (aᶻ ·ᶻ cⁿᶻ) (cᶻ ·ᶻ aⁿᶻ) bⁿᶻ 0<bⁿᶻ φ₃ where
      φ₁ = ( aᶻ ·ᶻ bⁿᶻ        <ᶻ bᶻ ·ᶻ aⁿᶻ        ⇒ᵖ⟨ ·ᶻ-preserves-<ᶻ (aᶻ ·ᶻ bⁿᶻ) (bᶻ ·ᶻ aⁿᶻ) cⁿᶻ 0<cⁿᶻ ⟩
             aᶻ ·ᶻ bⁿᶻ ·ᶻ cⁿᶻ <ᶻ bᶻ ·ᶻ aⁿᶻ ·ᶻ cⁿᶻ ⇒ᵖ⟨ transport (λ i → [ ·ᶻ-commʳ aᶻ bⁿᶻ cⁿᶻ i <ᶻ ·ᶻ-commʳ bᶻ aⁿᶻ cⁿᶻ i ]) ⟩
             aᶻ ·ᶻ cⁿᶻ ·ᶻ bⁿᶻ <ᶻ bᶻ ·ᶻ cⁿᶻ ·ᶻ aⁿᶻ ◼ᵖ) .snd p₁
      φ₂ = ( bᶻ ·ᶻ cⁿᶻ        <ᶻ cᶻ ·ᶻ bⁿᶻ        ⇒ᵖ⟨ ·ᶻ-preserves-<ᶻ (bᶻ ·ᶻ cⁿᶻ) (cᶻ ·ᶻ bⁿᶻ) aⁿᶻ 0<aⁿᶻ ⟩
             bᶻ ·ᶻ cⁿᶻ ·ᶻ aⁿᶻ <ᶻ cᶻ ·ᶻ bⁿᶻ ·ᶻ aⁿᶻ ⇒ᵖ⟨ transport (λ i → [ (bᶻ ·ᶻ cⁿᶻ ·ᶻ aⁿᶻ) <ᶻ ·ᶻ-commʳ cᶻ bⁿᶻ aⁿᶻ i ]) ⟩
             bᶻ ·ᶻ cⁿᶻ ·ᶻ aⁿᶻ <ᶻ cᶻ ·ᶻ aⁿᶻ ·ᶻ bⁿᶻ ◼ᵖ) .snd p₂
      φ₃ : [ aᶻ ·ᶻ cⁿᶻ ·ᶻ bⁿᶻ <ᶻ cᶻ ·ᶻ aⁿᶻ ·ᶻ bⁿᶻ ]
      φ₃ = <ᶻ-trans (aᶻ ·ᶻ cⁿᶻ ·ᶻ bⁿᶻ) (bᶻ ·ᶻ cⁿᶻ ·ᶻ aⁿᶻ) (cᶻ ·ᶻ aⁿᶻ ·ᶻ bⁿᶻ) φ₁ φ₂

<-asym : ∀ a b → [ a < b ] → [ ¬(b < a) ]
<-asym a b a<b b<a = <-irrefl a (<-trans a b a a<b b<a)

<-irrefl'' : ∀ a b → [ a < b ] ⊎ [ b < a ] → [ ¬(a ≡ₚ b) ]
<-irrefl'' a b (inl a<b) a≡b = <-irrefl b (substₚ (λ p → p < b) a≡b a<b)
<-irrefl'' a b (inr b<a) a≡b = <-irrefl b (substₚ (λ p → b < p) a≡b b<a)

<-tricho : (a b : ℚ) → ([ a < b ] ⊎ [ b < a ]) ⊎ [ a ≡ₚ b ] -- TODO: insert trichotomy definition here
<-tricho = SetQuotient.elimProp2 {R = _∼_} (λ a b → isProp[] ([ <-irrefl'' a b ] ([ <-asym a b ] (a < b) ⊎ᵖ (b < a)) ⊎ᵖ (a ≡ₚ b))) γ where
  γ : (a b : ℤ × ℕ₊₁) → ([ [ a ]ᶠ < [ b ]ᶠ ] ⊎ [ [ b ]ᶠ < [ a ]ᶠ ]) ⊎ [ [ a ]ᶠ ≡ₚ [ b ]ᶠ ]
  γ a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) = κ where
    aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
    bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
    κ : ([ (aᶻ ·ᶻ bⁿᶻ) <ᶻ (bᶻ ·ᶻ aⁿᶻ) ] ⊎ [ (bᶻ ·ᶻ aⁿᶻ) <ᶻ (aᶻ ·ᶻ bⁿᶻ) ]) ⊎ [ [ aᶻ , aⁿ ]ᶠ ≡ₚ [ bᶻ , bⁿ ]ᶠ ]
    κ with <ᶻ-tricho (aᶻ ·ᶻ bⁿᶻ) (bᶻ ·ᶻ aⁿᶻ)
    ... | inl p = inl p
    ... | inr p = inr ∣ eq/ {R = _∼_} a b p ∣

<-StrictLinearOrder : [ isStrictLinearOrder _<_ ]
<-StrictLinearOrder .IsStrictLinearOrder.is-irrefl = <-irrefl
<-StrictLinearOrder .IsStrictLinearOrder.is-trans  = <-trans
<-StrictLinearOrder .IsStrictLinearOrder.is-tricho = <-tricho

<-StrictPartialOrder : [ isStrictPartialOrder _<_ ]
<-StrictPartialOrder = strictlinearorder⇒strictpartialorder _<_ <-StrictLinearOrder

_#_ : hPropRel ℚ ℚ ℓ-zero
x # y = [ <-asym x y ] (x < y) ⊎ᵖ (y < x)

#-ApartnessRel : [ isApartnessRel _#_ ]
#-ApartnessRel = #''-isApartnessRel <-StrictPartialOrder <-asym

open IsApartnessRel #-ApartnessRel public renaming
  ( is-irrefl  to #-irrefl
  ; is-sym     to #-sym
  ; is-cotrans to #-cotrans
  )

#-split' : ∀ z n → [ [ z , n ]ᶠ # 0 ] → [ z <ᶻ 0 ] ⊎ [ 0 <ᶻ z ]
#-split' (pos zero) _ p = p
#-split' (neg zero) _ p = p
#-split' (posneg i) _ p = p
#-split' (pos (suc n)) _ p = transport (λ i → [ suc (·ⁿ-identityʳ n i) <ⁿ 0 ] ⊎ [ 0 <ⁿ suc (·ⁿ-identityʳ n i) ]) p
#-split' (neg (suc n)) _ p = p

_⁻¹'  : (x : ℤ × ℕ₊₁) → [ [ x ]ᶠ # 0 ] → ℚ
(xᶻ , xⁿ) ⁻¹' = λ _ → [ signed (signᶻ xᶻ) (ℕ₊₁→ℕ xⁿ) , absᶻ⁺¹ xᶻ ]ᶠ

⁻¹'-respects-∼ : (a b : ℤ × ℕ₊₁) (p : a ∼ b)
                → PathP (λ i → [ eq/ a b p i # 0 ] → ℚ) (a ⁻¹') (b ⁻¹')
⁻¹'-respects-∼ a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) p = κ where
  aⁿᶻ = [1+ aⁿ ⁿ]ᶻ; 0<aⁿᶻ : [ 0 <ᶻ aⁿᶻ ]; 0<aⁿᶻ = is-0<ⁿᶻ -- ℕ₊₁.n aⁿ , +ⁿ-comm (ℕ₊₁.n aⁿ) 1
  bⁿᶻ = [1+ bⁿ ⁿ]ᶻ; 0<bⁿᶻ : [ 0 <ᶻ bⁿᶻ ]; 0<bⁿᶻ = is-0<ⁿᶻ -- ℕ₊₁.n bⁿ , +ⁿ-comm (ℕ₊₁.n bⁿ) 1
  η : signᶻ aᶻ ≡ signᶻ bᶻ
  η i = sign (eq/ a b p i)
  s : aᶻ ·ᶻ bⁿᶻ ≡ bᶻ ·ᶻ aⁿᶻ
  s = p
  r : [ [ aᶻ , aⁿ ]ᶠ # 0 ] → (signed (signᶻ aᶻ) (ℕ₊₁→ℕ aⁿ) , absᶻ⁺¹ aᶻ) ∼ (signed (signᶻ bᶻ) (ℕ₊₁→ℕ bⁿ) , absᶻ⁺¹ bᶻ)
  r q = φ where
    φ : signed (signᶻ aᶻ) (ℕ₊₁→ℕ aⁿ) ·ᶻ [1+ absᶻ⁺¹ bᶻ ⁿ]ᶻ ≡ signed (signᶻ bᶻ) (ℕ₊₁→ℕ bⁿ) ·ᶻ [1+ absᶻ⁺¹ aᶻ ⁿ]ᶻ
    φ with #-split' aᶻ aⁿ q
    -- proof for aᶻ < 0
    ... | inl aᶻ<0 =
      signed (signᶻ aᶻ) (ℕ₊₁→ℕ aⁿ) ·ᶻ [1+ absᶻ⁺¹ bᶻ ⁿ]ᶻ ≡⟨ (λ i → signed (<ᶻ0-signᶻ aᶻ aᶻ<0 i) (ℕ₊₁→ℕ aⁿ) ·ᶻ absᶻ⁺¹-identity bᶻ (inl bᶻ<0) i) ⟩
      signed  sneg      (ℕ₊₁→ℕ aⁿ) ·ᶻ pos (absᶻ bᶻ)      ≡⟨ cong₂ signed (λ i → sneg ·ˢ q₁ i) q₂ ⟩
      signed  sneg      (ℕ₊₁→ℕ bⁿ) ·ᶻ pos (absᶻ aᶻ)      ≡⟨ (λ i → signed (<ᶻ0-signᶻ bᶻ bᶻ<0 (~ i)) (ℕ₊₁→ℕ bⁿ) ·ᶻ absᶻ⁺¹-identity aᶻ (inl aᶻ<0) (~ i)) ⟩
      signed (signᶻ bᶻ) (ℕ₊₁→ℕ bⁿ) ·ᶻ [1+ absᶻ⁺¹ aᶻ ⁿ]ᶻ ∎ where
      bᶻ<0 : [ bᶻ <ᶻ 0 ]
      bᶻ<0 = ∼-preserves-<ᶻ aᶻ aⁿ bᶻ bⁿ p .fst aᶻ<0
      abstract
        c      = suc (<ᶻ-split-neg aᶻ aᶻ<0 .fst)
        d      = suc (<ᶻ-split-neg bᶻ bᶻ<0 .fst)
        aᶻ≡-c  : aᶻ ≡ neg c
        aᶻ≡-c  = <ᶻ-split-neg aᶻ aᶻ<0 .snd
        bᶻ≡-d  : bᶻ ≡ neg d
        bᶻ≡-d  = <ᶻ-split-neg bᶻ bᶻ<0 .snd
        absa≡c : absᶻ aᶻ ≡ c
        absa≡c i = absᶻ (aᶻ≡-c i)
        absb≡d : absᶻ bᶻ ≡ d
        absb≡d i = absᶻ (bᶻ≡-d i)
      q₁ : signᶻ (pos (absᶻ bᶻ)) ≡ signᶻ (pos (absᶻ aᶻ))
      q₁ = transport (λ i → signᶻ-pos (absᶻ bᶻ) (~ i) ≡ signᶻ-pos (absᶻ aᶻ) (~ i)) refl
      s' = bᶻ ·ᶻ aⁿᶻ    ≡ aᶻ ·ᶻ bⁿᶻ                       ≡⟨ (λ i → ·ᶻ-comm bᶻ aⁿᶻ i ≡ ·ᶻ-comm aᶻ bⁿᶻ i) ⟩
           aⁿᶻ ·ᶻ bᶻ    ≡ bⁿᶻ ·ᶻ aᶻ                       ≡⟨ (λ i → aⁿᶻ ·ᶻ bᶻ≡-d i ≡ bⁿᶻ ·ᶻ aᶻ≡-c i) ⟩
           aⁿᶻ ·ᶻ neg d ≡ bⁿᶻ ·ᶻ neg c                    ≡⟨ refl ⟩
             signed (signᶻ (neg d)) (suc (ℕ₊₁.n aⁿ) ·ⁿ d)
           ≡ signed (signᶻ (neg c)) (suc (ℕ₊₁.n bⁿ) ·ⁿ c) ∎
      q₂ = (suc (ℕ₊₁.n aⁿ) ·ⁿ       d ≡ suc (ℕ₊₁.n bⁿ) ·ⁿ      c  ⇒⟨ transport (λ i → suc (ℕ₊₁.n aⁿ) ·ⁿ absb≡d (~ i) ≡ suc (ℕ₊₁.n bⁿ) ·ⁿ absa≡c (~ i)) ⟩
            suc (ℕ₊₁.n aⁿ) ·ⁿ absᶻ bᶻ ≡ suc (ℕ₊₁.n bⁿ) ·ⁿ absᶻ aᶻ ◼) (λ i → absᶻ (transport s' (sym s) i))
    -- proof for 0 < aᶻ
    ... | inr 0<aᶻ =
      signed (signᶻ aᶻ ⊕ spos) (suc (ℕ₊₁.n aⁿ) ·ⁿ suc (ℕ₊₁.n (absᶻ⁺¹ bᶻ))) ≡⟨ (λ i → signed (0<ᶻ-signᶻ aᶻ 0<aᶻ i ⊕ spos) (suc (ℕ₊₁.n aⁿ) ·ⁿ suc (ℕ₊₁.n (absᶻ⁺¹ bᶻ)))) ⟩
      signed             spos  (suc (ℕ₊₁.n aⁿ) ·ⁿ suc (ℕ₊₁.n (absᶻ⁺¹ bᶻ))) ≡⟨ transport s' (sym s) ⟩
      signed             spos  (suc (ℕ₊₁.n bⁿ) ·ⁿ suc (ℕ₊₁.n (absᶻ⁺¹ aᶻ))) ≡⟨ (λ i → signed (0<ᶻ-signᶻ bᶻ 0<bᶻ (~ i) ⊕ spos) (suc (ℕ₊₁.n bⁿ) ·ⁿ suc (ℕ₊₁.n (absᶻ⁺¹ aᶻ)))) ⟩
      signed (signᶻ bᶻ ⊕ spos) (suc (ℕ₊₁.n bⁿ) ·ⁿ suc (ℕ₊₁.n (absᶻ⁺¹ aᶻ))) ∎ where
      0<bᶻ : [ 0 <ᶻ bᶻ ]
      0<bᶻ = ∼-preserves-<ᶻ aᶻ aⁿ bᶻ bⁿ p .snd 0<aᶻ
      abstract
        c       = <ᶻ-split-pos aᶻ 0<aᶻ .fst
        d       = <ᶻ-split-pos bᶻ 0<bᶻ .fst
        aᶻ≡sc   : aᶻ ≡ pos (suc c)
        bᶻ≡sd   : bᶻ ≡ pos (suc d)
        absa≡sc : absᶻ aᶻ ≡ suc c
        absb≡sd : absᶻ bᶻ ≡ suc d
        aᶻ≡sc   = <ᶻ-split-pos aᶻ 0<aᶻ .snd
        bᶻ≡sd   = <ᶻ-split-pos bᶻ 0<bᶻ .snd
        absa≡sc i = absᶻ (aᶻ≡sc i)
        absb≡sd i = absᶻ (bᶻ≡sd i)
      s' = bᶻ  ·ᶻ aⁿᶻ         ≡ aᶻ  ·ᶻ bⁿᶻ         ≡⟨ (λ i → ·ᶻ-comm bᶻ aⁿᶻ i ≡ ·ᶻ-comm aᶻ bⁿᶻ i) ⟩
           aⁿᶻ ·ᶻ bᶻ          ≡ bⁿᶻ ·ᶻ aᶻ          ≡⟨ (λ i → aⁿᶻ ·ᶻ bᶻ≡sd i ≡ bⁿᶻ ·ᶻ aᶻ≡sc i) ⟩
           aⁿᶻ ·ᶻ pos (suc d) ≡ bⁿᶻ ·ᶻ pos (suc c) ≡⟨ refl ⟩
             pos (suc (ℕ₊₁.n aⁿ) ·ⁿ suc d)
           ≡ pos (suc (ℕ₊₁.n bⁿ) ·ⁿ suc c) ≡⟨ (λ i → pos (suc (ℕ₊₁.n aⁿ) ·ⁿ absb≡sd (~ i)) ≡ pos (suc (ℕ₊₁.n bⁿ) ·ⁿ absa≡sc (~ i))) ⟩
             pos (suc (ℕ₊₁.n aⁿ) ·ⁿ absᶻ bᶻ)
           ≡ pos (suc (ℕ₊₁.n bⁿ) ·ⁿ absᶻ aᶻ) ≡⟨ (λ i → pos (suc (ℕ₊₁.n aⁿ) ·ⁿ absᶻ⁺¹-identityⁿ bᶻ (inr 0<bᶻ) (~ i)) ≡ pos (suc (ℕ₊₁.n bⁿ) ·ⁿ absᶻ⁺¹-identityⁿ aᶻ (inr 0<aᶻ) (~ i))) ⟩
             pos (suc (ℕ₊₁.n aⁿ) ·ⁿ suc (ℕ₊₁.n (absᶻ⁺¹ bᶻ)))
           ≡ pos (suc (ℕ₊₁.n bⁿ) ·ⁿ suc (ℕ₊₁.n (absᶻ⁺¹ aᶻ))) ∎
  -- eq/ a b r : [ a ]ᶠ ≡ [ b ]ᶠ
  γ : [ [ a ]ᶠ # 0 ] ≡ [ [ b ]ᶠ # 0 ]
  γ i = [ eq/ a b p i # 0 ]
  κ : PathP _ (a ⁻¹') (b ⁻¹')
  κ i = λ(q : [ eq/ a b p i # 0 ]) → eq/ (signed (signᶻ aᶻ) (ℕ₊₁→ℕ aⁿ) , absᶻ⁺¹ aᶻ) (signed (signᶻ bᶻ) (ℕ₊₁→ℕ bⁿ) , absᶻ⁺¹ bᶻ) (r (ψ q)) i where
    ψ : [ eq/ a b p i # 0 ] → [ eq/ a b p i0 # 0 ]
    ψ p = transport (λ j → γ (i ∧ ~ j)) p

_⁻¹ : (x : ℚ) → {{ _ : [ x # 0 ]}} → ℚ
(x ⁻¹) {{p}} = SetQuotient.elim {R = _∼_} {B = λ x → [ x # 0 ] → ℚ} φ _⁻¹' ⁻¹'-respects-∼ x p where
  φ : ∀ x → isSet ([ x # 0 ] → ℚ)
  φ x = isSetΠ (λ _ → isSetℚ)
  -- φ' : ∀ x → isSet ({{_ : [ x # 0 ]}} → ℚ)
  -- φ' x = transport (λ i → ∀ x → isSet (instance≡ {A = [ x # 0 ]} {B = λ _ → ℚ} (~ i))) φ x

⊕-diagonal : ∀ s → s ⊕ s ≡ spos
⊕-diagonal spos = refl
⊕-diagonal sneg = refl

zeroᶠ : ∀ x → [ 0 / x ] ≡ 0
zeroᶠ x = eq/ (0 , x) (0 , 1) refl

#⇒#ᶻ : ∀ xᶻ xⁿ → [ [ xᶻ / xⁿ ] # 0 ] → [ xᶻ #ᶻ 0 ]
#⇒#ᶻ (pos zero)    xⁿ p = p
#⇒#ᶻ (neg zero)    xⁿ p = p
#⇒#ᶻ (posneg i)    xⁿ p = p
#⇒#ᶻ (pos (suc n)) xⁿ (inl p) = inl (transport (λ i → [ suc (·ⁿ-identityʳ n i) <ⁿ 0 ]) p)
#⇒#ᶻ (pos (suc n)) xⁿ (inr p) = inr (transport (λ i → [ 0 <ⁿ suc (·ⁿ-identityʳ n i) ]) p)
#⇒#ᶻ (neg (suc n)) xⁿ p = inl tt

#ᶻ⇒# : ∀ xᶻ xⁿ → [ xᶻ #ᶻ 0 ] → [ [ xᶻ / xⁿ ] # 0 ]
#ᶻ⇒# (pos zero) xⁿ p = p
#ᶻ⇒# (neg zero) xⁿ p = p
#ᶻ⇒# (posneg i) xⁿ p = p
#ᶻ⇒# (pos (suc n)) xⁿ (inl p) = inl (transport (λ i → [ suc (·ⁿ-identityʳ n (~ i)) <ⁿ 0 ]) p)
#ᶻ⇒# (pos (suc n)) xⁿ (inr p) = inr (transport (λ i → [ 0 <ⁿ suc (·ⁿ-identityʳ n (~ i)) ]) p)
#ᶻ⇒# (neg (suc n)) xⁿ p = inl tt

·-invʳ' : ∀ x → (p : [ [ x ]ᶠ # 0 ]) → [ x ]ᶠ · ([ x ]ᶠ ⁻¹) {{p}} ≡ 1
·-invʳ' x@(xᶻ , xⁿ) p = γ where
  aᶻ  : ℤ
  aⁿ  : ℕ₊₁
  aᶻ  = signed (signᶻ xᶻ ⊕ signᶻ xᶻ) (absᶻ xᶻ ·ⁿ suc (ℕ₊₁.n xⁿ))
  aⁿ  = 1+ (ℕ₊₁.n (absᶻ⁺¹ xᶻ) +ⁿ ℕ₊₁.n xⁿ ·ⁿ suc (ℕ₊₁.n (absᶻ⁺¹ xᶻ)))
  aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
  η = absᶻ xᶻ ·ⁿ suc (ℕ₊₁.n xⁿ) ≡⟨ ·ⁿ-comm (absᶻ xᶻ) (suc (ℕ₊₁.n xⁿ)) ⟩
      suc (ℕ₊₁.n xⁿ) ·ⁿ absᶻ xᶻ ≡⟨ (λ i → suc (ℕ₊₁.n xⁿ) ·ⁿ absᶻ⁺¹-identityⁿ xᶻ (#⇒#ᶻ xᶻ xⁿ p) (~ i)) ⟩
      suc (ℕ₊₁.n xⁿ) ·ⁿ suc (ℕ₊₁.n (absᶻ⁺¹ xᶻ)) ∎
  ψ : aᶻ ≡ aⁿᶻ
  ψ = signed (signᶻ xᶻ ⊕ signᶻ xᶻ) (absᶻ xᶻ ·ⁿ suc (ℕ₊₁.n xⁿ)) ≡⟨ cong₂ signed (⊕-diagonal (signᶻ xᶻ)) refl ⟩
      signed  spos                 (absᶻ xᶻ ·ⁿ suc (ℕ₊₁.n xⁿ)) ≡⟨ cong pos η ⟩
      pos (suc (ℕ₊₁.n xⁿ) ·ⁿ suc (ℕ₊₁.n (absᶻ⁺¹ xᶻ))) ∎
  φ : aᶻ ·ᶻ 1 ≡ 1 ·ᶻ aⁿᶻ
  φ = ·ᶻ-identity aᶻ .fst ∙ ψ ∙ sym (·ᶻ-identity aⁿᶻ .snd)
  κ : (aᶻ , aⁿ) ∼ (pos 1 , (1+ 0))
  κ = φ
  γ : [ aᶻ , aⁿ ]ᶠ ≡ 1
  γ = eq/ (aᶻ , aⁿ) (pos 1 , (1+ 0)) κ

·-invʳ : ∀ x → (p : [ x # 0 ]) → x · (x ⁻¹) {{p}} ≡ 1
·-invʳ = let P : ℚ → hProp ℓ-zero
             P x = ∀ᵖ[ p ∶ x # 0 ] ([ isSetℚ ] x · (x ⁻¹) {{p}} ≡ˢ 1)
         in  SetQuotient.elimProp {R = _∼_} (λ x → isProp[] (P x)) ·-invʳ'

·-invˡ : ∀ x → (p : [ x # 0 ]) → (x ⁻¹) {{p}} · x ≡ 1
·-invˡ x p = ·-comm _ x ∙ ·-invʳ x p

-- NOTE: we already have
--   ℚ-cancelˡ : ∀ {a b} (c : ℕ₊₁) → [ ℕ₊₁→ℤ c ℤ.* a / c *₊₁ b ] ≡ [ a / b ]
--   ℚ-cancelʳ : ∀ {a b} (c : ℕ₊₁) → [ a ℤ.* ℕ₊₁→ℤ c / b *₊₁ c ] ≡ [ a / b ]

module _ (aᶻ : ℤ) (aⁿ bⁿ : ℕ₊₁) (let aⁿᶻ = [1+ aⁿ ⁿ]ᶻ) (let bⁿᶻ = [1+ bⁿ ⁿ]ᶻ) where
  private
    lem : ∀ a b → signᶻ a ≡ signᶻ (signed (signᶻ a ⊕ spos) (absᶻ a ·ⁿ (ℕ₊₁→ℕ b)))
    lem (pos zero)    b j = signᶻ (posneg (i0 ∧ ~ j))
    lem (neg zero)    b j = signᶻ (posneg (i1 ∧ ~ j))
    lem (posneg i)    b j = signᶻ (posneg (i  ∧ ~ j))
    lem (pos (suc n)) b   = refl
    lem (neg (suc n)) b   = refl

    -- one could write this as a one-liner, even without mentioning cᶻ and cⁿ, but this reduces the overall proof-readability
    expand-fraction' : [ aᶻ / aⁿ ] ≡ [ aᶻ ·ᶻ bⁿᶻ / aⁿ ·₊₁ bⁿ ]
    expand-fraction' = eq/ _ _ $ (λ i → signed (lem aᶻ bⁿ i ⊕ spos) (((λ i → absᶻ aᶻ ·ⁿ ·ⁿ-comm (ℕ₊₁→ℕ aⁿ) (ℕ₊₁→ℕ bⁿ) i) ∙ ·ⁿ-assoc (absᶻ aᶻ) (ℕ₊₁→ℕ bⁿ) (ℕ₊₁→ℕ aⁿ)) i))

  expand-fraction : [ aᶻ / aⁿ ] ≡ [ aᶻ ·ᶻ bⁿᶻ / aⁿ ·₊₁ bⁿ ]
  expand-fraction = eq/ _ _ γ where
    cᶻ : ℤ
    cᶻ = signed (signᶻ aᶻ ⊕ spos) (absᶻ aᶻ ·ⁿ (ℕ₊₁→ℕ bⁿ))
    cⁿ : ℕ₊₁
    cⁿ = 1+ (ℕ₊₁.n bⁿ +ⁿ ℕ₊₁.n aⁿ ·ⁿ (ℕ₊₁→ℕ bⁿ))
    κ =  absᶻ aᶻ ·ⁿ ((ℕ₊₁→ℕ aⁿ)  ·ⁿ (ℕ₊₁→ℕ bⁿ)) ≡[ i ]⟨ absᶻ aᶻ ·ⁿ ·ⁿ-comm (ℕ₊₁→ℕ aⁿ) (ℕ₊₁→ℕ bⁿ) i ⟩
         absᶻ aᶻ ·ⁿ ((ℕ₊₁→ℕ bⁿ)  ·ⁿ (ℕ₊₁→ℕ aⁿ)) ≡⟨ ·ⁿ-assoc (absᶻ aᶻ) (ℕ₊₁→ℕ bⁿ) (ℕ₊₁→ℕ aⁿ) ⟩
        (absᶻ aᶻ ·ⁿ  (ℕ₊₁→ℕ bⁿ)) ·ⁿ (ℕ₊₁→ℕ aⁿ)  ∎
    γ : (aᶻ , aⁿ) ∼ (cᶻ , cⁿ)
    γ i = signed (lem aᶻ bⁿ i ⊕ spos) (κ i)

·-≡' : ∀ aᶻ aⁿ bᶻ bⁿ → [ aᶻ / aⁿ ] · [ bᶻ / bⁿ ] ≡ [ aᶻ ·ᶻ bᶻ / aⁿ ·₊₁ bⁿ ]
·-≡' aᶻ aⁿ bᶻ bⁿ = refl

∼⁻¹ : ∀ aᶻ aⁿ bᶻ bⁿ → [ aᶻ / aⁿ ] ≡ [ bᶻ / bⁿ ] → (aᶻ , aⁿ) ∼ (bᶻ , bⁿ)
∼⁻¹ aᶻ aⁿ bᶻ bⁿ p = eq/⁻¹ _ _ p

-- already have this in ᶻ
signᶻ-absᶻ-identity : ∀ a → signed (signᶻ a) (absᶻ a) ≡ a
signᶻ-absᶻ-identity (pos zero) j  = posneg (i0 ∧ j)
signᶻ-absᶻ-identity (neg zero) j  = posneg (i1 ∧ j)
signᶻ-absᶻ-identity (posneg i) j  = posneg (i  ∧ j)
signᶻ-absᶻ-identity (pos (suc n)) = refl
signᶻ-absᶻ-identity (neg (suc n)) = refl

-- already have this in ᶻ
absᶻ-preserves-·ᶻ : ∀ a b → absᶻ (a ·ᶻ b) ≡ absᶻ a ·ⁿ absᶻ b
absᶻ-preserves-·ᶻ a b = refl

-- already have this in ᶻ
signᶻ-absᶻ-≡ : ∀ a b → signᶻ a ≡ signᶻ b → absᶻ a ≡ absᶻ b → a ≡ b
signᶻ-absᶻ-≡ a b p q = transport (λ i → signᶻ-absᶻ-identity a i ≡ signᶻ-absᶻ-identity b i) λ i → signed (p i) (q i)

ℚ-reflects-nom : ∀ aᶻ bᶻ n → [ aᶻ / n ] ≡ [ bᶻ / n ] → aᶻ ≡ bᶻ
ℚ-reflects-nom aᶻ bᶻ n p = signᶻ-absᶻ-≡ aᶻ bᶻ φ η where
  n' = suc (ℕ₊₁.n n)
  0<n' : [ 0 <ⁿ n' ]
  0<n' = 0<ⁿsuc (ℕ₊₁.n n)
  s = signed (signᶻ aᶻ       ) (absᶻ aᶻ ·ⁿ n') ≡⟨ cong₂ signed (sym (⊕-identityʳ (signᶻ aᶻ))) refl ⟩
      signed (signᶻ aᶻ ⊕ spos) (absᶻ aᶻ ·ⁿ n') ≡⟨ eq/⁻¹ _ _ p ⟩
      signed (signᶻ bᶻ ⊕ spos) (absᶻ bᶻ ·ⁿ n') ≡⟨ cong₂ signed (⊕-identityʳ (signᶻ bᶻ)) refl ⟩
      signed (signᶻ bᶻ       ) (absᶻ bᶻ ·ⁿ n') ∎
  φ : signᶻ aᶻ ≡ signᶻ bᶻ
  φ i = sign (p i)
  κ : absᶻ aᶻ ·ⁿ n' ≡ absᶻ bᶻ ·ⁿ n'
  κ i = absᶻ (s i)
  η : absᶻ aᶻ ≡ absᶻ bᶻ
  η = ·ⁿ-reflects-≡ʳ (absᶻ aᶻ) (absᶻ bᶻ) n' 0<n' κ

ℕ₊₁→ℕ-reflects-≡ : ∀ a b → (ℕ₊₁→ℕ a) ≡ (ℕ₊₁→ℕ b) → a ≡ b
ℕ₊₁→ℕ-reflects-≡ (1+ a) (1+ b) p i = 1+ +ⁿ-preserves-≡ˡ {1} {a} {b} p i

ℚ-reflects-denom : ∀ z aⁿ bⁿ → [ z #ᶻ 0 ] → [ z / aⁿ ] ≡ [ z / bⁿ ] → aⁿ ≡ bⁿ
ℚ-reflects-denom z aⁿ bⁿ z#0 p = ℕ₊₁→ℕ-reflects-≡ aⁿ bⁿ (sym γ) where
  κ : absᶻ z ·ⁿ (ℕ₊₁→ℕ bⁿ) ≡ absᶻ z ·ⁿ (ℕ₊₁→ℕ aⁿ)
  κ i = absᶻ (eq/⁻¹ _ _ p i)
  φ : (z#0 : [ z #ᶻ 0 ]) → [ 0 <ⁿ absᶻ z ]
  φ (inl z<0) = let (n , z≡-sn) = <ᶻ-split-neg z z<0 in transport (λ i → [ 0 <ⁿ absᶻ (z≡-sn (~ i)) ]) (0<ⁿsuc n)
  φ (inr 0<z) = let (n , z≡+sn) = <ᶻ-split-pos z 0<z in transport (λ i → [ 0 <ⁿ absᶻ (z≡+sn (~ i)) ]) (0<ⁿsuc n)
  γ : ℕ₊₁→ℕ bⁿ ≡ ℕ₊₁→ℕ aⁿ
  γ = ·ⁿ-reflects-≡ˡ (ℕ₊₁→ℕ bⁿ) (ℕ₊₁→ℕ aⁿ) (absᶻ z) (φ z#0) κ

-- already have this in QuoInt
pos-reflects-≡ : ∀ a b → pos a ≡ pos b → a ≡ b
pos-reflects-≡ a b p i = absᶻ (p i)

snotz' : ∀ n → ¬ᵗ (suc n ≡ 0)
snotz' n p = let caseNat = λ{ 0 → ⊥⊥ ; (suc n) → ℕ } in subst caseNat p 0

¬0≡1ⁿ : ¬ᵗ _≡_ {A = ℕ} 0 1
¬0≡1ⁿ p = snotzⁿ {0} (sym p)

¬0≡1ᶻ : ¬ᵗ _≡_ {A = ℤ} 0 1
¬0≡1ᶻ p = ¬0≡1ⁿ $ pos-reflects-≡ 0 1 p

¬0≡1ᶠ : ¬ᵗ _≡_ {A = ℚ} 0 1
¬0≡1ᶠ p = ¬0≡1ᶻ $ ℚ-reflects-nom 0 1 1 p

-- already have this in ᶻ
signed0≡0 : ∀ s → signed s 0 ≡ 0
signed0≡0 spos   = refl
signed0≡0 sneg i = posneg (~ i)

·-nullifiesˡ' : ∀ bᶻ bⁿ → 0 · [ bᶻ / bⁿ ] ≡ 0
·-nullifiesˡ' bᶻ bⁿ =
  [ signed (signᶻ bᶻ) 0 / (1+ (ℕ₊₁.n bⁿ +ⁿ 0)) ] ≡⟨ cong₂ [_/_] (signed0≡0 (signᶻ bᶻ)) refl ⟩
  [                   0 / (1+ (ℕ₊₁.n bⁿ +ⁿ 0)) ] ≡⟨ zeroᶠ (1+ (ℕ₊₁.n bⁿ +ⁿ 0)) ⟩
  [                   0 / (1+ 0)               ] ∎

·-nullifiesʳ' : ∀ bᶻ bⁿ → [ bᶻ / bⁿ ] · 0 ≡ 0
·-nullifiesʳ' bᶻ bⁿ = ·-comm [ bᶻ / bⁿ ] 0 ∙ ·-nullifiesˡ' bᶻ bⁿ

·-inv-<ᶻ' : (a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) : ℤ × ℕ₊₁) → ([ a ]ᶠ · [ b ]ᶠ ≡ 1) → [ (0 <ᶻ aᶻ) ⊓ (0 <ᶻ bᶻ) ] ⊎ [ (aᶻ <ᶻ 0) ⊓ (bᶻ <ᶻ 0) ]
·-inv-<ᶻ' a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) p = γ where
  aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
  bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
  κ = ([ aᶻ /  aⁿ ] · [ bᶻ /   bⁿ ] ≡ [     1      /   (1+ 0)  ] ⇒⟨ transport (cong₂ _≡_ refl (transport (λ i → 1 ≡ [ ·ᶻ-identity aⁿᶻ .snd i / ·₊₁-identityˡ aⁿ i ]) (expand-fraction 1 1 aⁿ) ∙ expand-fraction aⁿᶻ aⁿ bⁿ)) ⟩
       [ aᶻ ·ᶻ bᶻ   /   aⁿ ·₊₁ bⁿ ] ≡ [ aⁿᶻ ·ᶻ bⁿᶻ / aⁿ ·₊₁ bⁿ ] ⇒⟨ ℚ-reflects-nom _ _ (aⁿ ·₊₁ bⁿ) ⟩
         aᶻ ·ᶻ bᶻ                   ≡   aⁿᶻ ·ᶻ bⁿᶻ               ◼) p
  φ₀ : [ 0 <ⁿ ((ℕ₊₁→ℕ aⁿ) ·ⁿ (ℕ₊₁→ℕ bⁿ)) ]
  φ₀ = 0<ⁿsuc _
  φ₁ : [ 0 <ᶻ aⁿᶻ ·ᶻ bⁿᶻ ]
  φ₁ = φ₀
  φ₂ : [ 0 <ᶻ aᶻ  ·ᶻ bᶻ  ]
  φ₂ = subst (λ p → [ 0 <ᶻ p ]) (sym κ) φ₁
  γ : [ (0 <ᶻ aᶻ) ⊓ (0 <ᶻ bᶻ) ] ⊎ [ (aᶻ <ᶻ 0) ⊓ (bᶻ <ᶻ 0) ]
  γ with <ᶻ-tricho 0 aᶻ
  ... | inl (inl 0<aᶻ) = inl (0<aᶻ , ·ᶻ-reflects-0<ᶻ aᶻ bᶻ φ₂ .fst .fst 0<aᶻ)
  ... | inl (inr aᶻ<0) = inr (aᶻ<0 , ·ᶻ-reflects-0<ᶻ aᶻ bᶻ φ₂ .snd .fst aᶻ<0)
  ... | inr      0≡aᶻ  = ⊥-elim {A = λ _ → [ (0 <ᶻ aᶻ) ⊓ (0 <ᶻ bᶻ) ] ⊎ [ (aᶻ <ᶻ 0) ⊓ (bᶻ <ᶻ 0) ]} (¬0≡1ᶠ η) where
    η =   0                      ≡⟨ sym $ zeroᶠ (aⁿ ·₊₁ bⁿ) ⟩
        [ 0        / aⁿ ·₊₁ bⁿ ] ≡⟨ (λ i → [ ·ᶻ-nullifiesˡ bᶻ (~ i) / aⁿ ·₊₁ bⁿ ]) ⟩
        [ 0  ·ᶻ bᶻ / aⁿ ·₊₁ bⁿ ] ≡⟨ (λ i → [ 0≡aᶻ i ·ᶻ bᶻ / aⁿ ·₊₁ bⁿ ]) ⟩
        [ aᶻ ·ᶻ bᶻ / aⁿ ·₊₁ bⁿ ] ≡⟨ p ⟩
          1                      ∎

private
  lem0<ᶻ : ∀ aᶻ → [ 0 <ᶻ aᶻ ] → aᶻ ≡ signed (signᶻ aᶻ ⊕ spos) (absᶻ aᶻ ·ⁿ 1)
  lem0<ᶻ aᶻ 0<aᶻ =
    aᶻ                                                            ≡⟨ γ ⟩
    pos (suc n)                                                   ≡⟨ (λ i → pos (suc (·ⁿ-identityʳ n (~ i)))) ⟩
    pos (suc (n ·ⁿ 1))                                            ≡⟨ refl ⟩
    signed (signᶻ (pos (suc n)) ⊕ spos) (absᶻ (pos (suc n)) ·ⁿ 1) ≡⟨ (λ i → signed (signᶻ (γ (~ i)) ⊕ spos) (absᶻ (γ (~ i)) ·ⁿ 1)) ⟩
    signed (signᶻ  aᶻ           ⊕ spos) (absᶻ  aᶻ           ·ⁿ 1) ∎ where
    abstract
      n = <ᶻ-split-pos aᶻ 0<aᶻ .fst
      γ : aᶻ ≡ pos (suc n)
      γ = <ᶻ-split-pos aᶻ 0<aᶻ .snd

  lem<ᶻ0 : ∀ aᶻ → [ aᶻ <ᶻ 0  ] → aᶻ ≡ signed (signᶻ aᶻ ⊕ spos) (absᶻ aᶻ ·ⁿ 1)
  lem<ᶻ0 aᶻ aᶻ<0 =
    aᶻ                                                            ≡⟨ γ ⟩
    neg (suc n)                                                   ≡⟨ (λ i → neg (suc (·ⁿ-identityʳ n (~ i)))) ⟩
    neg (suc (n ·ⁿ 1))                                            ≡⟨ refl ⟩
    signed (signᶻ (neg (suc n)) ⊕ spos) (absᶻ (neg (suc n)) ·ⁿ 1) ≡⟨ (λ i → signed (signᶻ (γ (~ i)) ⊕ spos) (absᶻ (γ (~ i)) ·ⁿ 1)) ⟩
    signed (signᶻ  aᶻ           ⊕ spos) (absᶻ  aᶻ           ·ⁿ 1) ∎ where
    abstract
      n = <ᶻ-split-neg aᶻ aᶻ<0 .fst
      γ : aᶻ ≡ neg (suc n)
      γ = <ᶻ-split-neg aᶻ aᶻ<0 .snd

·-inv#0' : (a b : ℤ × ℕ₊₁) → ([ a ]ᶠ · [ b ]ᶠ ≡ 1) → [ [ a ]ᶠ # 0 ⊓ [ b ]ᶠ # 0 ]
·-inv#0' a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) p with ·-inv-<ᶻ' a b p
... | inl (0<aᶻ , 0<bᶻ) = inr (subst (λ p → [ 0 <ᶻ p ]) (lem0<ᶻ aᶻ 0<aᶻ) 0<aᶻ)
                        , inr (subst (λ p → [ 0 <ᶻ p ]) (lem0<ᶻ bᶻ 0<bᶻ) 0<bᶻ)
... | inr (aᶻ<0 , bᶻ<0) = inl (subst (λ p → [ p <ᶻ 0 ]) (lem<ᶻ0 aᶻ aᶻ<0) aᶻ<0)
                        , inl (subst (λ p → [ p <ᶻ 0 ]) (lem<ᶻ0 bᶻ bᶻ<0) bᶻ<0)

·-inv#0 : ∀ x y → x · y ≡ 1 → [(x # 0) ⊓ (y # 0)]
·-inv#0 = let P : ℚ → ℚ → hProp ℓ-zero
              P x y = ([ isSetℚ ] (x · y) ≡ˢ 1) ⇒ ((x # 0) ⊓ (y # 0))
          in  SetQuotient.elimProp2 {R = _∼_} {C = λ x y → [ P x y ]} (λ x y → isProp[] (P x y)) ·-inv#0'

·-inv#0ˡ' : (a b : ℤ × ℕ₊₁) → ([ a ]ᶠ · [ b ]ᶠ ≡ 1) → [ [ a ]ᶠ # 0 ]
·-inv#0ˡ' a b p = ·-inv#0' a b p .fst

·-inv#0ˡ : ∀ x y → x · y ≡ 1 → [ x # 0 ]
·-inv#0ˡ x y p = ·-inv#0 x y p .fst

-- ·-reflects-signʳ : ∀ a b c → [ 0 < c ] → a · b ≡ c → [ ((0 < b) ⇒ (0 < a)) ⊓ ((b < 0) ⇒ (a < 0)) ]
-- ·-reflects-signʳ a b c p q .fst 0<b = {!   !}
-- ·-reflects-signʳ a b c p q .snd b<0 = {!   !}
-- ⁻¹-preserves-sign : ∀ z z⁻¹ → [ 0f < z ] → z · z⁻¹ ≡ 1f → [ 0f < z⁻¹ ]
-- ⁻¹-preserves-sign z z⁻¹

-- -- TODO: this is a plain copy from `MorePropAlgebra.Properties.AlmostPartiallyOrderedField`
-- --       we might put it into `MorePropAlgebra.Consequences`
-- -- uniqueness of inverses from `·-assoc` + `·-comm` + `·-lid` + `·-rid`
-- ·-rinv-unique'' : (x y z : F) → [ x · y ≡ˢ 1f ] → [ x · z ≡ˢ 1f ] → [ y ≡ˢ z ]
-- ·-rinv-unique'' x y z x·y≡1 x·z≡1 =
--   (      x  · y  ≡ˢ     1f ⇒ᵖ⟨ (λ x·y≡1 i → z · x·y≡1 i) ⟩
--     z · (x  · y) ≡ˢ z · 1f ⇒ᵖ⟨ pathTo⇒ (λ i → ·-assoc z x y i ≡ˢ ·-rid z i) ⟩
--    (z ·  x) · y  ≡ˢ z      ⇒ᵖ⟨ pathTo⇒ (λ i → (·-comm z x i) · y  ≡ˢ z) ⟩
--    (x ·  z) · y  ≡ˢ z      ⇒ᵖ⟨ pathTo⇒ (λ i → x·z≡1 i · y  ≡ˢ z) ⟩
--       1f    · y  ≡ˢ z      ⇒ᵖ⟨ pathTo⇒ (λ i → ·-lid y i ≡ˢ z) ⟩
--               y  ≡ˢ z      ◼ᵖ) .snd x·y≡1

·-inv'' : ∀ x → [ (∃[ y ] ([ isSetℚ ] (x · y) ≡ˢ 1)) ⇔ (x # 0) ]
·-inv'' x .fst p = ∣∣-elim (λ _ → φ') (λ{ (y , q) → γ y q } ) p where
  φ' = isProp[] (x # 0)
  γ : ∀ y → [ [ isSetℚ ] (x · y) ≡ˢ 1 ] → [ x # 0 ]
  γ y q = ·-inv#0ˡ x y q
·-inv'' x .snd p = ∣ (x ⁻¹) {{p}} , ·-invʳ x p ∣

-- -- note, that the following holds definitionally (TODO: put this at the definition of `min`)
-- _ =    min [ aᶻ , aⁿ ]ᶠ [ bᶻ , bⁿ ]ᶠ                 ≡⟨ refl ⟩
--     [ (minᶻ (aᶻ *ᶻ bⁿᶻ) (bᶻ *ᶻ aⁿᶻ) , aⁿ *₊₁ bⁿ) ]ᶠ  ∎
-- -- and we also have definitionally
-- _ : [1+ aⁿ *₊₁ bⁿ ⁿ]ᶻ ≡ aⁿᶻ *ᶻ bⁿᶻ
-- _ = refl
-- -- therefore, we have for the LHS:
-- _ = ([ cᶻ , cⁿ ]ᶠ ≤ min [ aᶻ , aⁿ ]ᶠ [ bᶻ , bⁿ ]ᶠ)                      ≡⟨ refl ⟩
--     ([ cᶻ , cⁿ ]ᶠ ≤ [ (minᶻ (aᶻ *ᶻ bⁿᶻ) (bᶻ *ᶻ aⁿᶻ) , aⁿ *₊₁ bⁿ) ]ᶠ)    ≡⟨ refl ⟩
--     (¬([ (minᶻ (aᶻ *ᶻ bⁿᶻ) (bᶻ *ᶻ aⁿᶻ) , aⁿ *₊₁ bⁿ) ]ᶠ < [ cᶻ , cⁿ ]ᶠ)) ≡⟨ refl ⟩
--     ¬((minᶻ (aᶻ *ᶻ bⁿᶻ) (bᶻ *ᶻ aⁿᶻ) *ᶻ cⁿᶻ) <ᶻ (cᶻ *ᶻ (aⁿᶻ *ᶻ bⁿᶻ)))    ≡⟨ refl ⟩
--     ((cᶻ *ᶻ (aⁿᶻ *ᶻ bⁿᶻ)) ≤ᶻ (minᶻ (aᶻ *ᶻ bⁿᶻ) (bᶻ *ᶻ aⁿᶻ) *ᶻ cⁿᶻ))     ∎
-- -- similar for the RHS:
-- _ =  ([ cᶻ , cⁿ ]ᶠ ≤ [ aᶻ , aⁿ ]ᶠ) ⊓  ([ cᶻ , cⁿ ]ᶠ ≤ [ bᶻ , bⁿ ]ᶠ) ≡⟨ refl ⟩
--     ¬([ aᶻ , aⁿ ]ᶠ < [ cᶻ , cⁿ ]ᶠ) ⊓ ¬([ bᶻ , bⁿ ]ᶠ < [ cᶻ , cⁿ ]ᶠ) ≡⟨ refl ⟩
--     ¬((aᶻ *ᶻ cⁿᶻ)  <ᶻ (cᶻ *ᶻ aⁿᶻ)) ⊓ ¬((bᶻ *ᶻ cⁿᶻ)  <ᶻ (cᶻ *ᶻ bⁿᶻ)) ≡⟨ refl ⟩
--      ((cᶻ *ᶻ aⁿᶻ)  ≤ᶻ (aᶻ *ᶻ cⁿᶻ)) ⊓  ((cᶻ *ᶻ bⁿᶻ)  ≤ᶻ (bᶻ *ᶻ cⁿᶻ)) ∎
-- -- therfore, only properties on ℤ remain
-- RHS = [ ((cᶻ *ᶻ aⁿᶻ)  ≤ᶻ (aᶻ *ᶻ cⁿᶻ)) ⊓  ((cᶻ *ᶻ bⁿᶻ)  ≤ᶻ (bᶻ *ᶻ cⁿᶻ)) ]
-- LHS = [ ((cᶻ *ᶻ (aⁿᶻ *ᶻ bⁿᶻ)) ≤ᶻ (minᶻ (aᶻ *ᶻ bⁿᶻ) (bᶻ *ᶻ aⁿᶻ) *ᶻ cⁿᶻ)) ]
-- strategy: multiply everything with aⁿᶻ, bⁿᶻ, cⁿᶻ

is-min : (x y z : ℚ) → [ (z ≤ min x y) ⇔ (z ≤ x) ⊓ (z ≤ y) ]
is-min = SetQuotient.elimProp3  {R = _∼_} (λ x y z → isProp[] ((z ≤ min x y) ⇔ (z ≤ x) ⊓ (z ≤ y))) γ where
  γ : (a b c : ℤ × ℕ₊₁) → [ ([ c ]ᶠ ≤ min [ a ]ᶠ [ b ]ᶠ) ⇔ ([ c ]ᶠ ≤ [ a ]ᶠ) ⊓ ([ c ]ᶠ ≤ [ b ]ᶠ) ]
  γ a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) c@(cᶻ , cⁿ) = pathTo⇔ (sym κ) where
    aⁿᶻ = [1+ aⁿ ⁿ]ᶻ; 0≤aⁿᶻ : [ 0 ≤ᶻ aⁿᶻ ]; 0≤aⁿᶻ = is-0≤ⁿᶻ
    bⁿᶻ = [1+ bⁿ ⁿ]ᶻ; 0≤bⁿᶻ : [ 0 ≤ᶻ bⁿᶻ ]; 0≤bⁿᶻ = is-0≤ⁿᶻ
    cⁿᶻ = [1+ cⁿ ⁿ]ᶻ; 0≤cⁿᶻ : [ 0 ≤ᶻ cⁿᶻ ]; 0≤cⁿᶻ = is-0≤ⁿᶻ
    κ = (
      ((cᶻ ·ᶻ aⁿᶻ)         ≤ᶻ (aᶻ ·ᶻ cⁿᶻ)        ) ⊓ ((cᶻ ·ᶻ bⁿᶻ)         ≤ᶻ (bᶻ ·ᶻ cⁿᶻ)        ) ≡⟨ ⊓≡⊓ (·ᶻ-creates-≤ᶻ-≡ (cᶻ ·ᶻ aⁿᶻ) (aᶻ ·ᶻ cⁿᶻ) bⁿᶻ 0≤bⁿᶻ) (·ᶻ-creates-≤ᶻ-≡ (cᶻ ·ᶻ bⁿᶻ) (bᶻ ·ᶻ cⁿᶻ) aⁿᶻ 0≤aⁿᶻ) ⟩
      ((cᶻ ·ᶻ aⁿᶻ) ·ᶻ bⁿᶻ  ≤ᶻ (aᶻ ·ᶻ cⁿᶻ) ·ᶻ bⁿᶻ ) ⊓ ((cᶻ ·ᶻ bⁿᶻ) ·ᶻ aⁿᶻ  ≤ᶻ (bᶻ ·ᶻ cⁿᶻ) ·ᶻ aⁿᶻ ) ≡⟨ ⊓≡⊓ (λ i → ·ᶻ-assoc cᶻ aⁿᶻ bⁿᶻ (~ i) ≤ᶻ ·ᶻ-assoc aᶻ cⁿᶻ bⁿᶻ (~ i)) (λ i → ·ᶻ-assoc cᶻ bⁿᶻ aⁿᶻ (~ i) ≤ᶻ ·ᶻ-assoc bᶻ cⁿᶻ aⁿᶻ (~ i)) ⟩
      ( cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ) ≤ᶻ  aᶻ ·ᶻ (cⁿᶻ ·ᶻ bⁿᶻ)) ⊓ ( cᶻ ·ᶻ (bⁿᶻ ·ᶻ aⁿᶻ) ≤ᶻ  bᶻ ·ᶻ (cⁿᶻ ·ᶻ aⁿᶻ)) ≡⟨ ⊓≡⊓ (λ i → cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ) ≤ᶻ  aᶻ ·ᶻ (·ᶻ-comm cⁿᶻ bⁿᶻ i)) (λ i → cᶻ ·ᶻ (·ᶻ-comm bⁿᶻ aⁿᶻ i) ≤ᶻ  bᶻ ·ᶻ (·ᶻ-comm cⁿᶻ aⁿᶻ i)) ⟩
      ( cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ) ≤ᶻ  aᶻ ·ᶻ (bⁿᶻ ·ᶻ cⁿᶻ)) ⊓ ( cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ) ≤ᶻ  bᶻ ·ᶻ (aⁿᶻ ·ᶻ cⁿᶻ)) ≡⟨ sym $ ⇔toPath' $ is-minᶻ (aᶻ ·ᶻ (bⁿᶻ ·ᶻ cⁿᶻ)) (bᶻ ·ᶻ (aⁿᶻ ·ᶻ cⁿᶻ)) (cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ)) ⟩
      ((cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ)) ≤ᶻ  minᶻ ( aᶻ ·ᶻ (bⁿᶻ  ·ᶻ cⁿᶻ)) (bᶻ ·ᶻ (aⁿᶻ  ·ᶻ cⁿᶻ)))                ≡⟨ (λ i → ((cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ)) ≤ᶻ minᶻ (·ᶻ-assoc aᶻ bⁿᶻ cⁿᶻ i) (·ᶻ-assoc bᶻ aⁿᶻ cⁿᶻ i))) ⟩
      ((cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ)) ≤ᶻ  minᶻ ((aᶻ ·ᶻ  bⁿᶻ) ·ᶻ cⁿᶻ) ((bᶻ ·ᶻ  aⁿᶻ) ·ᶻ cⁿᶻ))                 ≡⟨ (λ i → (cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ)) ≤ᶻ ·ᶻ-minᶻ-distribʳ (aᶻ ·ᶻ bⁿᶻ) (bᶻ ·ᶻ aⁿᶻ) cⁿᶻ 0≤cⁿᶻ (~ i)) ⟩
      ((cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ)) ≤ᶻ (minᶻ ( aᶻ ·ᶻ  bⁿᶻ)          (bᶻ ·ᶻ  aⁿᶻ)           ·ᶻ cⁿᶻ))       ∎)

is-max : (x y z : ℚ) → [ (max x y ≤ z) ⇔ (x ≤ z) ⊓ (y ≤ z) ]
is-max = SetQuotient.elimProp3  {R = _∼_} (λ x y z → isProp[] ((max x y ≤ z) ⇔ (x ≤ z) ⊓ (y ≤ z))) γ where
  γ : (a b c : ℤ × ℕ₊₁) → [ (max [ a ]ᶠ [ b ]ᶠ ≤ [ c ]ᶠ) ⇔ ([ a ]ᶠ ≤ [ c ]ᶠ) ⊓ ([ b ]ᶠ ≤ [ c ]ᶠ) ]
  γ a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) c@(cᶻ , cⁿ) = pathTo⇔ (sym κ) where
    aⁿᶻ = [1+ aⁿ ⁿ]ᶻ; 0≤aⁿᶻ : [ 0 ≤ᶻ aⁿᶻ ]; 0≤aⁿᶻ = is-0≤ⁿᶻ
    bⁿᶻ = [1+ bⁿ ⁿ]ᶻ; 0≤bⁿᶻ : [ 0 ≤ᶻ bⁿᶻ ]; 0≤bⁿᶻ = is-0≤ⁿᶻ
    cⁿᶻ = [1+ cⁿ ⁿ]ᶻ; 0≤cⁿᶻ : [ 0 ≤ᶻ cⁿᶻ ]; 0≤cⁿᶻ = is-0≤ⁿᶻ
    κ = ( aᶻ ·ᶻ cⁿᶻ         ≤ᶻ  cᶻ ·ᶻ aⁿᶻ        ) ⊓ ( bᶻ ·ᶻ cⁿᶻ         ≤ᶻ  cᶻ ·ᶻ bⁿᶻ        ) ≡⟨ ⊓≡⊓ (·ᶻ-creates-≤ᶻ-≡ (aᶻ ·ᶻ cⁿᶻ) (cᶻ ·ᶻ aⁿᶻ) bⁿᶻ 0≤bⁿᶻ) (·ᶻ-creates-≤ᶻ-≡ (bᶻ ·ᶻ cⁿᶻ) (cᶻ ·ᶻ bⁿᶻ) aⁿᶻ 0≤aⁿᶻ) ⟩
        ((aᶻ ·ᶻ cⁿᶻ) ·ᶻ bⁿᶻ ≤ᶻ (cᶻ ·ᶻ aⁿᶻ) ·ᶻ bⁿᶻ) ⊓ ((bᶻ ·ᶻ cⁿᶻ) ·ᶻ aⁿᶻ ≤ᶻ (cᶻ ·ᶻ bⁿᶻ) ·ᶻ aⁿᶻ) ≡⟨ ⊓≡⊓ (λ i → ·ᶻ-assoc aᶻ cⁿᶻ bⁿᶻ (~ i) ≤ᶻ ·ᶻ-assoc cᶻ aⁿᶻ bⁿᶻ (~ i)) (λ i → ·ᶻ-assoc bᶻ cⁿᶻ aⁿᶻ (~ i) ≤ᶻ ·ᶻ-assoc cᶻ bⁿᶻ aⁿᶻ (~ i)) ⟩
        (aᶻ ·ᶻ (cⁿᶻ ·ᶻ bⁿᶻ) ≤ᶻ cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ)) ⊓ (bᶻ ·ᶻ (cⁿᶻ ·ᶻ aⁿᶻ) ≤ᶻ cᶻ ·ᶻ (bⁿᶻ ·ᶻ aⁿᶻ)) ≡⟨ ⊓≡⊓ (λ i → aᶻ ·ᶻ ·ᶻ-comm cⁿᶻ bⁿᶻ i ≤ᶻ cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ)) (λ i → bᶻ ·ᶻ ·ᶻ-comm cⁿᶻ aⁿᶻ i ≤ᶻ cᶻ ·ᶻ ·ᶻ-comm bⁿᶻ aⁿᶻ i) ⟩
        (aᶻ ·ᶻ (bⁿᶻ ·ᶻ cⁿᶻ) ≤ᶻ cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ)) ⊓ (bᶻ ·ᶻ (aⁿᶻ ·ᶻ cⁿᶻ) ≤ᶻ cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ)) ≡⟨ sym $ ⇔toPath' $ is-maxᶻ (aᶻ ·ᶻ (bⁿᶻ ·ᶻ cⁿᶻ)) (bᶻ ·ᶻ (aⁿᶻ ·ᶻ cⁿᶻ)) (cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ)) ⟩
        maxᶻ (aᶻ ·ᶻ (bⁿᶻ ·ᶻ cⁿᶻ)) (bᶻ ·ᶻ (aⁿᶻ ·ᶻ cⁿᶻ)) ≤ᶻ cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ)                    ≡⟨ (λ i → maxᶻ (·ᶻ-assoc aᶻ bⁿᶻ cⁿᶻ i) (·ᶻ-assoc bᶻ aⁿᶻ cⁿᶻ i) ≤ᶻ cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ)) ⟩
        maxᶻ ((aᶻ ·ᶻ bⁿᶻ) ·ᶻ cⁿᶻ) ((bᶻ ·ᶻ aⁿᶻ) ·ᶻ cⁿᶻ) ≤ᶻ cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ)                    ≡⟨ (λ i → ·ᶻ-maxᶻ-distribʳ (aᶻ ·ᶻ bⁿᶻ) (bᶻ ·ᶻ aⁿᶻ) cⁿᶻ 0≤cⁿᶻ (~ i) ≤ᶻ cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ)) ⟩
        maxᶻ (aᶻ ·ᶻ bⁿᶻ) (bᶻ ·ᶻ aⁿᶻ) ·ᶻ cⁿᶻ ≤ᶻ cᶻ ·ᶻ (aⁿᶻ ·ᶻ bⁿᶻ) ∎

private
  lem2  : ∀ a b c d → (a ·ᶻ c) ·ᶻ (b ·ᶻ d) ≡ (a ·ᶻ b) ·ᶻ (c ·ᶻ d)
  lem2' : ∀ a b c d → (a ·ᶻ c) ·ᶻ (b ·ᶻ d) ≡ (a ·ᶻ b) ·ᶻ (d ·ᶻ c)
  lem3  : ∀ a b c d → (a ·ᶻ c) ·ᶻ (b ·ᶻ d) ≡ (a ·ᶻ d) ·ᶻ (c ·ᶻ b)
  lem3' : ∀ a b c d → (a ·ᶻ c) ·ᶻ (b ·ᶻ d) ≡ (a ·ᶻ d) ·ᶻ (b ·ᶻ c)

  lem2  a b c d = ·ᶻ-commʳ a c (b ·ᶻ d) ∙ (λ i → ·ᶻ-assoc a b d i ·ᶻ c) ∙ sym (·ᶻ-assoc (a ·ᶻ b) d c) ∙ (λ i → (a ·ᶻ b) ·ᶻ ·ᶻ-comm d c i)
  lem2' a b c d = lem2 a b c d ∙ λ i → (a ·ᶻ b) ·ᶻ ·ᶻ-comm c d i
  lem3  a b c d = (λ i → a ·ᶻ c ·ᶻ ·ᶻ-comm b d i) ∙ sym (·ᶻ-assoc a c (d ·ᶻ b)) ∙ (λ i → a ·ᶻ ·ᶻ-commˡ c d b i) ∙ ·ᶻ-assoc a d (c ·ᶻ b)
  lem3' a b c d = lem3 a b c d ∙ λ i → (a ·ᶻ d) ·ᶻ ·ᶻ-comm c b i

·-preserves-< : (x y z : ℚ) → [ 0 < z ] → [ x < y ] → [ x · z < y · z ]
·-preserves-< = SetQuotient.elimProp3 {R = _∼_} (λ x y z → isProp[] ((0 < z) ⇒ (x < y) ⇒ (x · z < y · z))) γ where
  γ : (a b c : ℤ × ℕ₊₁) → [ 0 < [ c ]ᶠ ] → [ [ a ]ᶠ < [ b ]ᶠ ] → [ [ a ]ᶠ · [ c ]ᶠ < [ b ]ᶠ · [ c ]ᶠ ]
  γ a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) c@(cᶻ , cⁿ) = κ where
    aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
    bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
    cⁿᶻ = [1+ cⁿ ⁿ]ᶻ; 0<cⁿᶻ : [ 0 <ᶻ cⁿᶻ ]; 0<cⁿᶻ = is-0<ⁿᶻ
    κ : [ 0 ·ᶻ cⁿᶻ <ᶻ cᶻ ·ᶻ 1 ] → [ aᶻ ·ᶻ bⁿᶻ <ᶻ bᶻ ·ᶻ aⁿᶻ ] → [ (aᶻ ·ᶻ cᶻ) ·ᶻ (bⁿᶻ ·ᶻ cⁿᶻ) <ᶻ (bᶻ ·ᶻ cᶻ) ·ᶻ (aⁿᶻ ·ᶻ cⁿᶻ) ]
    κ p q = transport (λ i → [ lem2 aᶻ bⁿᶻ cᶻ cⁿᶻ (~ i) <ᶻ lem2 bᶻ aⁿᶻ cᶻ cⁿᶻ (~ i) ]) $ ·ᶻ-preserves-<ᶻ (aᶻ ·ᶻ bⁿᶻ) (bᶻ ·ᶻ aⁿᶻ) (cᶻ ·ᶻ cⁿᶻ) 0<cᶻ·cⁿᶻ q where
      0<cᶻ : [ 0 <ᶻ cᶻ ]
      0<cᶻ = transport (λ i → [ ·ᶻ-nullifiesˡ cⁿᶻ i <ᶻ ·ᶻ-identity cᶻ .fst i ]) p
      0<cᶻ·cⁿᶻ : [ 0 <ᶻ (cᶻ ·ᶻ cⁿᶻ) ]
      0<cᶻ·cⁿᶻ = ·ᶻ-preserves-0<ᶻ cᶻ cⁿᶻ 0<cᶻ 0<cⁿᶻ

private
  -- continuing the pattern...
  elimProp4 : ∀{ℓ} {A : Type ℓ} → {R : A → A → Type ℓ}
            → {E : A SetQuotient./ R → A SetQuotient./ R → A SetQuotient./ R → A SetQuotient./ R → Type ℓ}
            → ((x y z w : A SetQuotient./ R ) → isProp (E x y z w))
            → ((a b c d : A) → E SetQuotient.[ a ] SetQuotient.[ b ] SetQuotient.[ c ] SetQuotient.[ d ])
            → (x y z w : A SetQuotient./ R)
            → E x y z w
  elimProp4 Eprop f = SetQuotient.elimProp (λ x → isPropΠ3 (λ y z w → Eprop x y z w))
                                           (λ x → SetQuotient.elimProp3 (λ y z w → Eprop SetQuotient.[ x ] y z w) (f x))

open import Cubical.HITs.Rationals.QuoQ using
  ( _+_
  ; -_
  ; +-assoc
  ; +-comm
  ; +-identityˡ
  ; +-identityʳ
  ; +-inverseˡ
  ; +-inverseʳ
  ) renaming
  ( *-identityˡ to ·-identityˡ
  ; *-identityʳ to ·-identityʳ
  ; *-distribˡ  to ·-distribˡ
  ; *-distribʳ  to ·-distribʳ
  )

-- the following hold definitionally:
--       [ aᶻ , aⁿ ]ᶠ · [ bᶻ , bⁿ ]ᶠ ≡ [ aᶻ · bᶻ , aⁿ ·₊₁ bⁿ ]ᶠ
--       [ aᶻ , aⁿ ]ᶠ < [ bᶻ , bⁿ ]ᶠ ≡ aᶻ ·ᶻ bⁿᶻ <ᶻ bᶻ ·ᶻ aⁿᶻ
--   min [ aᶻ , aⁿ ]ᶠ   [ bᶻ , bⁿ ]ᶠ ≡ [ (minᶻ (aᶻ ·ᶻ bⁿᶻ) (bᶻ ·ᶻ aⁿᶻ) , aⁿ ·₊₁ bⁿ) ]ᶠ
--       [ aᶻ , aⁿ ]ᶠ + [ bᶻ , bⁿ ]ᶠ ≡ [ aᶻ ·ᶻ bⁿᶻ +ᶻ bᶻ ·ᶻ aⁿᶻ , aⁿ ·₊₁ bⁿ ]ᶠ

+-<-ext : (w x y z : ℚ) → [ w + x < y + z ] → [ (w < y) ⊔ (x < z) ]
+-<-ext = elimProp4 {R = _∼_} (λ w x y z → isProp[] ((w + x < y + z) ⇒ ((w < y) ⊔ (x < z)))) γ where
  γ : (w x y z : ℤ × ℕ₊₁) → [ [ w ]ᶠ + [ x ]ᶠ < [ y ]ᶠ + [ z ]ᶠ ] → [ ([ w ]ᶠ < [ y ]ᶠ) ⊔ ([ x ]ᶠ < [ z ]ᶠ) ]
  γ w@(wᶻ , wⁿ) x@(xᶻ , xⁿ) y@(yᶻ , yⁿ) z@(zᶻ , zⁿ) = κ where
    wⁿᶻ = [1+ wⁿ ⁿ]ᶻ; 0<wⁿᶻ : [ 0 <ᶻ wⁿᶻ ]; 0<wⁿᶻ = is-0<ⁿᶻ
    xⁿᶻ = [1+ xⁿ ⁿ]ᶻ; 0<xⁿᶻ : [ 0 <ᶻ xⁿᶻ ]; 0<xⁿᶻ = is-0<ⁿᶻ
    yⁿᶻ = [1+ yⁿ ⁿ]ᶻ; 0<yⁿᶻ : [ 0 <ᶻ yⁿᶻ ]; 0<yⁿᶻ = is-0<ⁿᶻ
    zⁿᶻ = [1+ zⁿ ⁿ]ᶻ; 0<zⁿᶻ : [ 0 <ᶻ zⁿᶻ ]; 0<zⁿᶻ = is-0<ⁿᶻ
    0<xzⁿᶻ : [ 0 <ᶻ xⁿᶻ ·ᶻ zⁿᶻ ]; 0<xzⁿᶻ = ·ᶻ-preserves-0<ᶻ xⁿᶻ zⁿᶻ 0<xⁿᶻ 0<zⁿᶻ
    0<wyⁿᶻ : [ 0 <ᶻ wⁿᶻ ·ᶻ yⁿᶻ ]; 0<wyⁿᶻ = ·ᶻ-preserves-0<ᶻ wⁿᶻ yⁿᶻ 0<wⁿᶻ 0<yⁿᶻ
    φ₁ = wᶻ ·ᶻ xⁿᶻ ·ᶻ (yⁿᶻ ·ᶻ zⁿᶻ) ≡⟨ lem2  wᶻ yⁿᶻ xⁿᶻ zⁿᶻ ⟩ wᶻ ·ᶻ yⁿᶻ ·ᶻ (xⁿᶻ ·ᶻ zⁿᶻ) ∎
    φ₂ = xᶻ ·ᶻ wⁿᶻ ·ᶻ (yⁿᶻ ·ᶻ zⁿᶻ) ≡⟨ lem3  xᶻ yⁿᶻ wⁿᶻ zⁿᶻ ⟩ xᶻ ·ᶻ zⁿᶻ ·ᶻ (wⁿᶻ ·ᶻ yⁿᶻ) ∎
    φ₃ = yᶻ ·ᶻ zⁿᶻ ·ᶻ (wⁿᶻ ·ᶻ xⁿᶻ) ≡⟨ lem2' yᶻ wⁿᶻ zⁿᶻ xⁿᶻ ⟩ yᶻ ·ᶻ wⁿᶻ ·ᶻ (xⁿᶻ ·ᶻ zⁿᶻ) ∎
    φ₄ = zᶻ ·ᶻ yⁿᶻ ·ᶻ (wⁿᶻ ·ᶻ xⁿᶻ) ≡⟨ lem3' zᶻ wⁿᶻ yⁿᶻ xⁿᶻ ⟩ zᶻ ·ᶻ xⁿᶻ ·ᶻ (wⁿᶻ ·ᶻ yⁿᶻ) ∎
    φ = (    (wᶻ ·ᶻ xⁿᶻ +ᶻ xᶻ ·ᶻ wⁿᶻ) ·ᶻ (yⁿᶻ ·ᶻ zⁿᶻ)
          <ᶻ (yᶻ ·ᶻ zⁿᶻ +ᶻ zᶻ ·ᶻ yⁿᶻ) ·ᶻ (wⁿᶻ ·ᶻ xⁿᶻ) ⇒ᵖ⟨ transport (λ i → [ is-distᶻ (wᶻ ·ᶻ xⁿᶻ) (xᶻ ·ᶻ wⁿᶻ) (yⁿᶻ ·ᶻ zⁿᶻ) .snd i <ᶻ is-distᶻ (yᶻ ·ᶻ zⁿᶻ) (zᶻ ·ᶻ yⁿᶻ) (wⁿᶻ ·ᶻ xⁿᶻ) .snd i ]) ⟩
             wᶻ ·ᶻ xⁿᶻ ·ᶻ (yⁿᶻ ·ᶻ zⁿᶻ) +ᶻ xᶻ ·ᶻ wⁿᶻ ·ᶻ (yⁿᶻ ·ᶻ zⁿᶻ)
          <ᶻ yᶻ ·ᶻ zⁿᶻ ·ᶻ (wⁿᶻ ·ᶻ xⁿᶻ) +ᶻ zᶻ ·ᶻ yⁿᶻ ·ᶻ (wⁿᶻ ·ᶻ xⁿᶻ) ⇒ᵖ⟨ transport (λ i → [ φ₁ i +ᶻ φ₂ i <ᶻ φ₃ i +ᶻ φ₄ i ]) ⟩
             wᶻ ·ᶻ yⁿᶻ ·ᶻ (xⁿᶻ ·ᶻ zⁿᶻ) +ᶻ xᶻ ·ᶻ zⁿᶻ ·ᶻ (wⁿᶻ ·ᶻ yⁿᶻ)
          <ᶻ yᶻ ·ᶻ wⁿᶻ ·ᶻ (xⁿᶻ ·ᶻ zⁿᶻ) +ᶻ zᶻ ·ᶻ xⁿᶻ ·ᶻ (wⁿᶻ ·ᶻ yⁿᶻ) ◼ᵖ) .snd
    P₁ = wᶻ ·ᶻ yⁿᶻ ·ᶻ (xⁿᶻ ·ᶻ zⁿᶻ) <ᶻ yᶻ ·ᶻ wⁿᶻ ·ᶻ (xⁿᶻ ·ᶻ zⁿᶻ)
    P₂ = xᶻ ·ᶻ zⁿᶻ ·ᶻ (wⁿᶻ ·ᶻ yⁿᶻ) <ᶻ zᶻ ·ᶻ xⁿᶻ ·ᶻ (wⁿᶻ ·ᶻ yⁿᶻ)
    Q₁ = wᶻ ·ᶻ yⁿᶻ <ᶻ yᶻ ·ᶻ wⁿᶻ
    Q₂ = xᶻ ·ᶻ zⁿᶻ <ᶻ zᶻ ·ᶻ xⁿᶻ
    ψ = +ᶻ-<ᶻ-ext (wᶻ ·ᶻ yⁿᶻ ·ᶻ (xⁿᶻ ·ᶻ zⁿᶻ)) (xᶻ ·ᶻ zⁿᶻ ·ᶻ (wⁿᶻ ·ᶻ yⁿᶻ)) (yᶻ ·ᶻ wⁿᶻ ·ᶻ (xⁿᶻ ·ᶻ zⁿᶻ)) (zᶻ ·ᶻ xⁿᶻ ·ᶻ (wⁿᶻ ·ᶻ yⁿᶻ))
    κ : [ (wᶻ ·ᶻ xⁿᶻ +ᶻ xᶻ ·ᶻ wⁿᶻ) ·ᶻ (yⁿᶻ ·ᶻ zⁿᶻ) <ᶻ (yᶻ ·ᶻ zⁿᶻ +ᶻ zᶻ ·ᶻ yⁿᶻ) ·ᶻ (wⁿᶻ ·ᶻ xⁿᶻ) ]
      → [ Q₁ ⊔ Q₂ ]
    κ p =  case ψ (φ p) as P₁ ⊔ P₂ ⇒ (Q₁ ⊔ Q₂) of λ
      { (inl q) → inlᵖ (·ᶻ-reflects-<ᶻ (wᶻ ·ᶻ yⁿᶻ) (yᶻ ·ᶻ wⁿᶻ) (xⁿᶻ ·ᶻ zⁿᶻ) 0<xzⁿᶻ q)
      ; (inr q) → inrᵖ (·ᶻ-reflects-<ᶻ (xᶻ ·ᶻ zⁿᶻ) (zᶻ ·ᶻ xⁿᶻ) (wⁿᶻ ·ᶻ yⁿᶻ) 0<wyⁿᶻ q)
      }

+-Semigroup : [ isSemigroup _+_ ]
+-Semigroup .IsSemigroup.is-set   = isSetℚ
+-Semigroup .IsSemigroup.is-assoc = +-assoc

·-Semigroup : [ isSemigroup _·_ ]
·-Semigroup .IsSemigroup.is-set   = isSetℚ
·-Semigroup .IsSemigroup.is-assoc = ·-assoc

+-Monoid : [ isMonoid 0 _+_ ]
+-Monoid .IsMonoid.is-Semigroup  = +-Semigroup
+-Monoid .IsMonoid.is-identity x = +-identityʳ x , +-identityˡ x

·-Monoid : [ isMonoid 1 _·_ ]
·-Monoid .IsMonoid.is-Semigroup  = ·-Semigroup
·-Monoid .IsMonoid.is-identity x = ·-identityʳ x , ·-identityˡ x

is-Semiring : [ isSemiring 0 1 _+_ _·_ ]
is-Semiring .IsSemiring.+-Monoid = +-Monoid
is-Semiring .IsSemiring.·-Monoid = ·-Monoid
is-Semiring .IsSemiring.+-comm   = +-comm
is-Semiring .IsSemiring.is-dist x y z = sym (·-distribˡ x y z) , sym (·-distribʳ x y z)

is-CommSemiring : [ isCommSemiring 0 1 _+_ _·_ ]
is-CommSemiring .IsCommSemiring.is-Semiring = is-Semiring
is-CommSemiring .IsCommSemiring.·-comm      = ·-comm

≤-Lattice : [ isLattice _≤_ min max ]
≤-Lattice .IsLattice.≤-PartialOrder = linearorder⇒partialorder _ (≤'-isLinearOrder <-StrictLinearOrder)
≤-Lattice .IsLattice.is-min         = is-min
≤-Lattice .IsLattice.is-max         = is-max

is-LinearlyOrderedCommSemiring : [ isLinearlyOrderedCommSemiring 0 1 _+_ _·_ _<_ min max ]
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.is-CommSemiring     = is-CommSemiring
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.<-StrictLinearOrder = <-StrictLinearOrder
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.≤-Lattice           = ≤-Lattice
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.+-<-ext             = +-<-ext
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.·-preserves-<       = ·-preserves-<

+-inverse : (x : ℚ) → (x + (- x) ≡ 0) × ((- x) + x ≡ 0)
+-inverse x .fst = +-inverseʳ x
+-inverse x .snd = +-inverseˡ x

is-LinearlyOrderedCommRing : [ isLinearlyOrderedCommRing 0 1 _+_ _·_ -_ _<_ min max ]
is-LinearlyOrderedCommRing. IsLinearlyOrderedCommRing.is-LinearlyOrderedCommSemiring = is-LinearlyOrderedCommSemiring
is-LinearlyOrderedCommRing. IsLinearlyOrderedCommRing.+-inverse                      = +-inverse

is-LinearlyOrderedField : [ isLinearlyOrderedField 0 1 _+_ _·_ -_ _<_ min max ]
is-LinearlyOrderedField .IsLinearlyOrderedField.is-LinearlyOrderedCommRing = is-LinearlyOrderedCommRing
is-LinearlyOrderedField .IsLinearlyOrderedField.·-inv''                    = ·-inv''

ℚbundle : LinearlyOrderedField {ℓ-zero} {ℓ-zero}
ℚbundle .LinearlyOrderedField.Carrier                  = ℚ
ℚbundle .LinearlyOrderedField.0f                       = 0
ℚbundle .LinearlyOrderedField.1f                       = 1
ℚbundle .LinearlyOrderedField._+_                      = _+_
ℚbundle .LinearlyOrderedField.-_                       = -_
ℚbundle .LinearlyOrderedField._·_                      = _·_
ℚbundle .LinearlyOrderedField.min                      = min
ℚbundle .LinearlyOrderedField.max                      = max
ℚbundle .LinearlyOrderedField._<_                      = _<_
ℚbundle .LinearlyOrderedField.is-LinearlyOrderedField  = is-LinearlyOrderedField

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
{-# OPTIONS --cubical #-}
module ExerciseSession2 where

open import Part1
open import Part2
open import Part3
open import Part4

    -- (* Construct a point if isContr A → Π (x y : A) . isContr (x = y) *)

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

foo : isProp A → isProp' A
foo h = λ x y → (h x y) , λ q → isProp→isSet h _ _ (h x y) q

-- hProp : {ℓ : Level} → Type (ℓ-suc ℓ)
-- hProp {ℓ = ℓ} = Σ[ A ∈ Type ℓ ] isProp A

-- foo : isContr (Σ[ A ∈ hProp {ℓ = ℓ} ] (fst A))
-- foo = ({!!} , {!!}) , {!!}

-- Σ≡Prop : ((x : A) → isProp (B x)) → {u v : Σ A B}
--        → (p : u .fst ≡ v .fst) → u ≡ v

ext: agda


text:
module #5 where

open import Relation.Binary.PropositionalEquality
open import Function
open import Level

ind₌ : ∀{a b}{A : Set a} → (C : (x y : A) → (x ≡ y) → Set b) → ((x : A) → C x x refl) → {x y : A} → (p : x ≡ y) → C x y p
ind₌ C c {x}{y} p rewrite p = c y

transport : ∀ {i} {A : Set i}{P : A → Set i}{x y : A} → (p : x ≡ y) → (P x → P y)
transport {i} {A}{P} {x}{y} p = ind₌ D d p where
    D : (x y : A) → (p : x ≡ y) → Set i
    D x y p = P x → P y

    d : (x : A) → D x x refl
    d = λ x → id

record IsEquiv {i j}{A : Set i}{B : Set j}(to : A → B) : Set (i ⊔ j) where
  field
    from : B → A
    iso₁ : (x : A) → from (to x) ≡ x
    iso₂ : (y : B) → to (from y) ≡ y

{-
  Exercise 2.5. Prove that the functions (2.3.6) and (2.3.7) are inverse equivalences.
-}

lem2-3-6 : ∀ {i} {A B : Set i}{x y : A} → (p : x ≡ y) → (f : A → B) → (f x ≡ f y) → (transport p (f x) ≡ f y)
lem2-3-6 p f q rewrite p = refl

lem2-3-7 : ∀ {i} {A B : Set i}{x y : A} → (p : x ≡ y) → (f : A → B) → (transport p (f x) ≡ f y) → (f x ≡ f y)
lem2-3-7 p f q rewrite p = refl

lems-is-equiv : ∀ {i} {A B : Set i}{x y : A} → (p : x ≡ y) → (f : A → B) → IsEquiv (lem2-3-6 p f)
lems-is-equiv p f = record
  { from = lem2-3-7 p f
  ; iso₁ = λ x → {!!}
  ; iso₂ = λ y → {!!}
  }

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
module Parity where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ -> ℕ

infixl 60 _+_
infixl 70 _*_

_+_ : ℕ -> ℕ -> ℕ
n + zero  = n
n + suc m = suc (n + m)

_*_ : ℕ -> ℕ -> ℕ
n * zero  = zero
n * suc m = n * m + n

{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC suc #-}
{-# BUILTIN NATPLUS _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}

data Parity : ℕ -> Set where
  itsEven : (k : ℕ) -> Parity (2 * k)
  itsOdd  : (k : ℕ) -> Parity (2 * k + 1)

parity : (n : ℕ) -> Parity n
parity  zero              = itsEven zero
parity (suc n)         with parity n
parity (suc .(2 * k))     | itsEven k = itsOdd k
parity (suc .(2 * k + 1)) | itsOdd  k = itsEven (k + 1)

half : ℕ -> ℕ
half n         with parity n
half .(2 * k)     | itsEven k = k
half .(2 * k + 1) | itsOdd  k = k

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
{-# OPTIONS --sized-types #-}

open import FRP.JS.Array using ( ⟨⟩ ; ⟨_ ; _,_ ; _⟩ )
open import FRP.JS.Bool using ( Bool ; true ; false ; not )
open import FRP.JS.JSON using ( JSON ; float ; bool ; string ; object ; array ; null ; parse ; _≟_ )
open import FRP.JS.Maybe using ( Maybe ; just ; nothing ; _≟[_]_ )
open import FRP.JS.Object using ( ⟪_ ; _↦_⟫ ; _↦_,_ )
open import FRP.JS.QUnit using ( TestSuite ; test ; ok ; ok! ; _,_ )

module FRP.JS.Test.JSON where

⟨1⟩       = array (⟨ float 1.0 ⟩)
⟨n⟩       = array (⟨ null ⟩)
⟨1,n⟩     = array (⟨ float 1.0 , null ⟩)
⟨n,1⟩     = array (⟨ null , float 1.0 ⟩)
⟨⟨1⟩⟩     = array (⟨ ⟨1⟩ ⟩)
⟪a↦1⟫     = object (⟪ "a" ↦ float 1.0 ⟫)
⟪b↦n⟫     = object (⟪ "b" ↦ null ⟫)
⟪a↦1,b↦n⟫ = object (⟪ "a" ↦ float 1.0 , "b" ↦ null ⟫)
⟪a↦⟪a↦1⟫⟫ = object (⟪ "a" ↦ ⟪a↦1⟫ ⟫)
⟪a↦⟨1⟩⟫   = object (⟪ "a" ↦ ⟨1⟩ ⟫)
⟨⟪a↦1⟫⟩   = array (⟨ ⟪a↦1⟫ ⟩)

_≟?_ : Maybe JSON → Maybe JSON → Bool
j ≟? k = j ≟[ _≟_ ] k

tests : TestSuite
tests =
  ( test "≟"
    ( ok "n ≟ n" (null ≟ null)
    , ok "a ≟ a" (string "a" ≟ string "a")
    , ok "t ≟ t" (bool true ≟ bool true)
    , ok "f ≟ f" (bool false ≟ bool false)
    , ok "1 ≟ 1" (float 1.0 ≟ float 1.0)
    , ok "2 ≟ 2" (float 2.0 ≟ float 2.0)
    , ok "⟨1⟩ ≟ ⟨1⟩" (⟨1⟩ ≟ ⟨1⟩)
    , ok "⟨n⟩ ≟ ⟨n⟩" (⟨n⟩ ≟ ⟨n⟩)
    , ok "⟨1,n⟩ ≟ ⟨1,n⟩" (⟨1,n⟩ ≟ ⟨1,n⟩)
    , ok "⟪a↦1⟫ ≟ ⟪a↦1⟫" (⟪a↦1⟫ ≟ ⟪a↦1⟫)
    , ok "⟪b↦n⟫ ≟ ⟪b↦n⟫" (⟪b↦n⟫ ≟ ⟪b↦n⟫)
    , ok "⟪a↦1,b↦n⟫ ≟ ⟪a↦1,b↦n⟫" (⟪a↦1,b↦n⟫ ≟ ⟪a↦1,b↦n⟫)
    , ok "⟪a↦⟪a↦1⟫⟫ ≟ ⟪a↦⟪a↦1⟫⟫" (⟪a↦⟪a↦1⟫⟫ ≟ ⟪a↦⟪a↦1⟫⟫)
    , ok "⟪a↦⟨1⟩⟫ ≟ ⟪a↦⟨1⟩⟫" (⟪a↦⟨1⟩⟫ ≟ ⟪a↦⟨1⟩⟫)
    , ok "⟨⟪a↦1⟫⟩ ≟ ⟨⟪a↦1⟫⟩" (⟨⟪a↦1⟫⟩ ≟ ⟨⟪a↦1⟫⟩)
    , ok "n ≟ a" (not (null ≟ string "a"))
    , ok "n ≟ 'n'" (not (null ≟ string "null"))
    , ok "n ≟ f" (not (null ≟ bool false))
    , ok "n ≟ 0" (not (null ≟ float 0.0))
    , ok "a ≟ b" (not (string "a" ≟ string "b"))
    , ok "a ≟ A" (not (string "a" ≟ string "A"))
    , ok "t ≟ 't'" (not (string "true" ≟ bool true))
    , ok "1 ≟ '1'" (not (string "1.0" ≟ float 1.0))
    , ok "t ≟ f" (not (bool true ≟ bool false))
    , ok "f ≟ 0" (not (bool false ≟ float 0.0))
    , ok "1 ≟ 2" (not (float 1.0 ≟ float 2.0))
    , ok "⟨1⟩ ≟ ⟨n⟩" (not (⟨1⟩ ≟ ⟨n⟩))
    , ok "⟨1⟩ ≟ ⟨1,n⟩" (not (⟨1⟩ ≟ ⟨1,n⟩))
    , ok "⟨1,n⟩ ≟ ⟨n,1⟩" (not (⟨1,n⟩ ≟ ⟨n,1⟩))
    , ok "⟪a↦1⟫ ≟ ⟪b↦n⟫" (not (⟪a↦1⟫ ≟ ⟪b↦n⟫))
    , ok "⟪a↦1⟫ ≟ ⟪a↦1,b↦n⟫" (not (⟪a↦1⟫ ≟ ⟪a↦1,b↦n⟫))
    , ok "⟪a↦⟪a↦1⟫⟫ ≟ ⟪a↦1⟫" (not (⟪a↦⟪a↦1⟫⟫ ≟ ⟪a↦1⟫))
    , ok "⟪a↦⟨1⟩⟫ ≟ ⟪a↦1⟫" (not (⟪a↦⟨1⟩⟫ ≟ ⟪a↦1⟫))
    , ok "⟨⟪a↦1⟫⟩ ≟ ⟪a↦1⟫" (not (⟨⟪a↦1⟫⟩ ≟ ⟪a↦1⟫)) )
  , test "parse"
    ( ok! "parse n" (parse "null" ≟? just null)
    , ok! "parse a" (parse "\"a\"" ≟? just (string "a"))
    , ok! "parse a" (parse "true" ≟? just (bool true))
    , ok! "parse a" (parse "false" ≟? just (bool false))
    , ok! "parse a" (parse "1" ≟? just (float 1.0))
    , ok! "parse a" (parse "1.0" ≟? just (float 1.0))
    , ok! "parse ⟨1⟩" (parse "[1]" ≟? just ⟨1⟩)
    , ok! "parse ⟨n⟩" (parse "[null]" ≟? just ⟨n⟩)
    , ok! "parse ⟨1,n⟩" (parse "[1,null]" ≟? just ⟨1,n⟩)
    , ok! "parse ⟨n,1⟩" (parse "[null,1]" ≟? just ⟨n,1⟩)
    , ok! "parse ⟨⟨1⟩⟩" (parse "[[1]]" ≟? just ⟨⟨1⟩⟩)
    , ok! "parse ⟪a↦1⟫" (parse "{\"a\":1}" ≟? just ⟪a↦1⟫)
    , ok! "parse ⟪b↦n⟫" (parse "{\"b\":null}" ≟? just ⟪b↦n⟫)
    , ok! "parse ⟪a↦1,b↦n⟫" (parse "{\"a\":1,\"b\":null}" ≟? just ⟪a↦1,b↦n⟫)
    , ok! "parse ⟪a↦⟪a↦1⟫⟫" (parse "{\"a\":{\"a\":1}}" ≟? just ⟪a↦⟪a↦1⟫⟫)
    , ok! "parse ⟪a↦⟨1⟩⟫" (parse "{\"a\":[1]}" ≟? just ⟪a↦⟨1⟩⟫)
    , ok! "parse ⟨⟪a↦1⟫⟩" (parse "[{\"a\":1}]" ≟? just ⟨⟪a↦1⟫⟩)
    , ok! "parse ⟨⟪a↦1⟫⟩" (parse "][" ≟? nothing ) ) )

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
------------------------------------------------------------------------
-- A variant of the lens type in
-- Lens.Non-dependent.Higher.Capriotti.Variant.Erased
--
-- This variant uses ∥_∥ᴱ instead of ∥_∥.
------------------------------------------------------------------------

import Equality.Path as P

module Lens.Non-dependent.Higher.Capriotti.Variant.Erased.Variant
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J as B using (_↔_)
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq
  using (_≃_; Is-equivalence)
open import Equivalence.Erased.Cubical eq as EEq using (_≃ᴱ_)
open import Equivalence.Erased.Contractible-preimages.Cubical eq as ECP
  using (_⁻¹ᴱ_; Contractibleᴱ)
open import Erased.Cubical eq
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as PT using (∥_∥; ∣_∣)
open import H-level.Truncation.Propositional.Erased eq as T
  using (∥_∥ᴱ; ∣_∣)
open import Preimage equality-with-J using (_⁻¹_)
open import Univalence-axiom equality-with-J

open import Lens.Non-dependent eq
import Lens.Non-dependent.Higher.Erased eq as Higher
import Lens.Non-dependent.Higher.Capriotti.Variant eq as V

private
  variable
    a b p q  : Level
    A B      : Type a
    P Q      : A → Type p
    b₁ b₂ b₃ : A
    f        : (x : A) → P x

------------------------------------------------------------------------
-- Coherently-constant

-- Coherently constant type-valued functions.

Coherently-constant :
  {A : Type a} → (A → Type p) → Type (a ⊔ lsuc p)
Coherently-constant {p = p} {A = A} P =
  ∃ λ (Q : ∥ A ∥ᴱ → Type p) →
    (∀ x → P x ≃ᴱ Q ∣ x ∣) ×
    ∃ λ (Q→Q : ∀ x y → Q x → Q y) →
      Erased (∀ x y → Q→Q x y ≡
                      subst Q (T.truncation-is-proposition x y))

-- The "last part" of Coherently-constant is contractible (in erased
-- contexts).

@0 Contractible-last-part-of-Coherently-constant :
  Contractible
    (∃ λ (Q→Q : ∀ x y → Q x → Q y) →
     Erased (∀ x y → Q→Q x y ≡
                     subst Q (T.truncation-is-proposition x y)))
Contractible-last-part-of-Coherently-constant {Q = Q} =           $⟨ Contractibleᴱ-Erased-singleton ⟩
  Contractibleᴱ
    (∃ λ (Q→Q : ∀ x y → Q x → Q y) →
     Erased (Q→Q ≡ λ x y →
                   subst Q (T.truncation-is-proposition x y)))    ↝⟨ (ECP.Contractibleᴱ-cong _ $
                                                                      ∃-cong λ _ → Erased-cong (inverse $
                                                                      Eq.extensionality-isomorphism ext F.∘
                                                                      ∀-cong ext λ _ → Eq.extensionality-isomorphism ext)) ⦂ (_ → _) ⟩
  Contractibleᴱ
    (∃ λ (Q→Q : ∀ x y → Q x → Q y) →
     Erased (∀ x y → Q→Q x y ≡
                     subst Q (T.truncation-is-proposition x y)))  ↝⟨ ECP.Contractibleᴱ→Contractible ⟩□

  Contractible
    (∃ λ (Q→Q : ∀ x y → Q x → Q y) →
     Erased (∀ x y → Q→Q x y ≡
                     subst Q (T.truncation-is-proposition x y)))  □

-- In erased contexts Coherently-constant P is equivalent to
-- V.Coherently-constant P.

@0 Coherently-constant≃Variant-coherently-constant :
  {P : A → Type p} →
  Coherently-constant P ≃ V.Coherently-constant P
Coherently-constant≃Variant-coherently-constant {A = A} {P = P} =
  (∃ λ (Q : ∥ A ∥ᴱ → _) → (∀ x → P x ≃ᴱ Q ∣ x ∣) × _)  ↔⟨ (∃-cong λ _ → drop-⊤-right λ _ →
                                                           _⇔_.to contractible⇔↔⊤
                                                           Contractible-last-part-of-Coherently-constant) ⟩
  (∃ λ (Q : ∥ A ∥ᴱ → _) → ∀ x → P x ≃ᴱ Q ∣ x ∣)        ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ → inverse
                                                           EEq.≃≃≃ᴱ) ⟩
  (∃ λ (Q : ∥ A ∥ᴱ → _) → ∀ x → P x ≃  Q ∣ x ∣)        ↝⟨ (Σ-cong {k₁ = equivalence} (→-cong₁ ext PT.∥∥ᴱ≃∥∥) λ _ → F.id) ⟩□
  (∃ λ (Q : ∥ A ∥  → _) → ∀ x → P x ≃  Q ∣ x ∣)        □

-- In erased contexts Coherently-constant (f ⁻¹ᴱ_) is equivalent to
-- V.Coherently-constant (f ⁻¹_).

@0 Coherently-constant-⁻¹ᴱ≃Variant-coherently-constant-⁻¹ :
  Coherently-constant (f ⁻¹ᴱ_) ≃ V.Coherently-constant (f ⁻¹_)
Coherently-constant-⁻¹ᴱ≃Variant-coherently-constant-⁻¹ {f = f} =
  Coherently-constant (f ⁻¹ᴱ_)        ↝⟨ Coherently-constant≃Variant-coherently-constant ⟩
  V.Coherently-constant (f ⁻¹ᴱ_)      ↔⟨⟩
  (∃ λ Q → ∀ x → f ⁻¹ᴱ x ≃  Q ∣ x ∣)  ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ →
                                          Eq.≃-preserves ext (inverse ECP.⁻¹≃⁻¹ᴱ) F.id) ⟩
  (∃ λ Q → ∀ x → f ⁻¹ x ≃  Q ∣ x ∣)   ↔⟨⟩
  V.Coherently-constant (f ⁻¹_)       □

-- A variant of Coherently-constant.

Coherently-constant′ :
  {A : Type a} → (A → Type p) → Type (a ⊔ lsuc p)
Coherently-constant′ {p = p} {A = A} P =
  ∃ λ (P→P : ∀ x y → P x → P y) →
  ∃ λ (Q : ∥ A ∥ᴱ → Type p) →
  ∃ λ (P≃Q : ∀ x → P x ≃ᴱ Q ∣ x ∣) →
  Erased (P→P ≡
          λ x y →
          _≃ᴱ_.from (P≃Q y) ∘
          subst Q (T.truncation-is-proposition ∣ x ∣ ∣ y ∣) ∘
          _≃ᴱ_.to (P≃Q x))

-- Coherently-constant and Coherently-constant′ are pointwise
-- equivalent (with erased proofs).

Coherently-constant≃ᴱCoherently-constant′ :
  Coherently-constant P ≃ᴱ Coherently-constant′ P
Coherently-constant≃ᴱCoherently-constant′ {P = P} =
  (∃ λ Q →
   (∀ x → P x ≃ᴱ Q ∣ x ∣) ×
   ∃ λ (Q→Q : ∀ x y → Q x → Q y) →
   Erased (∀ x y → Q→Q x y ≡ subst Q (T.truncation-is-proposition x y)))  ↝⟨ lemma ⟩

  (∃ λ Q →
   ∃ λ (P≃Q : ∀ x → P x ≃ᴱ Q ∣ x ∣) →
   ∃ λ (P→P : ∀ x y → P x → P y) →
   Erased (P→P ≡
           λ x y →
           _≃ᴱ_.from (P≃Q y) ∘
           subst Q (T.truncation-is-proposition ∣ x ∣ ∣ y ∣) ∘
           _≃ᴱ_.to (P≃Q x)))                                              ↔⟨ ∃-comm F.∘
                                                                             (∃-cong λ _ → ∃-comm) ⟩□
  (∃ λ (P→P : ∀ x y → P x → P y) →
   ∃ λ Q →
   ∃ λ (P≃Q : ∀ x → P x ≃ᴱ Q ∣ x ∣) →
   Erased (P→P ≡
           λ x y →
           _≃ᴱ_.from (P≃Q y) ∘
           subst Q (T.truncation-is-proposition ∣ x ∣ ∣ y ∣) ∘
           _≃ᴱ_.to (P≃Q x)))                                              □
  where
  lemma =
    ∃-cong λ Q → ∃-cong λ P≃Q →

    (∃ λ (Q→Q : ∀ x y → Q x → Q y) →
     Erased (∀ x y →
             Q→Q x y ≡ subst Q (T.truncation-is-proposition x y)))        ↔⟨ (∀-cong ext λ _ → ∃-cong λ _ → Erased-cong (from-equivalence $
                                                                              Eq.extensionality-isomorphism bad-ext)) F.∘
                                                                             inverse ΠΣ-comm F.∘
                                                                             (∃-cong λ _ → Erased-Π↔Π) ⟩
    (∀ x →
     ∃ λ (Q→Q : ∀ y → Q x → Q y) →
     Erased (Q→Q ≡ λ y → subst Q (T.truncation-is-proposition x y)))      ↔⟨ (∀-cong ext λ _ →
                                                                              T.Σ-Π-∥∥ᴱ-Erased-≡-≃) ⟩
    (∀ x →
     ∃ λ (Q→Q : ∀ y → Q x → Q ∣ y ∣) →
     Erased (Q→Q ≡ λ y → subst Q (T.truncation-is-proposition x ∣ y ∣)))  ↔⟨ (∃-cong λ _ →
                                                                              (Erased-cong (from-equivalence $
                                                                               Eq.extensionality-isomorphism bad-ext)) F.∘
                                                                              inverse Erased-Π↔Π) F.∘
                                                                             ΠΣ-comm ⟩
    (∃ λ (Q→Q : ∀ x y → Q x → Q ∣ y ∣) →
     Erased (Q→Q ≡
             λ x y → subst Q (T.truncation-is-proposition x ∣ y ∣)))      ↔⟨ T.Σ-Π-∥∥ᴱ-Erased-≡-≃ ⟩

    (∃ λ (Q→Q : ∀ x y → Q ∣ x ∣ → Q ∣ y ∣) →
     Erased (Q→Q ≡
             λ x y → subst Q (T.truncation-is-proposition ∣ x ∣ ∣ y ∣)))  ↔⟨ (inverse $
                                                                              ΠΣ-comm F.∘
                                                                              (∀-cong ext λ _ → ΠΣ-comm)) F.∘
                                                                             (∃-cong λ _ →
                                                                              ((∀-cong ext λ _ → Erased-Π↔Π) F.∘
                                                                               Erased-Π↔Π) F.∘
                                                                              Erased-cong (from-equivalence $ inverse $
                                                                              Eq.extensionality-isomorphism bad-ext F.∘
                                                                              (∀-cong ext λ _ → Eq.extensionality-isomorphism bad-ext))) ⟩
    (∀ x y →
     ∃ λ (Q→Q : Q ∣ x ∣ → Q ∣ y ∣) →
     Erased (Q→Q ≡ subst Q (T.truncation-is-proposition ∣ x ∣ ∣ y ∣)))    ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                              let lemma = inverse $ →-cong ext (P≃Q _) (P≃Q _) in
                                                                              EEq.Σ-cong-≃ᴱ-Erased lemma λ _ →
                                                                              Erased-cong (from-equivalence $ inverse $
                                                                              Eq.≃-≡ $ EEq.≃ᴱ→≃ lemma)) ⟩
    (∀ x y →
     ∃ λ (P→P : P x → P y) →
     Erased (P→P ≡
             _≃ᴱ_.from (P≃Q y) ∘
             subst Q (T.truncation-is-proposition ∣ x ∣ ∣ y ∣) ∘
             _≃ᴱ_.to (P≃Q x)))                                            ↔⟨ (∃-cong λ _ → Erased-cong (from-equivalence $
                                                                              Eq.extensionality-isomorphism bad-ext F.∘
                                                                              (∀-cong ext λ _ → Eq.extensionality-isomorphism bad-ext))) F.∘
                                                                             (∃-cong λ _ →
                                                                              inverse $
                                                                              (∀-cong ext λ _ → Erased-Π↔Π) F.∘
                                                                              Erased-Π↔Π) F.∘
                                                                             ΠΣ-comm F.∘
                                                                             (∀-cong ext λ _ → ΠΣ-comm) ⟩□
    (∃ λ (P→P : ∀ x y → P x → P y) →
     Erased (P→P ≡
             λ x y →
             _≃ᴱ_.from (P≃Q y) ∘
             subst Q (T.truncation-is-proposition ∣ x ∣ ∣ y ∣) ∘
             _≃ᴱ_.to (P≃Q x)))                                            □

------------------------------------------------------------------------
-- The lens type family

-- Higher lenses with erased "proofs".

Lens : Type a → Type b → Type (lsuc (a ⊔ b))
Lens A B = ∃ λ (get : A → B) → Coherently-constant (get ⁻¹ᴱ_)

-- In erased contexts Lens A B is equivalent to V.Lens A B.

@0 Lens≃Variant-lens : Lens A B ≃ V.Lens A B
Lens≃Variant-lens {B = B} =
  (∃ λ get → Coherently-constant (get ⁻¹ᴱ_))   ↝⟨ (∃-cong λ _ → Coherently-constant-⁻¹ᴱ≃Variant-coherently-constant-⁻¹) ⟩□
  (∃ λ get → V.Coherently-constant (get ⁻¹_))  □

-- Some derived definitions.

module Lens {A : Type a} {B : Type b} (l : Lens A B) where

  -- A getter.

  get : A → B
  get = proj₁ l

  -- A predicate.

  H : Pow a ∥ B ∥ᴱ
  H = proj₁ (proj₂ l)

  -- An equivalence (with erased proofs).

  get⁻¹ᴱ-≃ᴱ : ∀ b → get ⁻¹ᴱ b ≃ᴱ H ∣ b ∣
  get⁻¹ᴱ-≃ᴱ = proj₁ (proj₂ (proj₂ l))

  -- The predicate H is, in a certain sense, constant.

  H→H : ∀ b₁ b₂ → H b₁ → H b₂
  H→H = proj₁ (proj₂ (proj₂ (proj₂ l)))

  -- In erased contexts H→H can be expressed using
  -- T.truncation-is-proposition.

  @0 H→H≡ : H→H b₁ b₂ ≡ subst H (T.truncation-is-proposition b₁ b₂)
  H→H≡ = erased (proj₂ (proj₂ (proj₂ (proj₂ l)))) _ _

  -- In erased contexts H→H b₁ b₂ is an equivalence.

  @0 H→H-equivalence : ∀ b₁ b₂ → Is-equivalence (H→H b₁ b₂)
  H→H-equivalence b₁ b₂ =                                         $⟨ _≃_.is-equivalence $ Eq.subst-as-equivalence _ _ ⟩
    Is-equivalence (subst H (T.truncation-is-proposition b₁ b₂))  ↝⟨ subst Is-equivalence $ sym H→H≡ ⟩□
    Is-equivalence (H→H b₁ b₂)                                    □

  -- One can convert from any "preimage" (with erased proofs) of the
  -- getter to any other.

  get⁻¹ᴱ-const : (b₁ b₂ : B) → get ⁻¹ᴱ b₁ → get ⁻¹ᴱ b₂
  get⁻¹ᴱ-const b₁ b₂ =
    get ⁻¹ᴱ b₁  ↝⟨ _≃ᴱ_.to $ get⁻¹ᴱ-≃ᴱ b₁ ⟩
    H ∣ b₁ ∣    ↝⟨ H→H ∣ b₁ ∣ ∣ b₂ ∣ ⟩
    H ∣ b₂ ∣    ↝⟨ _≃ᴱ_.from $ get⁻¹ᴱ-≃ᴱ b₂ ⟩□
    get ⁻¹ᴱ b₂  □

  -- The function get⁻¹ᴱ-const b₁ b₂ is an equivalence (in erased
  -- contexts).

  @0 get⁻¹ᴱ-const-equivalence :
    (b₁ b₂ : B) → Is-equivalence (get⁻¹ᴱ-const b₁ b₂)
  get⁻¹ᴱ-const-equivalence b₁ b₂ = _≃_.is-equivalence (
    get ⁻¹ᴱ b₁  ↝⟨ EEq.≃ᴱ→≃ $ get⁻¹ᴱ-≃ᴱ b₁ ⟩
    H ∣ b₁ ∣    ↝⟨ Eq.⟨ _ , H→H-equivalence ∣ b₁ ∣ ∣ b₂ ∣ ⟩ ⟩
    H ∣ b₂ ∣    ↝⟨ EEq.≃ᴱ→≃ $ inverse $ get⁻¹ᴱ-≃ᴱ b₂ ⟩□
    get ⁻¹ᴱ b₂  □)

  -- Some coherence properties.

  @0 H→H-∘ : H→H b₂ b₃ ∘ H→H b₁ b₂ ≡ H→H b₁ b₃
  H→H-∘ {b₂ = b₂} {b₃ = b₃} {b₁ = b₁} =
    H→H b₂ b₃ ∘ H→H b₁ b₂                               ≡⟨ cong₂ (λ f g → f ∘ g) H→H≡ H→H≡ ⟩

    subst H (T.truncation-is-proposition b₂ b₃) ∘
    subst H (T.truncation-is-proposition b₁ b₂)         ≡⟨ (⟨ext⟩ λ _ → subst-subst _ _ _ _) ⟩

    subst H (trans (T.truncation-is-proposition b₁ b₂)
               (T.truncation-is-proposition b₂ b₃))     ≡⟨ cong (subst H) $
                                                           mono₁ 1 T.truncation-is-proposition _ _ ⟩

    subst H (T.truncation-is-proposition b₁ b₃)         ≡⟨ sym H→H≡ ⟩∎

    H→H b₁ b₃                                           ∎

  @0 H→H-id : ∀ {b} → H→H b b ≡ id
  H→H-id {b = b} =
    H→H b b                                    ≡⟨ H→H≡ ⟩
    subst H (T.truncation-is-proposition b b)  ≡⟨ cong (subst H) $
                                                  mono₁ 1 T.truncation-is-proposition _ _ ⟩
    subst H (refl b)                           ≡⟨ (⟨ext⟩ λ _ → subst-refl _ _) ⟩∎
    id                                         ∎

  @0 H→H-inverse : H→H b₁ b₂ ∘ H→H b₂ b₁ ≡ id
  H→H-inverse {b₁ = b₁} {b₂ = b₂} =
    H→H b₁ b₂ ∘ H→H b₂ b₁  ≡⟨ H→H-∘ ⟩
    H→H b₂ b₂              ≡⟨ H→H-id ⟩∎
    id                     ∎

  @0 get⁻¹ᴱ-const-∘ :
    get⁻¹ᴱ-const b₂ b₃ ∘ get⁻¹ᴱ-const b₁ b₂ ≡ get⁻¹ᴱ-const b₁ b₃
  get⁻¹ᴱ-const-∘ {b₂ = b₂} {b₃ = b₃} {b₁ = b₁} = ⟨ext⟩ λ p →
    _≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ b₃)
      (H→H _ _
         (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b₂)
            (_≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ b₂)
               (H→H _ _ (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b₁) p)))))             ≡⟨ cong (_≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ _) ∘ H→H _ _) $
                                                                      _≃ᴱ_.right-inverse-of (get⁻¹ᴱ-≃ᴱ _) _ ⟩
    _≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ b₃)
      (H→H _ _ (H→H _ _ (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b₁) p)))               ≡⟨ cong (λ f → _≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ _) (f (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ _) _)))
                                                                      H→H-∘ ⟩∎
    _≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ b₃) (H→H _ _ (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b₁) p))  ∎

  @0 get⁻¹ᴱ-const-id : ∀ {b} → get⁻¹ᴱ-const b b ≡ id
  get⁻¹ᴱ-const-id {b = b} = ⟨ext⟩ λ p →
    _≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ b) (H→H _ _ (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b) p))  ≡⟨ cong (_≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ b)) $ cong (_$ _) H→H-id  ⟩
    _≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ b) (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b) p)            ≡⟨ _≃ᴱ_.left-inverse-of (get⁻¹ᴱ-≃ᴱ b) _ ⟩∎
    p                                                            ∎

  @0 get⁻¹ᴱ-const-inverse :
    get⁻¹ᴱ-const b₁ b₂ ∘ get⁻¹ᴱ-const b₂ b₁ ≡ id
  get⁻¹ᴱ-const-inverse {b₁ = b₁} {b₂ = b₂} =
    get⁻¹ᴱ-const b₁ b₂ ∘ get⁻¹ᴱ-const b₂ b₁  ≡⟨ get⁻¹ᴱ-const-∘ ⟩
    get⁻¹ᴱ-const b₂ b₂                       ≡⟨ get⁻¹ᴱ-const-id ⟩∎
    id                                       ∎

  -- A setter.

  set : A → B → A
  set a b =                      $⟨ get⁻¹ᴱ-const _ _ ⟩
    (get ⁻¹ᴱ get a → get ⁻¹ᴱ b)  ↝⟨ _$ (a , [ refl _ ]) ⟩
    get ⁻¹ᴱ b                    ↝⟨ proj₁ ⟩□
    A                            □

  -- Lens laws.

  @0 get-set : ∀ a b → get (set a b) ≡ b
  get-set a b =
    get (proj₁ (get⁻¹ᴱ-const (get a) b (a , [ refl _ ])))  ≡⟨ erased (proj₂ (get⁻¹ᴱ-const (get a) b (a , [ refl _ ]))) ⟩∎
    b                                                      ∎

  @0 set-get : ∀ a → set a (get a) ≡ a
  set-get a =
    proj₁ (get⁻¹ᴱ-const (get a) (get a) (a , [ refl _ ]))  ≡⟨ cong proj₁ $ cong (_$ a , [ refl _ ]) get⁻¹ᴱ-const-id ⟩∎
    a                                                      ∎

  @0 set-set : ∀ a b₁ b₂ → set (set a b₁) b₂ ≡ set a b₂
  set-set a b₁ b₂ =
    proj₁ (get⁻¹ᴱ-const (get (set a b₁)) b₂ (set a b₁ , [ refl _ ]))  ≡⟨ elim¹
                                                                           (λ {b} eq →
                                                                              proj₁ (get⁻¹ᴱ-const (get (set a b₁)) b₂ (set a b₁ , [ refl _ ])) ≡
                                                                              proj₁ (get⁻¹ᴱ-const b b₂ (set a b₁ , [ eq ])))
                                                                           (refl _)
                                                                           (get-set a b₁) ⟩
    proj₁ (get⁻¹ᴱ-const b₁ b₂ (set a b₁ , [ get-set a b₁ ]))          ≡⟨⟩

    proj₁ (get⁻¹ᴱ-const b₁ b₂
             (get⁻¹ᴱ-const (get a) b₁ (a , [ refl _ ])))              ≡⟨ cong proj₁ $ cong (_$ a , [ refl _ ]) get⁻¹ᴱ-const-∘ ⟩∎

    proj₁ (get⁻¹ᴱ-const (get a) b₂ (a , [ refl _ ]))                  ∎

  -- TODO: Can get-set-get and get-set-set be proved for the lens laws
  -- given above?

instance

  -- The lenses defined above have getters and setters.

  has-getter-and-setter :
    Has-getter-and-setter (Lens {a = a} {b = b})
  has-getter-and-setter = record
    { get = Lens.get
    ; set = Lens.set
    }

------------------------------------------------------------------------
-- Equality characterisation lemmas

-- An equality characterisation lemma.

@0 equality-characterisation₁ :
  {A : Type a} {B : Type b} {l₁ l₂ : Lens A B} →
  Block "equality-characterisation" →
  let open Lens in

  (l₁ ≡ l₂)
    ≃
  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     ∀ b p →
     subst (_$ ∣ b ∣) h
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym g) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)
equality-characterisation₁
  {a = a} {b = b} {A = A} {B = B} {l₁ = l₁} {l₂ = l₂} ⊠ =

  l₁ ≡ l₂                                                              ↝⟨ inverse $ Eq.≃-≡ $ Eq.↔⇒≃ (Σ-assoc F.∘ ∃-cong λ _ → Σ-assoc) ⟩

  ((get l₁ , H l₁ , get⁻¹ᴱ-≃ᴱ l₁) , _) ≡
  ((get l₂ , H l₂ , get⁻¹ᴱ-≃ᴱ l₂) , _)                                 ↔⟨ inverse $ ignore-propositional-component $ mono₁ 0
                                                                          Contractible-last-part-of-Coherently-constant ⟩

  (get l₁ , H l₁ , get⁻¹ᴱ-≃ᴱ l₁) ≡ (get l₂ , H l₂ , get⁻¹ᴱ-≃ᴱ l₂)      ↝⟨ inverse $ Eq.≃-≡ $ Eq.↔⇒≃ Σ-assoc ⟩

  ((get l₁ , H l₁) , get⁻¹ᴱ-≃ᴱ l₁) ≡ ((get l₂ , H l₂) , get⁻¹ᴱ-≃ᴱ l₂)  ↔⟨ inverse B.Σ-≡,≡↔≡ ⟩

  (∃ λ (eq : (get l₁ , H l₁) ≡ (get l₂ , H l₂)) →
     subst (λ (g , H) → ∀ b → g ⁻¹ᴱ b ≃ᴱ H ∣ b ∣) eq (get⁻¹ᴱ-≃ᴱ l₁) ≡
     get⁻¹ᴱ-≃ᴱ l₂)                                                     ↝⟨ (Σ-cong-contra ≡×≡↔≡ λ _ → F.id) ⟩

  (∃ λ ((g , h) : get l₁ ≡ get l₂ × H l₁ ≡ H l₂) →
     subst (λ (g , H) → ∀ b → g ⁻¹ᴱ b ≃ᴱ H ∣ b ∣)
       (cong₂ _,_ g h) (get⁻¹ᴱ-≃ᴱ l₁) ≡
     get⁻¹ᴱ-≃ᴱ l₂)                                                     ↔⟨ inverse Σ-assoc ⟩

  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     subst (λ (g , H) → ∀ b → g ⁻¹ᴱ b ≃ᴱ H ∣ b ∣)
       (cong₂ _,_ g h) (get⁻¹ᴱ-≃ᴱ l₁) ≡
     get⁻¹ᴱ-≃ᴱ l₂)                                                     ↝⟨ (∃-cong λ _ → ∃-cong λ _ → inverse $
                                                                           Eq.extensionality-isomorphism ext) ⟩
  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     ∀ b → subst (λ (g , H) → ∀ b → g ⁻¹ᴱ b ≃ᴱ H ∣ b ∣)
             (cong₂ _,_ g h) (get⁻¹ᴱ-≃ᴱ l₁) b ≡
           get⁻¹ᴱ-≃ᴱ l₂ b)                                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ → ≡⇒↝ _ $ cong (_≡ _) $ sym $
                                                                           push-subst-application _ _) ⟩
  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     ∀ b → subst (λ (g , H) → g ⁻¹ᴱ b ≃ᴱ H ∣ b ∣)
             (cong₂ _,_ g h) (get⁻¹ᴱ-≃ᴱ l₁ b) ≡
           get⁻¹ᴱ-≃ᴱ l₂ b)                                             ↔⟨ (∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ → inverse $
                                                                           EEq.to≡to≃≡ ext) ⟩
  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     ∀ b p →
     _≃ᴱ_.to (subst (λ (g , H) → g ⁻¹ᴱ b ≃ᴱ H ∣ b ∣)
               (cong₂ _,_ g h) (get⁻¹ᴱ-≃ᴱ l₁ b)) p ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                       ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                           ≡⇒↝ _ $ cong (_≡ _) $ lemma _ _ _ _) ⟩□
  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     ∀ b p →
     subst (_$ ∣ b ∣) h
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym g) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                       □

  where

  open Lens

  lemma : ∀ _ _ _ _ → _ ≡ _
  lemma g h b p =
    _≃ᴱ_.to (subst (λ (g , H) → g ⁻¹ᴱ b ≃ᴱ H ∣ b ∣)
              (cong₂ _,_ g h) (get⁻¹ᴱ-≃ᴱ l₁ b)) p                ≡⟨ cong (_$ p) EEq.to-subst ⟩

    subst (λ (g , H) → g ⁻¹ᴱ b → H ∣ b ∣)
      (cong₂ _,_ g h) (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b)) p               ≡⟨ subst-→ ⟩

    subst (λ (g , H) → H ∣ b ∣) (cong₂ _,_ g h)
      (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b)
         (subst (λ (g , H) → g ⁻¹ᴱ b) (sym $ cong₂ _,_ g h) p))  ≡⟨ subst-∘ _ _ _ ⟩

    subst (_$ ∣ b ∣) (cong proj₂ $ cong₂ _,_ g h)
      (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b)
         (subst (λ (g , H) → g ⁻¹ᴱ b) (sym $ cong₂ _,_ g h) p))  ≡⟨ cong₂ (λ p q → subst (λ (H : Pow a ∥ _ ∥ᴱ) → H ∣ b ∣)
                                                                                p (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) q))
                                                                      (cong-proj₂-cong₂-, _ _)
                                                                      (subst-∘ _ _ _) ⟩
    subst (_$ ∣ b ∣) h
      (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b)
         (subst (_⁻¹ᴱ b) (cong proj₁ $ sym $ cong₂ _,_ g h) p))  ≡⟨ cong (λ eq → subst (_$ ∣ b ∣) h
                                                                                (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) eq p))) $
                                                                    trans (cong-sym _ _) $
                                                                    cong sym $ cong-proj₁-cong₂-, _ _ ⟩∎
    subst (_$ ∣ b ∣) h
      (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym g) p))      ∎

-- Another equality characterisation lemma.

@0 equality-characterisation₂ :
  {l₁ l₂ : Lens A B} →
  Block "equality-characterisation" →
  let open Lens in

  (l₁ ≡ l₂)
    ≃
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     ∀ b p →
     subst id (h ∣ b ∣)
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)
equality-characterisation₂ {l₁ = l₁} {l₂ = l₂} ⊠ =
  l₁ ≡ l₂                                                               ↝⟨ equality-characterisation₁ ⊠ ⟩

  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     ∀ b p →
     subst (_$ ∣ b ∣) h
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym g) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                        ↝⟨ (Σ-cong-contra (Eq.extensionality-isomorphism bad-ext) λ _ →
                                                                            Σ-cong-contra (Eq.extensionality-isomorphism bad-ext) λ _ →
                                                                            F.id) ⟩
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     ∀ b p →
     subst (_$ ∣ b ∣) (⟨ext⟩ h)
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                        ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                            ≡⇒↝ _ $ cong (_≡ _) $
                                                                            subst-ext _ _) ⟩□
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     ∀ b p →
     subst id (h ∣ b ∣)
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                        □
  where
  open Lens

-- Yet another equality characterisation lemma.

@0 equality-characterisation₃ :
  {A : Type a} {B : Type b}
  {l₁ l₂ : Lens A B} →
  Block "equality-characterisation" →
  Univalence (a ⊔ b) →
  let open Lens in

  (l₁ ≡ l₂)
    ≃
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≃ H l₂ b) →
     ∀ b p →
     _≃_.to (h ∣ b ∣)
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)
equality-characterisation₃ {l₁ = l₁} {l₂ = l₂} ⊠ univ =
  l₁ ≡ l₂                                                               ↝⟨ equality-characterisation₂ ⊠ ⟩

  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     ∀ b p →
     subst id (h ∣ b ∣)
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                        ↝⟨ (∃-cong λ _ →
                                                                            Σ-cong-contra (∀-cong ext λ _ → inverse $ ≡≃≃ univ) λ _ → F.id) ⟩
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≃ H l₂ b) →
     ∀ b p →
     subst id (≃⇒≡ univ (h ∣ b ∣))
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                        ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                            ≡⇒↝ _ $ cong (_≡ _) $
                                                                            trans (subst-id-in-terms-of-≡⇒↝ equivalence) $
                                                                            cong (λ eq → _≃_.to eq _) $
                                                                            _≃_.right-inverse-of (≡≃≃ univ) _) ⟩□
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≃ H l₂ b) →
     ∀ b p →
     _≃_.to (h ∣ b ∣)
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                        □
  where
  open Lens

------------------------------------------------------------------------
-- Conversion functions

-- The lenses defined above can be converted to and from the lenses
-- defined in Higher.

Lens⇔Higher-lens :
  Block "conversion" →
  Lens A B ⇔ Higher.Lens A B
Lens⇔Higher-lens {A = A} {B = B} ⊠ = record
  { to = λ l → let open Lens l in record
      { R = Σ ∥ B ∥ᴱ H

      ; equiv =
          A                                                      ↝⟨ (inverse $ drop-⊤-right λ _ → Erased-other-singleton≃ᴱ⊤) ⟩
          (∃ λ (a : A) → ∃ λ (b : B) → Erased (get a ≡ b))       ↔⟨ ∃-comm ⟩
          (∃ λ (b : B) → get ⁻¹ᴱ b)                              ↝⟨ ∃-cong get⁻¹ᴱ-≃ᴱ ⟩
          (∃ λ (b : B) → H ∣ b ∣)                                ↝⟨ EEq.↔→≃ᴱ
                                                                      (λ (b , h) → (∣ b ∣ , b) , h)
                                                                      (λ ((∥b∥ , b) , h) → b , H→H ∥b∥ ∣ b ∣ h)
                                                                      (λ ((∥b∥ , b) , h) →
                                                                         Σ-≡,≡→≡ (cong (_, _) (T.truncation-is-proposition _ _)) (
              subst (H ∘ proj₁)
                (cong (_, _) (T.truncation-is-proposition _ _))
                (H→H _ _ h)                                                ≡⟨ trans (subst-∘ _ _ _) $
                                                                              trans (cong (flip (subst H) _) $ cong-∘ _ _ _) $
                                                                              cong (flip (subst H) _) $ sym $ cong-id _ ⟩
              subst H (T.truncation-is-proposition _ _)
                (H→H _ _ h)                                                ≡⟨ cong (_$ _) $ sym H→H≡ ⟩

              H→H _ _ (H→H _ _ h)                                          ≡⟨ cong (_$ h) H→H-∘ ⟩

              H→H _ _ h                                                    ≡⟨ cong (_$ h) H→H-id ⟩∎

              h                                                            ∎))
                                                                      (λ (b , h) → cong (_ ,_) (
              H→H _ _ h                                                  ≡⟨ cong (_$ h) H→H-id ⟩∎
              h                                                          ∎)) ⟩

          (∃ λ ((b , _) : ∥ B ∥ᴱ × B) → H b)                     ↔⟨ Σ-assoc F.∘
                                                                    (∃-cong λ _ → ×-comm) F.∘
                                                                    inverse Σ-assoc ⟩□
          Σ ∥ B ∥ᴱ H × B                                         □

      ; inhabited = _≃_.to PT.∥∥ᴱ≃∥∥ ∘ proj₁
      }
  ; from = λ l →
        Higher.Lens.get l
      , (λ _ → Higher.Lens.R l)
      , (λ b → inverse (Higher.remainder≃ᴱget⁻¹ᴱ l b))
      , (λ _ _ → id)
      , [ (λ _ _ → ⟨ext⟩ λ r →
             r                                    ≡⟨ sym $ subst-const _ ⟩∎
             subst (const (Higher.Lens.R l)) _ r  ∎)
        ]
  }

-- The conversion preserves getters and setters.

Lens⇔Higher-lens-preserves-getters-and-setters :
  (bl : Block "conversion") →
  Preserves-getters-and-setters-⇔ A B (Lens⇔Higher-lens bl)
Lens⇔Higher-lens-preserves-getters-and-setters ⊠ =
    (λ _ → refl _ , refl _)
  , (λ _ → refl _ , refl _)

-- Lens A B is equivalent to Higher.Lens A B (with erased proofs,
-- assuming univalence).

Lens≃ᴱHigher-lens :
  {A : Type a} {B : Type b} →
  Block "conversion" →
  @0 Univalence (a ⊔ b) →
  Lens A B ≃ᴱ Higher.Lens A B
Lens≃ᴱHigher-lens {A = A} {B = B} bl univ =
  EEq.↔→≃ᴱ
    (_⇔_.to (Lens⇔Higher-lens bl))
    (_⇔_.from (Lens⇔Higher-lens bl))
    (to∘from bl)
    (from∘to bl)
  where
  @0 to∘from :
    (bl : Block "conversion") →
    ∀ l →
    _⇔_.to (Lens⇔Higher-lens bl) (_⇔_.from (Lens⇔Higher-lens bl) l) ≡ l
  to∘from ⊠ l = _↔_.from (Higher.equality-characterisation₁ univ)
    ( (∥ B ∥ᴱ × R  ↔⟨ (drop-⊤-left-× λ r → _⇔_.to contractible⇔↔⊤ $
                       propositional⇒inhabited⇒contractible
                         T.truncation-is-proposition
                         (_≃_.from PT.∥∥ᴱ≃∥∥ (inhabited r))) ⟩□
       R          □)
    , (λ _ → refl _)
    )
    where
    open Higher.Lens l

  @0 from∘to :
    (bl : Block "conversion") →
    ∀ l →
    _⇔_.from (Lens⇔Higher-lens bl) (_⇔_.to (Lens⇔Higher-lens bl) l) ≡ l
  from∘to bl@⊠ l = _≃_.from (equality-characterisation₃ ⊠ univ)
    ( (λ _ → refl _)
    , Σ∥B∥ᴱH≃H
    , (λ b p@(a , [ get-a≡b ]) →
         _≃_.to (Σ∥B∥ᴱH≃H ∣ b ∣)
           (_≃ᴱ_.from (Higher.remainder≃ᴱget⁻¹ᴱ
                         (_⇔_.to (Lens⇔Higher-lens bl) l) b)
              (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ λ _ → refl _)) p))       ≡⟨ cong (_≃_.to (Σ∥B∥ᴱH≃H ∣ b ∣) ∘
                                                                            _≃ᴱ_.from (Higher.remainder≃ᴱget⁻¹ᴱ
                                                                                (_⇔_.to (Lens⇔Higher-lens bl) l) b)) $
                                                                      trans (cong (flip (subst (_⁻¹ᴱ b)) p) $
                                                                             trans (cong sym ext-refl) $
                                                                             sym-refl) $
                                                                      subst-refl _ _ ⟩
         _≃_.to (Σ∥B∥ᴱH≃H ∣ b ∣)
           (_≃ᴱ_.from (Higher.remainder≃ᴱget⁻¹ᴱ
                         (_⇔_.to (Lens⇔Higher-lens bl) l) b)
              p)                                                   ≡⟨⟩

         _≃_.to (Σ∥B∥ᴱH≃H ∣ b ∣)
           (Higher.Lens.remainder
              (_⇔_.to (Lens⇔Higher-lens bl) l) a)                  ≡⟨⟩

         subst H _ (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a)) (a , [ refl _ ]))  ≡⟨ cong (λ eq → subst H eq (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a)) (a , [ refl _ ]))) $
                                                                      mono₁ 1 T.truncation-is-proposition _ _ ⟩
         subst H (cong ∣_∣ get-a≡b)
           (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a)) (a , [ refl _ ]))          ≡⟨ elim¹
                                                                        (λ {b} eq →
                                                                           subst H (cong ∣_∣ eq)
                                                                             (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a)) (a , [ refl _ ])) ≡
                                                                           _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b) (a , [ eq ]))
                                                                        (
           subst H (cong ∣_∣ (refl _))
             (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a)) (a , [ refl _ ]))              ≡⟨ trans (cong (flip (subst H) _) $ cong-refl _) $
                                                                            subst-refl _ _ ⟩
           _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a)) (a , [ refl _ ])                  ∎)
                                                                        _ ⟩∎
         _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b) p                                   ∎)
    )
    where
    open Lens l

    Σ∥B∥ᴱH≃H = λ b →
      Σ ∥ B ∥ᴱ H  ↔⟨ (drop-⊤-left-Σ $ _⇔_.to contractible⇔↔⊤ $
                      propositional⇒inhabited⇒contractible
                        T.truncation-is-proposition b) ⟩□
      H b         □

-- The equivalence preserves getters and setters.

Lens≃ᴱHigher-lens-preserves-getters-and-setters :
  {A : Type a} {B : Type b}
  (bl : Block "conversion")
  (@0 univ : Univalence (a ⊔ b)) →
  Preserves-getters-and-setters-⇔ A B
    (_≃ᴱ_.logical-equivalence (Lens≃ᴱHigher-lens bl univ))
Lens≃ᴱHigher-lens-preserves-getters-and-setters bl univ =
  Lens⇔Higher-lens-preserves-getters-and-setters bl

max_stars_repo_name: nad/dependent-lenses

max_issues_repo_name: nad/dependent-lenses

max_forks_repo_name: nad/dependent-lenses


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Greatest Common Divisor for integers
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Integer.GCD where

open import Data.Integer.Base
open import Data.Integer.Divisibility
open import Data.Integer.Properties
open import Data.Nat.Base
import Data.Nat.GCD as ℕ
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Definition
------------------------------------------------------------------------

gcd : ℤ → ℤ → ℤ
gcd i j = + ℕ.gcd ∣ i ∣ ∣ j ∣

------------------------------------------------------------------------
-- Properties
------------------------------------------------------------------------

gcd[i,j]∣i : ∀ i j → gcd i j ∣ i
gcd[i,j]∣i i j = ℕ.gcd[m,n]∣m ∣ i ∣ ∣ j ∣

gcd[i,j]∣j : ∀ i j → gcd i j ∣ j
gcd[i,j]∣j i j = ℕ.gcd[m,n]∣n ∣ i ∣ ∣ j ∣

gcd-greatest : ∀ {i j c} → c ∣ i → c ∣ j → c ∣ gcd i j
gcd-greatest c∣i c∣j = ℕ.gcd-greatest c∣i c∣j

gcd[0,0]≡0 : gcd 0ℤ 0ℤ ≡ 0ℤ
gcd[0,0]≡0 = cong (+_) ℕ.gcd[0,0]≡0

gcd[i,j]≡0⇒i≡0 : ∀ i j → gcd i j ≡ 0ℤ → i ≡ 0ℤ
gcd[i,j]≡0⇒i≡0 i j eq = ∣n∣≡0⇒n≡0 (ℕ.gcd[m,n]≡0⇒m≡0 (+-injective eq))

gcd[i,j]≡0⇒j≡0 : ∀ {i j} → gcd i j ≡ 0ℤ → j ≡ 0ℤ
gcd[i,j]≡0⇒j≡0 {i} eq = ∣n∣≡0⇒n≡0 (ℕ.gcd[m,n]≡0⇒n≡0 ∣ i ∣ (+-injective eq))

gcd-comm : ∀ i j → gcd i j ≡ gcd j i
gcd-comm i j = cong (+_) (ℕ.gcd-comm ∣ i ∣ ∣ j ∣)


text:
{-

Part 1: The interval and path types

• The interval in Cubical Agda
• Path and PathP types
• Function extensionality
• Equality in Σ-types

-}

-- To make Agda cubical add the following options
{-# OPTIONS --cubical #-}
module Part1 where

-- To load an Agda file type "C-c C-l" in emacs (the notation "C-c"
-- means that one should hold "CTRL" and press "c", for general
-- documentation about emacs keybindings see:
-- https://www.gnu.org/software/emacs/manual/html_node/efaq/Basic-keys.html)

-- The "Core" package of the agda/cubical library sets things for us
open import Cubical.Core.Primitives public

-- The "Foundations" package of agda/cubical contains a lot of
-- important results (in particular the univalence theorem). As we
-- will develop many things from scratch we don't import it here, but
-- a typical file in the library would import the relevant files from
-- Foundations which it uses. To get everything in Foundations write:
--
-- open import Cubical.Foundations.Everything

-- To search for something among the imported files press C-s C-z and
-- then write what you want to search for.

-- Documentation of the Cubical Agda mode can be found at:
-- https://agda.readthedocs.io/en/v2.6.1.3/language/cubical.html

------------------------------------------------------------------------------
--                             Agda Basic                                   --
------------------------------------------------------------------------------

-- We parametrize everything by some universe levels (as opposed to
-- Coq we always have to give these explicitly unless we work with the
-- lowest universe)
variable
  ℓ ℓ' ℓ'' : Level

-- Universes in Agda are called "Set", but in order to avoid confusion
-- with h-sets we rename them to "Type".

-- Functions in Agda are written using equations:
id : {A : Type ℓ} → A → A
id x = x
-- The {A : Type} notation says that A is an implicit argument of Type ℓ.

-- The notation (x : A) → B and {x : A} → B introduces a dependent
-- function (so B might mention B), in other words an element of a
-- Π-type.

-- We could also write this using a λ-abstraction:
id' : {A : Type ℓ} → A → A
id' = λ x → x
-- To input a nice symbol for the lambda write "\lambda". Agda support
-- Unicode symbols natively:
-- https://agda.readthedocs.io/en/latest/tools/emacs-mode.html#unicode-input
-- To input the "ℓ" write "\ell"

-- We can build Agda terms interactively in emacs by writing a ? as RHS:
--
-- id'' : {A : Type ℓ} → A → A
-- id'' = ?
--
-- Try uncommenting this and pressing "C-c C-l". This will give us a
-- hole and by entering it with the cursor we can get information
-- about what Agda expects us to provide and get help from Agda in
-- providing this.
--
-- By pressing "C-c C-," while having the cursor in the goal Agda
-- shows us the current context and goal. As we're trying to write a
-- function we can press "C-c C-r" (for refine) to have Agda write the
-- λ-abstraction "λ x → ?" automatically for us. If one presses "C-c C-,"
-- in the hole again "x : A" will now be in the context. If we type
-- "x" in the hole and press "C-c C-." Agda will show us that we have
-- an A, which is exactly what we want to provide to fill the goal. By
-- pressing "C-c C-SPACE" Agda will then fill the hole with "x" for us.
--
-- Agda has lots of handy commands like this for manipulating goals:
-- https://agda.readthedocs.io/en/latest/tools/emacs-mode.html#commands-in-context-of-a-goal

-- A good resource to get start with Agda is the documentation:
-- https://agda.readthedocs.io/en/latest/getting-started/index.html

------------------------------------------------------------------------------
--                     The interval and path types                          --
------------------------------------------------------------------------------

-- The interval in Cubical Agda is written I and the endpoints are
--
--   i0 : I
--   i1 : I
--
-- These stand for "interval 0" and "interval 1".

-- We can apply a function out of the interval to an endpoint just
-- like we would apply any Agda function:
apply0 : (A : Type ℓ) (p : I → A) → A
apply0 A p = p i0

-- The equality type _≡_ is not inductively defined in Cubical Agda,
-- instead it's a builtin primitive. An element of x ≡ y consists of a
-- function p : I → A such that p i0 is definitionally x and p i1 is
-- definitionally y. The check that the endpoints are correct when we
-- provide a p : I → A is automatically checked by Agda during
-- typechecking, so introducing an element of x ≡ y is done just like
-- how we introduce elements of I → A but Agda will check the side
-- conditions.
--
-- So we can write paths using λ-abstraction:
path1 : {A : Type ℓ} (x : A) → x ≡ x
path1 x = λ i → x
--
-- As explained above Agda checks that whatever we write as definition
-- matches the path that we have written (so the endpoints have to be
-- correct). In this case everything is fine and path1 can be thought
-- of as a proof reflexivity. Let's give it a nicer name and more
-- implicit arguments:
--
refl : {A : Type ℓ} {x : A} → x ≡ x
refl {x = x} = λ i → x
--
-- The notation {x = x} lets us access the implicit argument x (the x
-- in the LHS) and rename it to x (the x in the RHS) in the body of refl.
-- We could just as well have written:
--
-- refl : {A : Type ℓ} {x : A} → x ≡ x
-- refl {x = y} = λ i → y

-- Note that we cannot pattern-match on interval variables as I is not
-- inductively defined:
--
-- foo : {A : Type} → I → A
-- foo r = {!r!}   -- Try typing C-c C-c

-- It often gets tiring to write {A : Type ℓ} everywhere, so let's
-- assume that we have some types:
variable
  A B : Type ℓ
-- This will make A and B elements of different universes (all
-- arguments is maximally generalized) and all definitions that use
-- them will have them as implicit arguments.

-- We can now implement some basic operations on _≡_. Let's start with
-- cong (called "ap" in the HoTT book):
cong : (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f p i = f (p i)

-- Note that the definition differs from the HoTT definition in that
-- it is not defined by J or pattern-matching on p, but rather it's
-- just a direct definition as a composition fo functions. Agda treats
-- p : x ≡ y as a function, so we can just apply it to i to get an
-- element of A which at i0 is x and at i1 is y. By applying f to this
-- element we hence get an element of B which at i0 is f x and at i1
-- is f y.

-- As this is just function composition it satisfies lots of nice
-- definitional equalities, see the Warmup.agda file. Some of these
-- are not satisfied by the HoTT definition of cong/ap.

-- In HoTT function extensionality is proved as a consequence of
-- univalence using a rather ingenious proof due to Voevodsky, but in
-- cubical systems it has a much more direct proof. As paths are just
-- functions we can get it by just swapping the arguments to p:
funExt : {f g : A → B} (p : (x : A) → f x ≡ g x) → f ≡ g
funExt p i x = p x i

-- To see that this has the correct type not that when i is i0 we have
-- "p x i0 = f x" and when i is i1 we have "p x i1 = g x", so by η for
-- functions we have a path f ≡ g as desired.

-- The interval has additional operations:
--
-- Minimum: _∧_ : I → I → I
-- Maximum: _∨_ : I → I → I
-- Symmetry: ~_ : I → I

-- These satisfy the equations of a De Morgan algebra (i.e. a
-- distributive lattice (_∧_ , _∨_ , i0 , i1) with an involution
-- ~). So we have the following kinds of equations definitionally:
--
-- i0 ∨ i    = i
-- i  ∨ i1   = i1
-- i  ∨ j    = j ∨ i
-- i0 ∧ i    = i0
-- i1 ∧ i    = i
-- i  ∧ j    = j ∧ i
-- ~ (~ i)   = i
-- i0        = ~ i1
-- ~ (i ∨ j) = ~ i ∧ ~ j
-- ~ (i ∧ j) = ~ i ∨ ~ j

-- These operations are very useful as they let us define even more
-- things directly. For example symmetry of paths is easily defined
-- using ~:
sym : {x y : A} → x ≡ y → y ≡ x
sym p i = p (~ i)

-- The operations _∧_ and _∨_ are called "connections" and lets us
-- build higher dimensional cubes from lower dimensional ones, for
-- example if we have a path p : x ≡ y then
--
--   sq i j = p (i ∧ j)
--
-- is a square (as we've parametrized by i and j) with the following
-- boundary:
--
--    sq i0 j = p (i0 ∧ j) = p i0 = x
--    sq i1 j = p (i1 ∧ j) = p j
--    sq i i0 = p (i ∧ i0) = p i0 = x
--    sq i i1 = p (i ∧ i1) = p i
--
-- So if we draw this we get:
--
--              p
--        x --------> y
--        ^           ^
--        ¦           ¦
--   refl ¦     sq    ¦ p
--        ¦           ¦
--        ¦           ¦
--        x --------> x
--            refl
--
-- These operations are very useful, for example let's prove that
-- singletons are contractible (aka based path induction).
--
-- We first need the notion of contractible types. For this we need
-- to use a Σ-type:
isContr : Type ℓ → Type ℓ
isContr A = Σ[ x ∈ A ] ((y : A) → x ≡ y)

-- Σ-types are introduced in the file Agda.Builtin.Sigma as the record
-- (modulo some renaming):
--
-- record Σ {ℓ ℓ'} (A : Type ℓ) (B : A → Type ℓ') : Type (ℓ-max ℓ ℓ') where
--   constructor _,_
--   field
--     fst : A
--     snd : B fst
--
-- So the projections are fst/snd and the constructor is _,_. We
-- also define non-dependent product as a special case of Σ-types in
-- Cubical.Data.Sigma.Base as:
--
-- _×_ : ∀ {ℓ ℓ'} (A : Type ℓ) (B : Type ℓ') → Type (ℓ-max ℓ ℓ')
-- A × B = Σ A (λ _ → B)
--
-- The notation ∀ {ℓ ℓ'} lets us omit the type of ℓ and ℓ' in the
-- definition.

-- We define the type of singletons as follows
singl : {A : Type ℓ} (a : A) → Type ℓ
singl {A = A} a = Σ[ x ∈ A ] a ≡ x

-- To show that this type is contractible we need to provide a center
-- of contraction and the fact that any element of it is path-equal to
-- the center
isContrSingl : (x : A) → isContr (singl x)
isContrSingl x = ctr , prf
  where
  -- The center is just a pair with x and refl
  ctr : singl x
  ctr = x , refl

  -- We then need to prove that ctr is equal to any element s : singl x.
  -- This is an equality in a Σ-type, so the first component is a path
  -- and the second is a path over the path we pick as first argument,
  -- so the second component is a square. In fact, we need a square
  -- relating refl and pax, so we can use an _∧_ connection.
  prf : (s : singl x) → ctr ≡ s
  prf (y , pax) i = (pax i) , λ j → pax (i ∧ j)

-- As we saw in the second component of prf we often need squares when
-- proving things. In fact, pax (i ∧ j) is a path relating refl to pax
-- *over* another path "λ j → x ≡ pax j". This notion of path over a
-- path is very useful when working in HoTT as well as cubically. In
-- HoTT these are called path-overs and are defined using transport,
-- but in Cubical Agda they are a primitive notion called PathP ("Path
-- of a Path"). In general PathP A x y has
--
--    A : I → Type ℓ
--    x : A i0
--    y : A i1
--
-- So PathP lets us natively define heteorgeneous paths, i.e. paths
-- where the endpoints lie in different types. This lets us specify
-- the type of the second component of prf:
prf' : (x : A) (s : singl x) → (x , refl) ≡ s
prf' x (y , pax) i = (pax i) , λ j → goal i j
  where
  goal : PathP (λ j → x ≡ pax j) refl pax
  goal i j = pax (i ∧ j)

-- Just like _×_ is a special case of Σ-types we have that _≡_ is a
-- special case of PathP. In fact, x ≡ y is just short for PathP (λ _ → A) x y:
reflP : {x : A} → PathP (λ _ → A) x x
reflP {x = x} = λ _ → x

-- Having the primitive notion of equality be heterogeneous is an
-- easily overlooked, but very important, strength of cubical type
-- theory. This allows us to work directly with equality in Σ-types
-- without using transport:
module _ {A : Type ℓ} {B : A → Type ℓ'} {x y : Σ A B} where

  ΣPathP : Σ[ p ∈ fst x ≡ fst y ] PathP (λ i → B (p i)) (snd x) (snd y)
         → x ≡ y
  ΣPathP eq i = fst eq i , snd eq i

  PathPΣ : x ≡ y
         → Σ[ p ∈ fst x ≡ fst y ] PathP (λ i → B (p i)) (snd x) (snd y)
  PathPΣ eq = (λ i → fst (eq i)) , (λ i → snd (eq i))

  -- The fact that these cancel is proved by refl

-- If one looks carefully the proof of prf uses ΣPathP inlined, in
-- fact this is used all over the place when working cubically and
-- simplifies many proofs which in HoTT requires long complicated
-- reasoning about transport.
isContrΠ : {B : A → Type ℓ'} (h : (x : A) → isContr (B x))
         → isContr ((x : A) → B x)
isContrΠ h = (λ x → fst (h x)) , (λ f i x → snd (h x) (f x) i)

-- Let us end this session with defining propositions and sets
isProp : Type ℓ → Type ℓ
isProp A = (x y : A) → x ≡ y

isSet : Type ℓ → Type ℓ
isSet A = (x y : A) → isProp (x ≡ y)

-- In the agda/cubical library we call these h-levels following
-- Voevodsky instead of n-types and index by natural numbers instead
-- of ℕ₋₂. So isContr is h-level 0, isProp is h-level 1, isSet is
-- h-level 2, etc. For details see Cubical/Foundations/HLevels.agda


text:
{-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.polarity:10 -v tc.inj:40 -v tc.conv.irr:20 #-}  -- -v tc.mod.apply:100 #-}
module Issue168 where

postulate X : Set

open import Issue168b
open Membership X

postulate
  P : Nat → Set
  lemma : ∀ n → P (id n)

foo : P zero
foo = lemma _

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- A definitional interpreter
------------------------------------------------------------------------

open import Prelude

import Lambda.Syntax

module Lambda.Interpreter
  {Name : Type}
  (open Lambda.Syntax Name)
  (def : Name → Tm 1)
  where

import Equality.Propositional as E

open import Monad E.equality-with-J
open import Vec.Data E.equality-with-J

open import Delay-monad
open import Delay-monad.Bisimilarity

open import Lambda.Delay-crash

open Closure Tm

------------------------------------------------------------------------
-- The interpreter

infix 10 _∙_

mutual

  ⟦_⟧ : ∀ {i n} → Tm n → Env n → Delay-crash Value i
  ⟦ var x ⟧       ρ = return (index ρ x)
  ⟦ lam t ⟧       ρ = return (lam t ρ)
  ⟦ t₁ · t₂ ⟧     ρ = do v₁ ← ⟦ t₁ ⟧ ρ
                         v₂ ← ⟦ t₂ ⟧ ρ
                         v₁ ∙ v₂
  ⟦ call f t ⟧    ρ = do v ← ⟦ t ⟧ ρ
                         lam (def f) [] ∙ v
  ⟦ con b ⟧       ρ = return (con b)
  ⟦ if t₁ t₂ t₃ ⟧ ρ = do v₁ ← ⟦ t₁ ⟧ ρ
                         ⟦if⟧ v₁ t₂ t₃ ρ

  _∙_ : ∀ {i} → Value → Value → Delay-crash Value i
  lam t₁ ρ ∙ v₂ = later λ { .force → ⟦ t₁ ⟧ (v₂ ∷ ρ) }
  con _    ∙ _  = crash

  ⟦if⟧ : ∀ {i n} →
         Value → Tm n → Tm n → Env n → Delay-crash Value i
  ⟦if⟧ (lam _ _)   _  _  _ = crash
  ⟦if⟧ (con true)  t₂ t₃ ρ = ⟦ t₂ ⟧ ρ
  ⟦if⟧ (con false) t₂ t₃ ρ = ⟦ t₃ ⟧ ρ

------------------------------------------------------------------------
-- An example

-- The semantics of Ω is the non-terminating computation never.

Ω-loops : ∀ {i} → [ i ] ⟦ Ω ⟧ [] ∼ never
Ω-loops =
  ⟦ Ω ⟧ []                             ∼⟨⟩
  ⟦ ω · ω ⟧ []                         ∼⟨⟩
  lam ω-body [] ∙ lam ω-body []        ∼⟨ later (λ { .force →

      ⟦ ω-body ⟧ (lam ω-body [] ∷ [])       ∼⟨⟩
      lam ω-body [] ∙ lam ω-body []         ∼⟨⟩
      ⟦ Ω ⟧ []                              ∼⟨ Ω-loops ⟩∼
      never                                 ∎ }) ⟩∼

  never                                ∎

-- A more direct proof.

Ω-loops′ : ∀ {i} → [ i ] ⟦ Ω ⟧ [] ∼ never
Ω-loops′ = later λ { .force → Ω-loops′ }

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

-- Should not be accepted
f  : (@0 n : Nat) (m : Nat) → n + 0 ≡ m → Nat
f n m refl = m


text:
{-# OPTIONS --without-K --safe #-}

open import Categories.Category
open import Categories.Functor

module Categories.Adjoint.AFT.SolutionSet {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
                                          (F : Functor C D) where

open import Level

private
  module C = Category C
  module D = Category D
  module F = Functor F
  open D
  open F

record SolutionSet i : Set (o ⊔ ℓ ⊔ o′ ⊔ ℓ′ ⊔ e′ ⊔ (suc i)) where
  field
    I       : Set i
    S       : I → C.Obj
    S₀      : ∀ {A X} → X ⇒ F₀ A → I
    S₁      : ∀ {A X} (f : X ⇒ F₀ A) → S (S₀ f) C.⇒ A
    ϕ       : ∀ {A X} (f : X ⇒ F₀ A) → X ⇒ F₀ (S (S₀ f))
    commute : ∀ {A X} (f : X ⇒ F₀ A) → F₁ (S₁ f) ∘ ϕ f ≈ f

record SolutionSet′ : Set (o ⊔ ℓ ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  field
    S₀      : ∀ {A X} → X ⇒ F₀ A → C.Obj
    S₁      : ∀ {A X} (f : X ⇒ F₀ A) → S₀ f C.⇒ A
    ϕ       : ∀ {A X} (f : X ⇒ F₀ A) → X ⇒ F₀ (S₀ f)
    commute : ∀ {A X} (f : X ⇒ F₀ A) → F₁ (S₁ f) ∘ ϕ f ≈ f

SolutionSet⇒SolutionSet′ : ∀ {i} → SolutionSet i → SolutionSet′
SolutionSet⇒SolutionSet′ s = record
  { S₀      = λ f → S (S₀ f)
  ; S₁      = S₁
  ; ϕ       = ϕ
  ; commute = commute
  }
  where open SolutionSet s

SolutionSet′⇒SolutionSet : ∀ i → SolutionSet′ → SolutionSet (o ⊔ i)
SolutionSet′⇒SolutionSet i s = record
  { I       = Lift i C.Obj
  ; S       = lower
  ; S₀      = λ f → lift (S₀ f)
  ; S₁      = S₁
  ; ϕ       = ϕ
  ; commute = commute
  }
  where open SolutionSet′ s

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
postulate
  Typ : Set
  ⊢   : Typ → Set
  N   : Typ
  t   : ⊢ N

record TopPred : Set where
  constructor tp
  field nf : Typ

postulate
  inv-t[σ] : (T : Typ) → ⊢ T → TopPred

su-I′ : TopPred → Typ
su-I′ krip =
    let tp _ = inv-t[σ] _ t
        open TopPred krip
    in N

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Semigroup where

open import Cubical.Algebra.Semigroup.Base public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Function.Equals.Multi where

open import Data.Tuple.Raise
open import Data.Tuple.RaiseTypeᵣ
open import Functional
open import Function.Multi.Functions
open import Function.Multi
open import Logic
open import Logic.Predicate
open import Logic.Predicate.Multi
import      Lvl
import      Lvl.MultiFunctions as Lvl
open import Numeral.Natural
open import Structure.Setoid
open import Syntax.Function
open import Type

private variable ℓ ℓₑ : Lvl.Level
private variable n : ℕ
private variable ℓ𝓈 : Lvl.Level ^ n

module Names where
  -- Pointwise function equality for a pair of multivariate functions.
  -- Example:
  --   (f ⦗ ⊜₊(3) ⦘ g) = (∀{x}{y}{z} → (f(x)(y)(z) ≡ g(x)(y)(z)))
  ⊜₊ : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)}{B : Type{ℓ}} ⦃ equiv-B : Equiv{ℓₑ}(B) ⦄ → (As ⇉ B) → (As ⇉ B) → Stmt{ℓₑ Lvl.⊔ (Lvl.⨆(ℓ𝓈))}
  ⊜₊(n) = ∀₊(n) ∘₂ pointwise(n)(2) (_≡_)

record ⊜₊ (n : ℕ) {ℓ𝓈}{As : Types{n}(ℓ𝓈)}{B : Type{ℓ}} ⦃ equiv-B : Equiv{ℓₑ}(B) ⦄ (f : As ⇉ B) (g : As ⇉ B) : Stmt{ℓₑ Lvl.⊔ (Lvl.⨆(ℓ𝓈))} where
  constructor intro
  field proof : f ⦗ Names.⊜₊(n) ⦘ g

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda