text:
-- {-# OPTIONS -v interaction:100 #-}
module Issue810 where

postulate
  T : Set → Set

introHid : {A : Set} → T A
introHid = {!!}

data Sg {A : Set} : A → Set where
  sg : (a : A) → Sg a

intro : ∀ {A}{a : A} → Sg a
intro = {!!}

intro′ : ∀ {A}(a : A) → Sg a
intro′ = {!!}

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import lib.Base
open import lib.PathGroupoid

open import lib.path-seq.Concat
open import lib.path-seq.Inversion
open import lib.path-seq.Reasoning

module lib.path-seq.Rotations {i} {A : Type i} where

{-
The order of the arguments p, q, r follows the occurrences
of these variables in the output type
-}

pre-rotate-in : {a a' a'' : A} {q : a' =-= a''} {p : a == a'} {r : a =-= a''}
  → p ◃∙ q =ₛ r
  → q =ₛ ! p ◃∙ r
pre-rotate-in {q = q} {p = idp} {r = r} e =
  q
    =ₛ⟨ =ₛ-in (! (↯-∙∙ (idp ◃∎) q)) ⟩
  idp ◃∙ q
    =ₛ⟨ e ⟩
  r
    =ₛ⟨ =ₛ-in (! (↯-∙∙ (idp ◃∎) r)) ⟩
  idp ◃∙ r ∎ₛ

pre-rotate-out : {a a' a'' : A} {p : a == a'} {q : a' =-= a''} {r : a =-= a''}
  → q =ₛ ! p ◃∙ r
  → p ◃∙ q =ₛ r
pre-rotate-out {p = idp} {q = q} {r = r} e =
  idp ◃∙ q
    =ₛ⟨ =ₛ-in (↯-∙∙ (idp ◃∎) q) ⟩
  q
    =ₛ⟨ e ⟩
  idp ◃∙ r
    =ₛ⟨ =ₛ-in (↯-∙∙ (idp ◃∎) r) ⟩
  r ∎ₛ

pre-rotate'-in : {a a' a'' : A} {p : a == a'} {r : a =-= a''} {q : a' =-= a''}
  → r =ₛ p ◃∙ q
  → ! p ◃∙ r =ₛ q
pre-rotate'-in e =
  !ₛ (pre-rotate-in (!ₛ e))

pre-rotate'-out : {a a' a'' : A} {r : a =-= a''} {p : a == a'} {q : a' =-= a''}
  → ! p ◃∙ r =ₛ q
  → r =ₛ p ◃∙ q
pre-rotate'-out e =
  !ₛ (pre-rotate-out (!ₛ e))

pre-rotate-seq-in : {a a' a'' : A} {q : a' =-= a''} {p : a =-= a'} {r : a =-= a''}
  → p ∙∙ q =ₛ r
  → q =ₛ seq-! p ∙∙ r
pre-rotate-seq-in {q = q} {p = []} {r = r} e = e
pre-rotate-seq-in {q = q} {p = p ◃∙ s} {r = r} e =
  q
    =ₛ⟨ pre-rotate-seq-in {q = q} {p = s} {r = ! p ◃∙ r} (pre-rotate-in e) ⟩
  seq-! s ∙∙ ! p ◃∙ r
    =ₛ⟨ =ₛ-in (ap ↯ (! (∙∙-assoc (seq-! s) (! p ◃∎) r))) ⟩
  seq-! (p ◃∙ s) ∙∙ r ∎ₛ

pre-rotate'-seq-in : {a a' a'' : A} {p : a =-= a'} {r : a =-= a''} {q : a' =-= a''}
  → r =ₛ p ∙∙ q
  → seq-! p ∙∙ r =ₛ q
pre-rotate'-seq-in {p = p} {r = r} {q = q} e =
  !ₛ (pre-rotate-seq-in {q = q} {p} {r} (!ₛ e))

post-rotate'-in : {a a' a'' : A}
  → {r : a =-= a''} {q : a' == a''} {p : a =-= a'}
  → r =ₛ p ∙▹ q
  → r ∙▹ ! q =ₛ p
post-rotate'-in {r = r} {q = idp} {p = p} e =
  r ∙▹ idp
    =ₛ⟨ =ₛ-in (↯-∙∙ r (idp ◃∎) ∙ ∙-unit-r (↯ r)) ⟩
  r
    =ₛ⟨ e ⟩
  p ∙▹ idp
    =ₛ⟨ =ₛ-in (↯-∙∙ p (idp ◃∎) ∙ ∙-unit-r (↯ p)) ⟩
  p ∎ₛ

post-rotate-in : {a a' a'' : A}
  → {p : a =-= a'} {r : a =-= a''} {q : a' == a''}
  → p ∙▹ q =ₛ r
  → p =ₛ r ∙▹ ! q
post-rotate-in {p = p} {r = r} {q = q} e =
  !ₛ (post-rotate'-in (!ₛ e))

post-rotate-out : {a a' a'' : A}
  → {p : a =-= a'} {q : a' == a''} {r : a =-= a''}
  → p =ₛ r ∙▹ ! q
  → p ∙▹ q =ₛ r
post-rotate-out {p = p} {q = q} {r = r} e = =ₛ-in $
  ↯ (p ∙▹ q)
    =⟨ ap (λ v → ↯ (p ∙▹ v)) (! (!-! q)) ⟩
  ↯ (p ∙▹ ! (! q))
    =⟨ =ₛ-out (post-rotate'-in {r = p} {q = ! q} {p = r} e) ⟩
  ↯ r =∎

post-rotate'-seq-in : {a a' a'' : A}
  → {r : a =-= a''} {q : a' =-= a''} {p : a =-= a'}
  → r =ₛ p ∙∙ q
  → r ∙∙ seq-! q =ₛ p
post-rotate'-seq-in {r = r} {q = []} {p = p} e =
  r ∙∙ []
    =ₛ⟨ =ₛ-in (ap ↯ (∙∙-unit-r r)) ⟩
  r
    =ₛ⟨ e ⟩
  p ∙∙ []
    =ₛ⟨ =ₛ-in (ap ↯ (∙∙-unit-r p)) ⟩
  p ∎ₛ
post-rotate'-seq-in {r = r} {q = q ◃∙ s} {p = p} e =
  r ∙∙ (seq-! s ∙▹ ! q)
    =ₛ⟨ =ₛ-in (ap ↯ (! (∙∙-assoc r (seq-! s) (! q ◃∎)))) ⟩
  (r ∙∙ seq-! s) ∙▹ ! q
    =ₛ⟨ post-rotate'-in {r = r ∙∙ seq-! s} {q = q} {p = p} $
        post-rotate'-seq-in {r = r} {s} {p ∙▹ q} $
        r
          =ₛ⟨ e ⟩
        p ∙∙ (q ◃∙ s)
          =ₛ⟨ =ₛ-in (ap ↯ (! (∙∙-assoc p (q ◃∎) s))) ⟩
        (p ∙▹ q) ∙∙ s ∎ₛ
      ⟩
  p ∎ₛ

post-rotate-seq-in : {a a' a'' : A}
  → {p : a =-= a'} {r : a =-= a''} {q : a' =-= a''}
  → p ∙∙ q =ₛ r
  → p =ₛ r ∙∙ (seq-! q)
post-rotate-seq-in {p = p} {r = r} {q = q} e =
  !ₛ (post-rotate'-seq-in {r = r} {q = q} {p = p} (!ₛ e))

post-rotate'-seq-out : {a a' a'' : A}
  → {r : a =-= a''} {p : a =-= a'} {q : a' =-= a''}
  → r ∙∙ seq-! q =ₛ p
  → r =ₛ p ∙∙ q
post-rotate'-seq-out {r = r} {p = p} {q = q} e =
  r
    =ₛ⟨ post-rotate-seq-in {p = r} {r = p} {q = seq-! q} e ⟩
  p ∙∙ seq-! (seq-! q)
    =ₛ⟨ =ₛ-in (ap (λ v → ↯ (p ∙∙ v)) (seq-!-seq-! q)) ⟩
  p ∙∙ q ∎ₛ

post-rotate-seq-out : {a a' a'' : A}
  → {p : a =-= a'} {q : a' =-= a''} {r : a =-= a''}
  → p =ₛ r ∙∙ seq-! q
  → p ∙∙ q =ₛ r
post-rotate-seq-out e =
  !ₛ (post-rotate'-seq-out (!ₛ e))

ext: agda

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
------------------------------------------------------------------------
-- Is-equivalence, defined in terms of contractible fibres
------------------------------------------------------------------------

-- Partly based on Voevodsky's work on univalent foundations.

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

open import Equality

module Equivalence.Contractible-preimages
  {e⁺} (eq : ∀ {a p} → Equality-with-J a p e⁺) where

open Derived-definitions-and-properties eq

open import Prelude as P hiding (id)

open import Bijection eq using (_↔_)
open import Equality.Decision-procedures eq
open import H-level eq as H-level
open import H-level.Closure eq
open import Preimage eq as Preimage using (_⁻¹_)
open import Surjection eq using (_↠_)

private
  variable
    a b ℓ p q : Level
    A B       : Type a
    f g       : A → B

------------------------------------------------------------------------
-- Is-equivalence

-- A function f is an equivalence if all preimages under f are
-- contractible.

Is-equivalence :
  {A : Type a} {B : Type b} →
  (A → B) → Type (a ⊔ b)
Is-equivalence f = ∀ y → Contractible (f ⁻¹ y)

abstract

  -- Is-equivalence f is a proposition, assuming extensional equality.

  propositional :
    Extensionality (a ⊔ b) (a ⊔ b) →
    {A : Type a} {B : Type b} (f : A → B) →
    Is-proposition (Is-equivalence f)
  propositional {a = a} ext f =
    Π-closure (lower-extensionality a lzero ext) 1 λ _ →
      Contractible-propositional ext

  -- If the domain is contractible and the codomain is propositional,
  -- then Is-equivalence f is contractible.

  sometimes-contractible :
    Extensionality (a ⊔ b) (a ⊔ b) →
    {A : Type a} {B : Type b} {f : A → B} →
    Contractible A → Is-proposition B →
    Contractible (Is-equivalence f)
  sometimes-contractible {a = a} ext A-contr B-prop =
    Π-closure (lower-extensionality a lzero ext) 0 λ _ →
      cojoin ext (Σ-closure 0 A-contr (λ _ → +⇒≡ B-prop))

  -- Is-equivalence f is not always contractible.

  not-always-contractible₁ :
    ∃ λ (A : Type a) → ∃ λ (B : Type b) → ∃ λ (f : A → B) →
      Is-proposition A × Contractible B ×
      ¬ Contractible (Is-equivalence f)
  not-always-contractible₁ =
    ⊥ ,
    ↑ _ ⊤ ,
    const (lift tt) ,
    ⊥-propositional ,
    ↑-closure 0 ⊤-contractible ,
    λ c → ⊥-elim (proj₁ (proj₁ (proj₁ c (lift tt))))

  not-always-contractible₂ :
    ∃ λ (A : Type a) → ∃ λ (B : Type b) → ∃ λ (f : A → B) →
      Contractible A × Is-set B ×
      ¬ Contractible (Is-equivalence f)
  not-always-contractible₂ =
    ↑ _ ⊤ ,
    ↑ _ Bool ,
    const (lift true) ,
    ↑-closure 0 ⊤-contractible ,
    ↑-closure 2 Bool-set ,
    λ c → Bool.true≢false (cong lower
            (proj₂ (proj₁ (proj₁ c (lift false)))))

-- Is-equivalence respects extensional equality.

respects-extensional-equality :
  (∀ x → f x ≡ g x) →
  Is-equivalence f → Is-equivalence g
respects-extensional-equality f≡g f-eq = λ b →
  H-level.respects-surjection
    (_↔_.surjection (Preimage.respects-extensional-equality f≡g))
    0
    (f-eq b)

-- If f is an equivalence, then it has an inverse.

inverse :
  {@0 A : Type a} {@0 B : Type b} {@0 f : A → B} →
  Is-equivalence f → B → A
inverse eq y = proj₁ (proj₁ (eq y))

right-inverse-of :
  {@0 A : Type a} {@0 B : Type b} {@0 f : A → B} →
  (eq : Is-equivalence f) → ∀ x → f (inverse eq x) ≡ x
right-inverse-of eq x = proj₂ (proj₁ (eq x))

abstract

  left-inverse-of :
    (eq : Is-equivalence f) → ∀ x → inverse eq (f x) ≡ x
  left-inverse-of {f = f} eq x =
    cong (proj₁ {B = λ x′ → f x′ ≡ f x}) (
      proj₁ (eq (f x))  ≡⟨ proj₂ (eq (f x)) (x , refl (f x)) ⟩∎
      (x , refl (f x))  ∎)

-- All fibres of an equivalence over a given point are equal to a
-- given fibre.

irrelevance :
  {@0 A : Type a} {@0 B : Type b} {@0 f : A → B} →
  (eq : Is-equivalence f) →
  ∀ y (p : f ⁻¹ y) → (inverse eq y , right-inverse-of eq y) ≡ p
irrelevance eq y = proj₂ (eq y)

abstract

  -- The two proofs left-inverse-of and right-inverse-of are
  -- related.

  left-right-lemma :
    (eq : Is-equivalence f) →
    ∀ x → cong f (left-inverse-of eq x) ≡ right-inverse-of eq (f x)
  left-right-lemma {f = f} eq x =
    lemma₁ f _ _ (lemma₂ (irrelevance eq (f x) (x , refl (f x))))
    where
    lemma₁ : {x y : A} (f : A → B) (p : x ≡ y) (q : f x ≡ f y) →
             refl (f y) ≡ trans (cong f (sym p)) q →
             cong f p ≡ q
    lemma₁ f = elim
      (λ {x y} p → ∀ q → refl (f y) ≡ trans (cong f (sym p)) q →
                         cong f p ≡ q)
      (λ x q hyp →
         cong f (refl x)                  ≡⟨ cong-refl f ⟩
         refl (f x)                       ≡⟨ hyp ⟩
         trans (cong f (sym (refl x))) q  ≡⟨ cong (λ p → trans (cong f p) q) sym-refl ⟩
         trans (cong f (refl x)) q        ≡⟨ cong (λ p → trans p q) (cong-refl f) ⟩
         trans (refl (f x)) q             ≡⟨ trans-reflˡ _ ⟩∎
         q                                ∎)

    lemma₂ : ∀ {f : A → B} {y} {f⁻¹y₁ f⁻¹y₂ : f ⁻¹ y}
             (p : f⁻¹y₁ ≡ f⁻¹y₂) →
             proj₂ f⁻¹y₂ ≡
             trans (cong f (sym (cong (proj₁ {B = λ x → f x ≡ y}) p)))
                   (proj₂ f⁻¹y₁)
    lemma₂ {f = f} {y = y} =
      let pr = proj₁ {B = λ x → f x ≡ y} in
      elim {A = f ⁻¹ y}
        (λ {f⁻¹y₁ f⁻¹y₂} p →
           proj₂ f⁻¹y₂ ≡
             trans (cong f (sym (cong pr p))) (proj₂ f⁻¹y₁))
        (λ f⁻¹y →
           proj₂ f⁻¹y                                               ≡⟨ sym $ trans-reflˡ _ ⟩
           trans (refl (f (proj₁ f⁻¹y))) (proj₂ f⁻¹y)               ≡⟨ cong (λ p → trans p (proj₂ f⁻¹y)) (sym (cong-refl f)) ⟩
           trans (cong f (refl (proj₁ f⁻¹y))) (proj₂ f⁻¹y)          ≡⟨ cong (λ p → trans (cong f p) (proj₂ f⁻¹y)) (sym sym-refl) ⟩
           trans (cong f (sym (refl (proj₁ f⁻¹y)))) (proj₂ f⁻¹y)    ≡⟨ cong (λ p → trans (cong f (sym p)) (proj₂ f⁻¹y))
                                                                            (sym (cong-refl pr)) ⟩∎
           trans (cong f (sym (cong pr (refl f⁻¹y)))) (proj₂ f⁻¹y)  ∎)

  right-left-lemma :
    (eq : Is-equivalence f) →
    ∀ x →
    cong (inverse eq) (right-inverse-of eq x) ≡
    left-inverse-of eq (inverse eq x)
  right-left-lemma {f = f} eq x =
    let f⁻¹ = inverse eq in
    subst
      (λ x → cong f⁻¹ (right-inverse-of eq x) ≡
             left-inverse-of eq (f⁻¹ x))
      (right-inverse-of eq x)
      (cong f⁻¹ (right-inverse-of eq (f (f⁻¹ x)))             ≡⟨ cong (cong f⁻¹) $ sym $ left-right-lemma eq _ ⟩

       cong f⁻¹ (cong f (left-inverse-of eq (f⁻¹ x)))         ≡⟨ cong-∘ f⁻¹ f _ ⟩

       cong (f⁻¹ ∘ f) (left-inverse-of eq (f⁻¹ x))            ≡⟨ cong-roughly-id (f⁻¹ ∘ f) (λ _ → true) (left-inverse-of eq _) _ _
                                                                   (λ z _ → left-inverse-of eq z) ⟩
       trans (left-inverse-of eq (f⁻¹ (f (f⁻¹ x))))
         (trans (left-inverse-of eq (f⁻¹ x))
            (sym (left-inverse-of eq (f⁻¹ x))))               ≡⟨ cong (trans _) $ trans-symʳ _ ⟩

       trans (left-inverse-of eq (f⁻¹ (f (f⁻¹ x)))) (refl _)  ≡⟨ trans-reflʳ _ ⟩∎

       left-inverse-of eq (f⁻¹ (f (f⁻¹ x)))                   ∎)

abstract

  -- If Σ-map P.id f is an equivalence, then f is also an equivalence.

  drop-Σ-map-id :
    {A : Type a} {P : A → Type p} {Q : A → Type q}
    (f : ∀ {x} → P x → Q x) →
    Is-equivalence {A = Σ A P} {B = Σ A Q} (Σ-map P.id f) →
    ∀ x → Is-equivalence (f {x = x})
  drop-Σ-map-id {p = ℓp} {q = ℓq} {A = A} {P = P} {Q = Q} f eq x z =
    H-level.respects-surjection surj 0 (eq (x , z))
    where
    map-f : Σ A P → Σ A Q
    map-f = Σ-map P.id f

    to-P : ∀ {x y} {p : ∃ Q} → (x , f y) ≡ p → Type (ℓp ⊔ ℓq)
    to-P {y = y} {p} _ = ∃ λ y′ → f y′ ≡ proj₂ p

    to : map-f ⁻¹ (x , z) → f ⁻¹ z
    to ((x′ , y) , eq) = elim¹ to-P (y , refl (f y)) eq

    from : f ⁻¹ z → map-f ⁻¹ (x , z)
    from (y , eq) = (x , y) , cong (_,_ x) eq

    to∘from : ∀ p → to (from p) ≡ p
    to∘from (y , eq) = elim¹
      (λ {z′} (eq : f y ≡ z′) →
         _≡_ {A = ∃ λ (y : P x) → f y ≡ z′}
             (elim¹ to-P (y , refl (f y)) (cong (_,_ x) eq))
             (y , eq))
      (elim¹ to-P (y , refl (f y)) (cong (_,_ x) (refl (f y)))  ≡⟨ cong (elim¹ to-P (y , refl (f y))) $
                                                                        cong-refl (_,_ x) ⟩
       elim¹ to-P (y , refl (f y)) (refl (x , f y))             ≡⟨ elim¹-refl to-P _ ⟩∎
       (y , refl (f y))                                         ∎)
      eq

    surj : map-f ⁻¹ (x , z) ↠ f ⁻¹ z
    surj = record
      { logical-equivalence = record { to = to; from = from }
      ; right-inverse-of    = to∘from
      }

  -- A "computation" rule for drop-Σ-map-id.

  inverse-drop-Σ-map-id :
    {A : Type a} {P : A → Type p} {Q : A → Type q}
    {f : ∀ {x} → P x → Q x} {x : A} {y : Q x}
    {eq : Is-equivalence {A = Σ A P} {B = Σ A Q} (Σ-map P.id f)} →
    inverse (drop-Σ-map-id f eq x) y ≡
    subst P (cong proj₁ (right-inverse-of eq (x , y)))
      (proj₂ (inverse eq (x , y)))
  inverse-drop-Σ-map-id
    {P = P} {Q = Q} {f = f} {x = x} {y = y} {eq = eq} =

    let lemma = elim¹
          (λ {q′} eq →
             cong proj₁
               (proj₂ (other-singleton-contractible (Σ-map P.id f p′))
                  (q′ , eq)) ≡
             eq)
          (cong proj₁
             (proj₂ (other-singleton-contractible (Σ-map P.id f p′))
                (Σ-map P.id f p′ , refl _))                           ≡⟨ cong (cong proj₁) $
                                                                         other-singleton-contractible-refl _ ⟩

           cong proj₁ (refl _)                                        ≡⟨ cong-refl _ ⟩∎

           refl _                                                     ∎)
          _
    in
    proj₁
      (subst
         (λ ((_ , y) , _) → f ⁻¹ y)
         (proj₂
            (other-singleton-contractible (Σ-map P.id f p′))
            (q′ , right-inverse-of eq q′))
         (proj₂ p′ , refl _))                                 ≡⟨ cong proj₁ $ push-subst-pair _ _ ⟩

    subst
      (λ ((x , _) , _) → P x)
      (proj₂
         (other-singleton-contractible (Σ-map P.id f p′))
         (q′ , right-inverse-of eq q′))
      (proj₂ p′)                                              ≡⟨ trans (subst-∘ _ _ _) (subst-∘ _ _ _) ⟩

    subst P
      (cong proj₁ $ cong proj₁ $
       proj₂
         (other-singleton-contractible (Σ-map P.id f p′))
         (q′ , right-inverse-of eq q′))
      (proj₂ p′)                                              ≡⟨ cong (λ eq → subst P (cong proj₁ eq) (proj₂ p′))
                                                                 lemma ⟩∎
    subst P
      (cong proj₁ (right-inverse-of eq q′))
      (proj₂ p′)                                              ∎
    where
    q′ : ∃ Q
    q′ = x , y

    p′ : ∃ P
    p′ = inverse eq q′

------------------------------------------------------------------------
-- _≃_

-- A notion of equivalence.

infix 4 _≃_

_≃_ : Type a → Type b → Type (a ⊔ b)
A ≃ B = ∃ λ (f : A → B) → Is-equivalence f

-- An identity equivalence.

id : A ≃ A
id = P.id , singleton-contractible

-- Equalities can be converted to equivalences.

≡⇒≃ : A ≡ B → A ≃ B
≡⇒≃ = elim (λ {A B} _ → A ≃ B) (λ _ → id)

-- If ≡⇒≃ is applied to reflexivity, then the result is equal to id.

≡⇒≃-refl : ≡⇒≃ (refl A) ≡ id
≡⇒≃-refl = elim-refl (λ {A B} _ → A ≃ B) (λ _ → id)

-- Univalence for fixed types.

Univalence′ : (A B : Type ℓ) → Type (lsuc ℓ)
Univalence′ A B = Is-equivalence (≡⇒≃ {A = A} {B = B})

-- Univalence.

Univalence : ∀ ℓ → Type (lsuc ℓ)
Univalence ℓ = {A B : Type ℓ} → Univalence′ A B

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Decidable setoid membership over lists
------------------------------------------------------------------------

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

open import Relation.Binary using (Decidable; DecSetoid)

module Data.List.Membership.DecSetoid {a ℓ} (DS : DecSetoid a ℓ) where

open import Data.List.Relation.Unary.Any using (any)
open DecSetoid DS

------------------------------------------------------------------------
-- Re-export contents of propositional membership

open import Data.List.Membership.Setoid (DecSetoid.setoid DS) public

------------------------------------------------------------------------
-- Other operations

infix 4 _∈?_

_∈?_ : Decidable _∈_
x ∈? xs = any (x ≟_) xs


text:
{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

-- If we could prove ifInjective then we could true ≡ false (see Dan
-- Licata example in
-- http://thread.gmane.org/gmane.comp.lang.agda/4511).

module FOTC.Base.Consistency.IfInjective where

open import FOTC.Base

------------------------------------------------------------------------------

postulate ifInjective : ∀ {b b' t t'} →
                        (if b then t else t') ≡ (if b' then t else t') → b ≡ b'
{-# ATP prove ifInjective #-}

true≡false : true ≡ false
true≡false = ifInjective {true} {false} {true} {true}
                         (trans (if-true true) (sym (if-false true)))

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Logic.Classical
open import Logic
import      Lvl
open import Type
open import Structure.Setoid

-- Elementary Plane Geometry.
-- An axiomatic approach to plane geometry in first order logic.
-- The axiomatic system used here is usually called "Tarski's axioms", and plane geometry is also known as two-dimensional Euclidean geometry.
module Geometry.Axioms
  {ℓₚ ℓₚₑ ℓₗₗₑ ℓₗᵢₗ}
  (Point : Type{ℓₚ}) ⦃ Point-equiv : Equiv{ℓₚₑ}(Point) ⦄
  (Equidistanced : (Point ⨯ Point) → (Point ⨯ Point) → Stmt{ℓₗₗₑ}) -- Two pairs of points have the same distance between each other.
  (Aligned : Point → Point → Point → Stmt{ℓₗᵢₗ})                   -- Three points are aligned in a weak order. The second point is between the first and the third in a line.
  ⦃ classical : ∀{ℓ}{P : Stmt{ℓ}} → Classical(P) ⦄
  where

open import Data.Tuple.Equivalence
open import Functional
open import Functional.Combinations
open import Logic.Predicate
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Sets.ExtensionalPredicateSet renaming (_≡_ to _≡ₛ_)
open import Structure.Relator.Equivalence
open import Structure.Relator.Ordering
open import Structure.Relator.Properties
open import Structure.Relator
open import Structure.Setoid.Uniqueness
open import Syntax.Function
open import Syntax.Implication
open import Syntax.Transitivity
open import Syntax.Type

private variable ℓ ℓ₁ ℓ₂ ℓₗ ℓₗ₁ ℓₗ₂ : Lvl.Level
private variable p a b c d e p₁ p₂ pᵢ pₒ pᵣ a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂ e₁ e₂ i m₁ m₂ : Point
private variable P Q : Point → Stmt{ℓ}

-- Three points are aligned in a strict order. The second point is between the first and the third in a line without being the first or the second.
Between : Point → Point → Point → Stmt
Between a b c = (Aligned a b c) ∧ ((a ≢ b) ∧ (b ≢ c))

-- Three points are collinear when they all are points of a single line.
Collinear : Point → Point → Point → Stmt
Collinear a b c = (Aligned a b c) ∨ (Aligned b c a) ∨ (Aligned c a b)

Aligned₄ : Point → Point → Point → Point → Stmt
Aligned₄ = combine₄Fn₃Op₂ Aligned (_∧_)

-- The equivalence on points.
_≡ₚ_ = Equiv._≡_ Point-equiv

-- Source: Tarski's axioms of geometry (https://en.wikipedia.org/wiki/Tarski%27s_axioms @ 2020-06-14).
-- TODO: Are there any modifications of the axioms when working in constructive logic?
record Axioms : Typeω where
  field
    ⦃ Equidistanced-relator ⦄ : BinaryRelator(Equidistanced)
    ⦃ Aligned-relator ⦄ : TrinaryRelator(Aligned)
    -- ⦃ Point-equivalence-classical ⦄ : Classical₂(_≡ₚ_)
    -- ⦃ Equidistanced-classical ⦄ : Classical₂(Equidistanced)
    -- ⦃ Aligned-classical ⦄ : Classical₃(Aligned)

    -- The distance between p₁ and p₂ is the same as the distance between p₂ and p₁.
    -- The order of the points in the equidistance relation does not matter.
    -- Example:
    --   • (p₁) <--- (p₂)
    --   • (p₁) ---> (p₂)
    --   These two drawings depict lines between points p₁ and p₂. They have the same length.
    --   So there is no need to draw an arrow head on the lines when referring to the length of a line.
    -- Also called: A1 in Metamathematische Methoden in der Geometrie.
    Equidistanced-flipped : Equidistanced(p₁ , p₂)(p₂ , p₁)

    -- Equidistance is a transitive relation.
    -- Example:
    --   la: (a₁) ---- (a₂)
    --   lb: (b₁) ---- (b₂)
    --   lc: (c₁) ---- (c₂)
    --   Here is a drawing of three lines.
    --   The line la have the same length as lb, and the line la have the same length as lc. Then lb have the same length as lc.
    -- Also called: A2 in Metamathematische Methoden in der Geometrie.
    Equidistanced-symmetric-transitivity : Equidistanced(a₁ , a₂)(b₁ , b₂) → Equidistanced(a₁ , a₂)(c₁ , c₂) → Equidistanced(b₁ , b₂)(c₁ , c₂)

    -- If two points have the same distance as the distance between a single point with itself, then they are the same point.
    -- Essentially, if two points have no distance between each other, they are the same point.
    -- Example:
    --   (p₁) ---------- (p₂)
    --   (p)
    --   Here p₁ and p₂ are arbitrary points, and a line between them is depicted.
    --   The line from p to p is also depicted (as a point).
    --   Currently, these lines do not have the same length, and for p₁ and p₂ to have the same distance as the single point line consisting of p, the line must collapse to a single point, making p₁ and p₂ the same point.
    -- Also called:
    -- • Identity axiom for the `Equidistance` relation.
    -- • A3 in Metamathematische Methoden in der Geometrie.
    Equidistanced-point : Equidistanced(p₁ , p₂)(p , p) → (p₁ ≡ p₂)

    -- Given two lines, there exists a line extending the first line so that the extension part is of the same length as the second line.
    -- Essentially, given a starting point and a direction, it is always possible to construct a line of the same length as an another already existing line.
    -- Or: It is always possible to extend a line by the length of another line.
    -- Example:
    --   Given two lines:
    --   (p) <-- (a₁)
    --   (a₂) ------> (b₂)
    --   it is possible to construct an extension of the first line like this:
    --   (b₁) <------(p)-- (a₁)
    --   The extension from a₁ to b₁ have the same direction as the first line (a₁ to p) and the same length as the second line (from a₂ to b₂).
    -- Also called:
    -- • A4 in Metamathematische Methoden in der Geometrie.
    segment-construction : ∃(b₁ ↦ (Aligned a₁ p b₁) ∧ Equidistanced(p , b₁)(a₂ , b₂))

    -- Given two bisected triangles, if all except one of the non-bisected sides of the first triangle have the same length as the second one's, then the unknown side of the first triangle is also congruent to the unknown side of the second.
    --
    -- Note: If any of the points other than (a,b) or (a,d) are equal, then the result follows from the assumptions.
    --         (d)\__
    --        /  \_  \__
    --      /      \_   \__
    --    /          \     \
    --  (a)__________(b)___(c)
    --
    -- Also called:
    -- • A5 in Metamathematische Methoden in der Geometrie.
    five-segment : (a₁ ≢ b₁) → (Aligned a₁ b₁ c₁) → (Aligned a₂ b₂ c₂) → Equidistanced(a₁ , b₁)(a₂ , b₂) → Equidistanced(b₁ , c₁)(b₂ , c₂) → Equidistanced(a₁ , d₁)(a₂ , d₂) → Equidistanced(b₁ , d₁)(b₂ , d₂) → Equidistanced(c₁ , d₁)(c₂ , d₂)

    -- If a point is between two identical points, then they are the same point.
    -- Alternatively, if a point is in a line consisting of only a single point, then the point is the single point.
    -- Example:
    --   (p₁) ------(a)--- (p₂)
    --   Here, a line from p₁ to p₂ is depicted, and a point a is in this line.
    --   But if p₁ and p₂ would be the same point p, then the line would collapse to a single point, making a and p the same.
    -- Also called:
    -- • Identity axiom for the `Aligned` relation.
    -- • A6 in Metamathematische Methoden in der Geometrie.
    Aligned-point : (Aligned p a p) → (a ≡ p)

    -- Given two connected lines and one point in each of the lines, two lines connecting the points and the endpoints of the other line have an intersection point.
    -- Example:
    --         (c)
    --       /     \
    --    (m₁)\   /(m₂)
    --    /   _(i)_   \
    --  (a)__/     \__(b)
    -- Also called:
    -- • Axiom of Pasch.
    -- • Inner Pasch.
    -- • A7 in Metamathematische Methoden in der Geometrie.
    Aligned-intersection : (Aligned a m₁ c) → (Aligned b m₂ c) → ∃(i ↦ (Aligned m₁ i b) ∧ (Aligned m₂ i a))

    -- Also called:
    -- • Axiom schema of Continuity
    -- • A11' in Metamathematische Methoden in der Geometrie.
    Aligned-continuity : ∃(a ↦ ∀{x y} → P(x) → Q(y) → (Aligned a x y)) → ∃(a ↦ ∀{x y} → P(x) → Q(y) → (Aligned x a y))

    -- A triangle exists.
    -- This excludes the possibility of this theory describing 0 or 1-dimensional spaces when using the standard interpretation of the axioms.
    -- Example:
    --    (c)
    --   /   \
    -- (a)___(b)
    -- Also called:
    -- • A8 in Metamathematische Methoden in der Geometrie.
    lower-dimension₂ : ∃{Obj = Point ⨯ Point ⨯ Point}(\(a , b , c) → (¬ Aligned a b c) ∧ (¬ Aligned b c a) ∧ (¬ Aligned c a b))

    -- Also called:
    -- • A9 in Metamathematische Methoden in der Geometrie.
    upper-dimension₂ : Equidistanced(a , p₁)(a , p₂) → Equidistanced(b , p₁)(b , p₂) → Equidistanced(c , p₁)(c , p₂) → (p₁ ≢ p₂) → (Aligned a b c) ∨ (Aligned b c a) ∨ (Aligned c a b)

    -- Given three points, they are either collinear (forming a line), or there is a circumcentered point for the triangle of the three points (a point where the distance between this point and all three vertices are equal).
    -- Example:
    --   Here is an example of the different cases depicted:
    --   • (a) ----(b)------ (c)
    --   • (b) ----(c)------ (a)
    --   • (c) ----(a)------ (b)
    --   •      (a)\__
    --         /  ‖   \__
    --       /     ‖      \
    --     (b)______‖______(c)
    --       \___   ‖  ___/
    --           \_(m)_/
    --     or when the triangle is equilateral:
    --        (a)
    --        / \
    --       /   \
    --      / (m) \
    --     /_______\
    --   (b)       (c)
    -- Also called:
    -- • Axiom of Euclid.
    -- • Variant of A10 in Metamathematische Methoden in der Geometrie.
    center-of-3 : (Collinear a b c) ∨ ∃(m ↦ Equidistanced(a , m)(b , m) ∧ Equidistanced(a , m)(c , m))

module _ ⦃ axioms : Axioms ⦄ where
  open Axioms(axioms)

  -- A line constructed by the points `a` and `b` have an intersection point on a circle with the center point `c` and radius point `pᵣ` when a part of the line.
  -- Also called:
  -- • CA in Metamathematische Methoden in der Geometrie.
  -- circle-line-intersection : (Aligned₄ c pᵢ pᵣ pₒ) → Equidistanced(c , a)(c , pᵢ) → Equidistanced(c , b)(c , pₒ) → ∃(i ↦ Equidistanced(c , i)(c , pᵣ) ∧ (Aligned a i b))

  instance
    -- Identical pairs of points have the same distance between each other.
    -- Also called: 2.1 in Metamathematische Methoden in der Geometrie.
    Equidistanced-reflexivity : Reflexivity(Equidistanced)
    Reflexivity.proof Equidistanced-reflexivity {p₁ , p₂} = Equidistanced-symmetric-transitivity (Equidistanced-flipped {p₂}{p₁}) (Equidistanced-flipped {p₂}{p₁})

  instance
    -- Also called: 2.2 in Metamathematische Methoden in der Geometrie.
    Equidistanced-symmetry : Symmetry(Equidistanced)
    Symmetry.proof Equidistanced-symmetry p = Equidistanced-symmetric-transitivity p (reflexivity(Equidistanced))

  instance
    -- Also called: 2.3 in Metamathematische Methoden in der Geometrie.
    Equidistanced-transitivity : Transitivity(Equidistanced)
    Transitivity.proof Equidistanced-transitivity p q = Equidistanced-symmetric-transitivity (symmetry(Equidistanced) p) q

  instance
    -- Also called: 2.7 in Metamathematische Methoden in der Geometrie.
    Equidistanced-equivalence : Equivalence(Equidistanced)
    Equidistanced-equivalence = intro

  -- The distance between a point and itself is the same for all points.
  -- Also called: 2.8 in Metamathematische Methoden in der Geometrie.
  Equidistanced-points : Equidistanced(a , a) (b , b)
  Equidistanced-points {a}{b}
    with [∃]-intro p ⦃ [∧]-intro _ bpaa ⦄ ← segment-construction{a}{b} {a}{a}
    =
      • (b ≡ b) ∧ (p ≡ b)            :-[ [∧]-intro (reflexivity(_≡_)) (symmetry(_≡_) (Equidistanced-point bpaa)) ]
      • Equidistanced(b , p) (b , p) :-[ reflexivity(Equidistanced) ]
      ⇒₂-[ substitute₂ᵣ(Equidistanced) ]
      Equidistanced(b , p) (b , b) ⇒-[ Equidistanced-symmetric-transitivity bpaa ]
      Equidistanced(a , a) (b , b) ⇒-end

  -- Addition of two distances when the points are in a line.
  -- Also called: 2.11 in Metamathematische Methoden in der Geometrie.
  segment-sum : (Aligned a₁ b₁ c₁) → (Aligned a₂ b₂ c₂) → Equidistanced(a₁ , b₁)(a₂ , b₂) → Equidistanced(b₁ , c₁)(b₂ , c₂) → Equidistanced(a₁ , c₁)(a₂ , c₂)
  segment-sum {a₁ = a₁}{b₁ = b₁} abc₁ abc₂ ab₁ab₂ bc₁bc₂ with excluded-middle(a₁ ≡ b₁)
  ... | [∨]-introₗ a₁b₁
    with a₂b₂ ← Equidistanced-point (symmetry(Equidistanced) (substitute₂ₗ(Equidistanced) ([∧]-intro a₁b₁ (reflexivity(_≡ₚ_))) ab₁ab₂))
    = substitute₂(Equidistanced) ([∧]-intro (symmetry(_≡ₚ_) a₁b₁) (reflexivity(_≡ₚ_))) ([∧]-intro (symmetry(_≡ₚ_) a₂b₂) (reflexivity(_≡ₚ_))) bc₁bc₂
  ... | [∨]-introᵣ na₁b₁ =
    Equidistanced-flipped
    🝖 (five-segment
      na₁b₁
      abc₁
      abc₂
      ab₁ab₂
      bc₁bc₂
      Equidistanced-points
      (Equidistanced-flipped 🝖 ab₁ab₂ 🝖 Equidistanced-flipped)
    )
    🝖 Equidistanced-flipped

  -- The segment extension axiom constructs unique points when the given pair of points forms a line segment to extend.
  -- Also called: 2.12 in Metamathematische Methoden in der Geometrie.
  segment-construction-uniqueness : (a₁ ≢ p) → Unique(b₁ ↦ (Aligned a₁ p b₁) ∧ Equidistanced(p , b₁)(a₂ , b₂))
  segment-construction-uniqueness na₁p ([∧]-intro al-a₁p₁x eq-p₁xa₂b₂) ([∧]-intro al-a₁p₁y eq-p₁ya₂b₂)
    with pxpy ← transitivity(Equidistanced) eq-p₁xa₂b₂ (symmetry(Equidistanced) eq-p₁ya₂b₂)
    with a₁xa₁y ← segment-sum al-a₁p₁x al-a₁p₁y (reflexivity(Equidistanced)) pxpy
    = Equidistanced-point (five-segment na₁p al-a₁p₁x al-a₁p₁y (reflexivity(Equidistanced)) pxpy (reflexivity(Equidistanced)) (reflexivity(Equidistanced)))

  -- Two points are always aligned.
  -- Also called: 3.1 in Metamathematische Methoden in der Geometrie.
  Aligned-reflexivityᵣ : Aligned a b b
  Aligned-reflexivityᵣ {a}{b}
    with [∃]-intro p ⦃ [∧]-intro alig equi ⦄ ← segment-construction{a}{b} {a}{a}
    = substitute₃-unary₃(Aligned) (symmetry(_≡_) (Equidistanced-point equi)) alig

  -- A single point is always aligned with itself.
  Aligned-reflexivity : Aligned a a a
  Aligned-reflexivity = Aligned-reflexivityᵣ

  -- When three points are aligned in one direction, they are also aligned in the opposite direction.
  -- Also called: 3.2 in Metamathematische Methoden in der Geometrie.
  Aligned-symmetry : Aligned a b c → Aligned c b a
  Aligned-symmetry {a}{b}{c} alig
    with [∃]-intro p ⦃ [∧]-intro bpb cpa ⦄ ← Aligned-intersection{a}{b}{_}{b}{c} alig Aligned-reflexivityᵣ
    with pb ← Aligned-point bpb
    = substitute₃-unary₂(Aligned) pb cpa

  -- Two points are always aligned.
  -- Also called: 3.3 in Metamathematische Methoden in der Geometrie.
  Aligned-reflexivityₗ : Aligned a a b
  Aligned-reflexivityₗ = Aligned-symmetry Aligned-reflexivityᵣ

  -- Also called: 3.4 in Metamathematische Methoden in der Geometrie.
  Aligned-antisymmetryₗ : (Aligned a b c) → (Aligned b a c) → (a ≡ b)
  Aligned-antisymmetryₗ {a}{b}{c} al-abc al-bac
    with [∃]-intro i ⦃ [∧]-intro al-bib al-aia ⦄ ← Aligned-intersection{a}{b}{c} al-abc al-bac
    with ia ← Aligned-point al-aia
    with ib ← Aligned-point al-bib
    = symmetry(_≡_) ia 🝖 ib

  Aligned-antisymmetryᵣ : (Aligned a b c) → (Aligned a c b) → (b ≡ c)
  Aligned-antisymmetryᵣ al-abc al-acb = symmetry(_≡_) (Aligned-antisymmetryₗ (Aligned-symmetry al-abc) (Aligned-symmetry al-acb))

  -- Also called: 3.6(1) in Metamathematische Methoden in der Geometrie.
  Aligned-transitivityᵣ-exchange : (Aligned a b c) → (Aligned a c d) → (Aligned b c d)
  Aligned-transitivityᵣ-exchange abc acd
    with [∃]-intro i ⦃ [∧]-intro bid cic ⦄ ← Aligned-intersection (Aligned-symmetry abc) (Aligned-symmetry acd)
    with ic ← Aligned-point cic
    = substitute₃-unary₂(Aligned) ic bid

  -- Also called: 3.5(1) in Metamathematische Methoden in der Geometrie.
  Aligned-transitivityₗ-exchange : (Aligned a b d) → (Aligned b c d) → (Aligned a b c)
  Aligned-transitivityₗ-exchange abd bcd = Aligned-symmetry (Aligned-transitivityᵣ-exchange (Aligned-symmetry bcd) (Aligned-symmetry abd))

  -- Also called: 3.7(1) in Metamathematische Methoden in der Geometrie.
  Aligned-semitransitivityᵣ : (Aligned a b c) → (Aligned b c d) → (b ≢ c) → (Aligned a c d)
  Aligned-semitransitivityᵣ {a}{b}{c}{d} abc bcd nbc
    with [∃]-intro x ⦃ [∧]-intro acx cxcd ⦄ ← segment-construction{a}{c}{c}{d}
    with bcx ← Aligned-transitivityᵣ-exchange abc acx
    with xd ← segment-construction-uniqueness nbc ([∧]-intro bcx cxcd) ([∧]-intro bcd (reflexivity(Equidistanced)))
    = substitute₃-unary₃(Aligned) xd acx

  -- Also called: 3.5(2) in Metamathematische Methoden in der Geometrie.
  Aligned-transitivityₗ-merge : (Aligned a b d) → (Aligned b c d) → (Aligned a c d)
  Aligned-transitivityₗ-merge {a}{b}{d}{c} abd bcd with excluded-middle(b ≡ₚ c)
  ... | [∨]-introₗ bc  = substitute₃-unary₂(Aligned) bc abd
  ... | [∨]-introᵣ nbc = Aligned-semitransitivityᵣ (Aligned-transitivityₗ-exchange abd bcd) bcd nbc

  -- Also called: 3.6(2) in Metamathematische Methoden in der Geometrie.
  Aligned-transitivityᵣ-merge : (Aligned a b c) → (Aligned a c d) → (Aligned a b d)
  Aligned-transitivityᵣ-merge abc acd = Aligned-symmetry (Aligned-transitivityₗ-merge (Aligned-symmetry acd) (Aligned-symmetry abc))

  -- Also called: 3.7(2) in Metamathematische Methoden in der Geometrie.
  Aligned-semitransitivityₗ : (Aligned a b c) → (Aligned b c d) → (b ≢ c) → (Aligned a b d)
  Aligned-semitransitivityₗ abc bcd nbc = Aligned-symmetry(Aligned-semitransitivityᵣ (Aligned-symmetry bcd) (Aligned-symmetry abc) (nbc ∘ symmetry(_≡ₚ_)))

  Aligned₄-intro-[123,134] : (Aligned a b c) → (Aligned a c d) → (Aligned₄ a b c d)
  Aligned₄-intro-[123,134] abc acd = abc , abd , acd , bcd where
    abd = Aligned-transitivityᵣ-merge    abc acd
    bcd = Aligned-transitivityᵣ-exchange abc acd

  Aligned₄-intro-[124,234] : (Aligned a b d) → (Aligned b c d) → (Aligned₄ a b c d)
  Aligned₄-intro-[124,234] abd bcd = abc , abd , acd , bcd where
    abc = Aligned-transitivityₗ-exchange abd bcd
    acd = Aligned-transitivityₗ-merge    abd bcd

  -- Existence of two distinct points.
  -- Also called: 3.13 in Metamathematische Methoden in der Geometrie.
  lower-dimension₁ : ∃{Obj = Point ⨯ Point}(\{(a , b) → a ≢ b})
  lower-dimension₁
    with [∃]-intro (a , b , _) ⦃ [∧]-intro ([∧]-intro p _) _ ⦄ ← lower-dimension₂
    = [∃]-intro (a , b) ⦃ ab ↦ p(substitute₃-unary₂(Aligned) ab Aligned-reflexivityₗ) ⦄

  -- Also called: 3.14 in Metamathematische Methoden in der Geometrie.
  extension-existence : ∃(e ↦ (Aligned a b e) ∧ (b ≢ e))
  extension-existence{a}{b}
    with [∃]-intro (x , y) ⦃ nab ⦄ ← lower-dimension₁
    with [∃]-intro e ⦃ [∧]-intro abe bexy ⦄ ← segment-construction{a}{b}{x}{y}
    = [∃]-intro e ⦃ [∧]-intro abe (nab ∘ (be ↦ Equidistanced-point(symmetry(Equidistanced) (substitute₂ₗ(Equidistanced) ([∧]-intro be (reflexivity(_≡ₚ_))) bexy)))) ⦄

  -- Also called: 3.17 in Metamathematische Methoden in der Geometrie.
  triangle-edge-lines-intersection : (Aligned a₁ b₁ c) → (Aligned a₂ b₂ c) → (Aligned a₁ p a₂) → ∃(i ↦ (Aligned p i c) ∧ (Aligned b₁ i b₂))
  triangle-edge-lines-intersection a₁b₁c a₂b₂c a₁pa₂
    with [∃]-intro j ⦃ [∧]-intro pjc b₂ja₁ ⦄ ← Aligned-intersection a₁pa₂ (Aligned-symmetry a₂b₂c)
    with [∃]-intro i ⦃ [∧]-intro b₁ib₂ jic ⦄ ← Aligned-intersection (Aligned-symmetry a₁b₁c) (b₂ja₁)
    = [∃]-intro i ⦃ [∧]-intro (Aligned-transitivityₗ-merge pjc jic) b₁ib₂ ⦄

  -- Also called: 4.6 in Metamathematische Methoden in der Geometrie.
  postulate equidistanced-points-are-aligned : Equidistanced₃(a₁ , b₁ , c₁)(a₂ , b₂ , c₂) → (Aligned a₁ b₁ c₁) → (Aligned a₂ b₂ c₂)

  -- Also called: 5.1 in Metamathematische Methoden in der Geometrie.
  postulate Aligned-order-cases₃-skip₂ : (a ≢ b) → (Aligned a b c₁) → (Aligned a b c₂) → ((Aligned a c₁ c₂) ∨ (Aligned a c₂ c₁))

  -- Also called: 5.2 in Metamathematische Methoden in der Geometrie.
  postulate Aligned-order-cases₃-skip₁ : (a ≢ b) → (Aligned a b c₁) → (Aligned a b c₂) → ((Aligned b c₁ c₂) ∨ (Aligned b c₂ c₁))

  -- Also called: 5.3 in Metamathematische Methoden in der Geometrie.
  postulate Aligned-order-cases₂-skip₃ : (Aligned a b₁ c) → (Aligned a b₂ c) → ((Aligned a b₁ b₂) ∨ (Aligned a b₂ b₁))

  -- The distance between the first pair of points are lesser or equal to the distance between the second pair of points.
  -- The definition states that there should exist a point bₘ such that a (b₁,bₘ) is a subline of (b₁,b₂) and such that the subline is of the same length as (a₁,a₂).
  -- Also called: 5.4 in Metamathematische Methoden in der Geometrie.
  LeDistanced : (Point ⨯ Point) → (Point ⨯ Point) → Stmt
  LeDistanced(a₁ , a₂)(b₁ , b₂) = ∃(bₘ ↦ (Aligned b₁ bₘ b₂) ∧ Equidistanced(a₁ , a₂)(b₁ , bₘ))

  -- Also called: 5.4 in Metamathematische Methoden in der Geometrie.
  GeDistanced : (Point ⨯ Point) → (Point ⨯ Point) → Stmt
  GeDistanced = swap LeDistanced

  -- Also called: 5.5 in Metamathematische Methoden in der Geometrie.
  postulate LeDistanced-alternative : LeDistanced(a₁ , a₂)(b₁ , b₂) ↔ ∃(aₒ ↦ (Aligned a₁ a₂ aₒ) ∧ Equidistanced(a₁ , aₒ)(b₁ , b₂))

  -- Also called: 5.7 in Metamathematische Methoden in der Geometrie.
  instance
    postulate LeDistanced-reflexivity : Reflexivity(LeDistanced)

  -- Also called: 5.8 in Metamathematische Methoden in der Geometrie.
  instance
    postulate LeDistanced-transitivity : Transitivity(LeDistanced)

  -- Also called: 5.9 in Metamathematische Methoden in der Geometrie.
  instance
    postulate LeDistanced-antisymmetry : Antisymmetry(LeDistanced)(Equidistanced)

  -- Also called: 5.10 in Metamathematische Methoden in der Geometrie.
  instance
    postulate LeDistanced-converseTotal : ConverseTotal(LeDistanced)

  -- Also called: 5.11 in Metamathematische Methoden in der Geometrie.
  instance
    postulate LeDistanced-minimal : Weak.Properties.LE.Minimum(LeDistanced)(p , p)

  -- Also called: 5.12 in Metamathematische Methoden in der Geometrie.
  postulate Collinear-aligned-ledistanced-equivalence : (Collinear a b c) → ((Aligned a b c) ↔ (LeDistanced(a , b)(a , c) ∧ LeDistanced(b , c)(a , c)))

  -- Also called: 5.14 in Metamathematische Methoden in der Geometrie.
  LtDistanced : (Point ⨯ Point) → (Point ⨯ Point) → Stmt
  LtDistanced(a₁ , a₂)(b₁ , b₂) = LeDistanced(a₁ , a₂)(b₁ , b₂) ∧ (¬ Equidistanced(a₁ , a₂)(b₁ , b₂))

  -- Also called: 5.14 in Metamathematische Methoden in der Geometrie.
  GtDistanced : (Point ⨯ Point) → (Point ⨯ Point) → Stmt
  GtDistanced = swap GeDistanced

  aligned-equidistanced-equality : (Aligned a b₁ b₂) → Equidistanced(a , b₁)(a , b₂) → (b₁ ≡ₚ b₂)
  aligned-equidistanced-equality ab₁b₂ ab₁ab₂ = {!!}

  aligned-equidistanced-last-equality : (a ≢ b) → (Aligned a b c₁) → (Aligned a b c₂) → Equidistanced(b , c₁)(b , c₂) → (c₁ ≡ c₂)
  aligned-equidistanced-last-equality nab abc₁ abc₂ bc₁bc₂ = {!Aligned-order-cases₃-skip₁ nab abc₁ abc₂!}

  Aligned-classical : Classical₃(Aligned)
  Classical.excluded-middle (Aligned-classical {a} {b} {c})
    with [∃]-intro d ⦃ [∧]-intro abd bdbc ⦄ ← segment-construction{a}{b}{b}{c}
    with excluded-middle(a ≡ₚ b) | excluded-middle(c ≡ₚ d)
  ... | _              | [∨]-introₗ cd  = [∨]-introₗ (substitute₃-unary₃(Aligned) (symmetry(_≡ₚ_) cd) abd)
  ... | [∨]-introₗ ab  | [∨]-introᵣ ncd = [∨]-introₗ (substitute₃-unary₂(Aligned) ab Aligned-reflexivityₗ)
  ... | [∨]-introᵣ nab | [∨]-introᵣ ncd = [∨]-introᵣ (abc ↦ ncd(aligned-equidistanced-last-equality nab abc abd (symmetry(Equidistanced) bdbc)))

  {-
  -- Also called: 6.14 in Metamathematische Methoden in der Geometrie.
  lineSet : (a : Point) → (b : Point) → ⦃ distinct : (a ≢ b) ⦄ → PredSet(Point)
  lineSet a b ∋ p = Collinear a p b
  PredSet.preserve-equiv (lineSet a b) = {!TrinaryRelator.unary₂(Collinear)!} -- TODO-}

  -- Example:
  --         (c)
  --       /     \
  --    (m₁)\   /(m₂)
  --    /   _(i)_   \
  --  (a)__/     \__(b)
  -- Also called: Outer Pasch.
  postulate Aligned-outer-intersection : (Aligned a i m₂) → (Aligned b m₂ c) → ∃(m₁ ↦ (Aligned a m₁ c) ∧ (Aligned b i m₁))
  {-Aligned-outer-intersection {a}{i}{m₂}{b}{c} aim2 bm2c with excluded-middle(Collinear b i m₂) ⦃ classical ⦄
  Aligned-outer-intersection {a}{i}{m₂}{b}{c} aim2 bm2c | [∨]-introₗ coll-bim2 with excluded-middle(Aligned b i m₂) ⦃ classical ⦄
  ... | [∨]-introₗ al-bim2 = [∃]-intro c ⦃ [∧]-intro {!!} ([∨]-elim ([∨]-elim (al-bim2 ↦ {!!}) (al-im2b ↦ {!!})) (al-m2bi ↦ {!!}) coll-bim2) ⦄
  ... | [∨]-introᵣ x = {!!}
  Aligned-outer-intersection {a}{i}{m₂}{b}{c} aim2 bm2c | [∨]-introᵣ x = {!!}-}
    {-with [∃]-intro ii ⦃ p ⦄ ← Aligned-intersection {!!} {!!}
    = {!!}-}

{-

  -- A point on the bisecting ray of the given line.
  -- Example:
  --        ⋮
  --        |
  --       (p)
  --      / | \
  --     /  |  \
  --   (a)-----(b)
  --        |
  --        ⋮
  BisectingRayPoint : Point → Point → Point → Stmt
  BisectingRayPoint a p b = Equidistanced(a , p)(b , p)

  -- The points are all aligned in a line with the second point being in the center of the line constructed from the other points.
  -- Example:
  --   (a)---(m)---(b)
  -- `m` is the centerpoint (in the middle) of `a` and `b`.
  CenterAligned : Point → Point → Point → Stmt
  CenterAligned a m b = (BisectingRayPoint a m b) ∧ (Aligned a m b)

  -- The points form a perpendicular triangle with b being the corner where the perpendicular angle is residing.
  -- Example:
  --       (a)
  --      / | \
  --     /  |  \
  --    /   |   \
  --  (c)--(b)--(cₘ)
  PerpendicularCorner : Point → Point → Point → Stmt
  PerpendicularCorner a b c = ∃(cₘ ↦ (CenterAligned c b cₘ) ∧ (BisectingRayPoint c a cₘ))

  -- The distance between the first pair of points are lesser or equal to the distance between the second pair of points.
  -- This is defined by considering points on a bisecting ray in the center of each of the two lines constructed from the pairs of points. If there is a function that maps points on the second bisecting ray to the first bisecting ray such that this mapping preserves the distance to one of the endpoints of its corresponding line, then the distance between the first pair is lesser than the second.
  -- Example:
  --    (bBisect)
  --       /|\
  --      / | \
  --     /  |  \
  --  (b₁)=====(b₂)

  --   (aBisect)
  --      /|\
  --     / | \
  --    |  |  |
  --  (a₁)===(a₂)
  --
  --   Here, b₁ and b₂ are equally distanced to bBisect.
  --   The definition then states that there exists a similiar construction aBisect on a₁ and a₂, and it does.
  --   And this second construction (aBisect) should have the same distance to its endpoints (for example a₂) as the first (bBisect) have (for example b₂), which it does.
  --   Now, in the extreme case where the distance between bBisect and the endpoints are shrunk, bBisect would collapse into being a center point of the line (b₁,b₂), but because the distance between a₁ and a₂ is smaller, aBisect will still be outside of the line (a₁,a₂). Though, it still exists.
  --   This would not be the case if the relation was reversed.
  LeDistanced2 : (Point ⨯ Point) → (Point ⨯ Point) → Stmt
  LeDistanced2(a₁ , a₂)(b₁ , b₂) =
    ∀{bBisect} → (BisectingRayPoint b₁ bBisect b₂) →
    ∃(aBisect  ↦ (BisectingRayPoint a₁ aBisect a₂) ∧ Equidistanced(a₂ , aBisect)(b₂ , bBisect))

  -- Aligned-Distanced-equivalence : (Aligned a b c) ↔ (∀{d} → LeDistanced2(a , d)(a , b) → LeDistanced2(c , d)(b , c) → (b ≡ d))

  -- Note: The only purpose of this definition is so that instance search works (because it do not work on functions, and negation is defined as a function).
  record DistinctPoints (a b : Point) : Type{ℓₚₑ} where
    constructor intro
    field proof : (a ≢ b)

  -- A line segment is a geometric figure defined by two distinct points
  -- The interpretation is that these two points connect each other, and the set of points of the figure are the points between these two points.
  record LineSegment : Type{ℓₚ Lvl.⊔ ℓₚₑ} where
    constructor lineSegment
    field
      from : Point
      to : Point
      ⦃ distinct ⦄ : DistinctPoints from to

    -- A point on the line segment.
    point : Point
    point = [∃]-witness (Aligned-intersection {to}{from} {from} {to}{from} Aligned-reflexivityᵣ Aligned-reflexivityᵣ)

    -- The line segment flipped.
    flip : LineSegment
    flip = record{from = to ; to = from ; distinct = intro(DistinctPoints.proof distinct ∘ symmetry(_≡_))}

    copyTo : Point → LineSegment
    copyTo base = {!!}

    -- TODO: This is apparently difficult to construct
    center : Point
    -- center = {!!}

    -- The bisector (TODO: which one?) line of this line segment. (TODO: Too unspecific. Where does it start and end?)
    bisector : LineSegment
    -- bisector = {!!}
  private variable l l₁ l₂ l₃ : LineSegment

  -- Point inclusion in line segment (a point is in a line segment).
  _∈₂_ : Point → LineSegment → Type
  p ∈₂ lineSegment a b = Aligned a p b

  -- Line segment congruence (two line segments are of equal length)
  _⎶_ : LineSegment → LineSegment → Type
  lineSegment a₁ a₂ ⎶ lineSegment b₁ b₂ = Equidistanced(a₁ , a₂)(b₁ , b₂)

  Perpendicular : LineSegment → LineSegment → Stmt
  Perpendicular(lineSegment a₁ a₂)(lineSegment b₁ b₂) = ∃(c ↦ (Collinear a₁ a₂ c) ∧ (Collinear b₁ b₂ c) ∧ (PerpendicularCorner a₂ c b₂))

  Parallel : LineSegment → LineSegment → Stmt
  Parallel a b = Perpendicular a (LineSegment.bisector b)

  point-in-lineSegment : LineSegment.point(l) ∈₂ l
  point-in-lineSegment{l} = [∧]-elimₗ([∃]-proof (Aligned-intersection Aligned-reflexivityᵣ Aligned-reflexivityᵣ))

  -- A triangle is a geometric figure defined by three unaligned points.
  -- The interpretation is that these three points connect each other, forming three line segments, and the set of points of the figure are the points inside the line segments.
  record Triangle : Type{ℓₚ Lvl.⊔ ℓₗᵢₗ} where
    constructor triangle
    field
      point₁ : Point
      point₂ : Point
      point₃ : Point
      ⦃ distinct₁ ⦄ : ¬ Aligned point₁ point₂ point₃
      ⦃ distinct₂ ⦄ : ¬ Aligned point₂ point₃ point₁
      ⦃ distinct₃ ⦄ : ¬ Aligned point₃ point₁ point₂

    side₁₂ : LineSegment
    side₁₂ = line point₁ point₂ ⦃ intro(contrapositiveᵣ (p1p2 ↦ substitute₃-unary₁(Aligned) (symmetry(_≡_) p1p2) Aligned-reflexivityₗ) distinct₁) ⦄

    side₂₃ : LineSegment
    side₂₃ = line point₂ point₃ ⦃ intro(contrapositiveᵣ (p2p3 ↦ substitute₃-unary₁(Aligned) (symmetry(_≡_) p2p3) Aligned-reflexivityₗ) distinct₂) ⦄

    side₃₁ : LineSegment
    side₃₁ = line point₃ point₁ ⦃ intro(contrapositiveᵣ (p3p1 ↦ substitute₃-unary₁(Aligned) (symmetry(_≡_) p3p1) Aligned-reflexivityₗ) distinct₃) ⦄
  private variable tri tri₁ tri₂ : Triangle

  -- A triangle exists.
  -- This comes directly from an axiom.
  Triangle-existence : Triangle
  Triangle-existence
    with [∃]-intro(x , y , z) ⦃ [∧]-intro ([∧]-intro p q) r ⦄ ← lower-dimension
    = triangle x y z ⦃ p ⦄ ⦃ q ⦄ ⦃ r ⦄

  Aligned-four : (Aligned a b c) → (Aligned p₁ b c) → (Aligned a b p₂) → (Aligned p₁ b p₂)
  Aligned-four abc p₁bc abp₂
    with [∃]-intro d ⦃ [∧]-intro bdp₂ bdc ⦄ ← Aligned-intersection (Aligned-symmetry abc) (Aligned-symmetry abp₂)
    with [∃]-intro e ⦃ [∧]-intro bep₁ bea ⦄ ← Aligned-intersection abc p₁bc
    = {!Aligned-transitivityᵣ abp₂ p₁bc!}
  Aligned-alternative-start : (Aligned a₁ b c)→ (Aligned a₂ b c) → ((Aligned a₁ a₂ b) ∨ (Aligned a₂ a₁ b))

  -- Note: The difference between segment-construction and this is that this is not extending the line (a₁,b₁). segment-equidistanced-copy constructs a new line which is of the same length as (a₂,b₂) but starting from a₁ and is in the direction of p.
  -- TODO: A proof idea is to use center-of-3 and eliminate the last case. For the different cases, one uses different segment-constructions as usual
  segment-equidistanced-copy : ∃(p ↦ ((Aligned a₁ b₁ p) ∨ (Aligned a₁ p b₁)) ∧ Equidistanced(a₁ , p)(a₂ , b₂))
  segment-equidistanced-copy {a₁}{b₁} {a₂}{b₂}
    with [∃]-intro ext ⦃ [∧]-intro al-b₁a₁ext d-a₁ext-a₂b₂ ⦄ ← segment-construction{b₁}{a₁} {a₂}{b₂}
    with [∃]-intro p   ⦃ [∧]-intro al-exta₁p  d-a₁p-exta₁  ⦄ ← segment-construction{ext}{a₁} {ext}{a₁}
    with center-of-3 {a₁}{b₁}{p}
  ... | [∨]-introₗ ([∨]-introₗ ([∨]-introₗ al-a₁b₁p)) = [∃]-intro p ⦃ [∧]-intro ([∨]-introₗ al-a₁b₁p) (d-a₁p-exta₁ 🝖 Equidistanced-flipped 🝖 d-a₁ext-a₂b₂) ⦄
  ... | [∨]-introₗ ([∨]-introₗ ([∨]-introᵣ al-b₁pa₁)) = [∃]-intro p ⦃ [∧]-intro ([∨]-introᵣ (Aligned-symmetry al-b₁pa₁)) (d-a₁p-exta₁ 🝖 Equidistanced-flipped 🝖 d-a₁ext-a₂b₂) ⦄
  ... | [∨]-introₗ ([∨]-introᵣ             al-pa₁b₁)  = [∃]-intro p ⦃ [∧]-intro ([∨]-introᵣ {!!}) (d-a₁p-exta₁ 🝖 Equidistanced-flipped 🝖 d-a₁ext-a₂b₂) ⦄ -- TODO: Use Aligned-four to prove (a₁ ≡ ext), which implies (a₁ ≡ p), so therefore ( Aligned a₁ a₁ b₁) by substitution. Note that this is the case when (a₂ ≡ b₂), but it is not used in the proof.
  ... | [∨]-introᵣ x = {!!} -- TODO: x essentially states that a₁ b₁ p is not in a line, which can be proven that they are like in the cases above by Aligned-alternative-start

  -- A circle is a geometric figure defined by two distinct points.
  -- The interpretation is that the first point is the center point, and the second point lies on the arc of the circle.
  -- The distance between the points is the radius of the circle, and all points within the radius from the center point defines the set of points of the circle.
  record Circle : Type{ℓₚ Lvl.⊔ ℓₚₑ} where
    constructor circle
    field
      center : Point
      outer : Point
      ⦃ distinct ⦄ : DistinctPoints center outer

    -- A line from the center point to the arc.
    radiusLineSegment : LineSegment
    radiusLineSegment = lineSegment center outer

    {- TODO
    -- A line from the center point to the arc in the direction of the given point.
    radiusLineSegmentTowards : Point → LineSegment
    radiusLineSegmentTowards p
      with [∃]-intro q ⦃ [∧]-intro cpq pqco ⦄ ← segment-construction{center}{p} {center}{outer}
      = lineSegment center q ⦃ intro(cq ↦ (
        • (
          • center ≡ q                          :-[ cq ]
          • Aligned center p q                  :-[ cpq ]
          ⇒₂-[ substitute₃-unary₁(Aligned) ]
          Aligned q p q                         ⇒-[ Aligned-point ]
          p ≡ q                                 ⇒-[ pq ↦ [∧]-intro pq (reflexivity(_≡_)) ]
          (p ≡ q) ∧ (q ≡ q)                     ⇒-end
        )
        • Equidistanced(p , q) (center , outer) :-[ pqco ]
        ⇒₂-[ substitute₂ₗ(Equidistanced) ]
        Equidistanced(q , q) (center , outer)   ⇒-[ symmetry(Equidistanced) ]
        Equidistanced(center , outer) (q , q)   ⇒-[ Equidistanced-point ]
        center ≡ outer                          ⇒-[ DistinctPoints.proof distinct ]
        ⊥                                       ⇒-end
      )) ⦄

    -- TODO: I am confused. Is the point (LineSegment.to(radiusLineTowards p)) always further away than p?
    radiusLineTowards-aligned : Aligned center p (Line.to(radiusLineSegmentTowards p))
    radiusLineTowards-aligned{p}
      with [∃]-intro q ⦃ [∧]-intro cpq pqco ⦄ ← segment-construction{center}{p} {center}{outer}
      = cpq

    radiusLineSegmentTowards-radius : Equidistanced(center , LineSegment.to(radiusLineSegmentTowards p)) (center , outer)
    radiusLineSegmentTowards-radius{p}
      with [∃]-intro q ⦃ [∧]-intro cpq pqco ⦄ ← segment-construction{center}{p} {center}{outer}
      = {!pqco!} -- TODO: pqco is actually stating that (p,q) and (center,outer) is equally distanced, which is not what we want, so radiusLineTowards should be modified to use segment-construction-alt
    -}

    -- TODO: Two circles' intersection points are either 0, 1, 2 or they are the same circle.
    -- intersection : ∀{C₁ C₂} → (∀{p} → ¬(p ∈ₒ C₁) ∧ ¬(p ∈ₒ C₂)) ∨ ∃!(p ↦ (p ∈ₒ C₁) ∧ (p ∈ₒ C₂)) ∨ ∃(p₁ ↦ ∃(p₂ ↦ (p ∈ₒ C₁) ∧ (p ∈ₒ C₂))) ∨ (C₁ ≡ C₂)

  -- Point inclusion in circle (a point is in a circle).
  _∈ₒ_ : Point → Circle → Type
  p ∈ₒ circle c o = LeDistanced(c , p)(c , o)
  -- TODO: Is this equivalent? ∃(op ↦ Equidistanced(c , o)(c , op) ∧ (Aligned c p op)) It extends the line (c,p) instead of shrinking the line (c,o)
-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Structures.Everything where

open import Cubical.Structures.Pointed public
open import Cubical.Structures.InftyMagma public
open import Cubical.Structures.Monoid public
open import Cubical.Structures.Queue public

open import Cubical.Structures.TypeEqvTo public

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
module PLRTree.Heap {A : Set}(_≤_ : A → A → Set) where

open import PLRTree {A}

data _≤*_ : A → PLRTree → Set where
  lf≤* : (x : A)
                   → x ≤* leaf
  nd≤* : {t : Tag}{x y : A}{l r : PLRTree}
                   → x ≤ y
                   → x ≤* l
                   → x ≤* r
                   → x ≤* node t y l r

data Heap : PLRTree → Set where
  leaf : Heap leaf
  node : {t : Tag}{x : A}{l r : PLRTree}
                   → x ≤* l
                   → x ≤* r
                   → Heap l
                   → Heap r
                   → Heap (node t x l r)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-# OPTIONS --safe #-}
module Cubical.HITs.S2.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Pointed

data S² : Type₀ where
  base : S²
  surf : PathP (λ i → base ≡ base) refl refl

S²∙ : Pointed ℓ-zero
S²∙ = S² , base

S²ToSetElim : ∀ {ℓ} {A : S² → Type ℓ}
           → ((x : S²) → isSet (A x))
           → A base
           → (x : S²) → A x
S²ToSetElim set b base = b
S²ToSetElim set b (surf i j) =
  isOfHLevel→isOfHLevelDep 2 set b b {a0 = refl} {a1 = refl} refl refl surf i j

-- Wedge connectivity lemmas for S² (binary maps 2-groupoids)
wedgeconFunS² : ∀ {ℓ} {P : S² → S² → Type ℓ}
         → ((x y : _) → isOfHLevel 4 (P x y))
         → (l : ((x : S²) → P x base))
         → (r : (x : S²) → P base x)
         → l base ≡ r base
         → (x y : _) → P x y
wedgeconFunS² {P = P} hlev l r p base y = r y
wedgeconFunS² {P = P} hlev l r p (surf i i₁) y = help y i i₁
  where
  help : (y : S²) → SquareP (λ i j → P (surf i j) y)
                     (λ _ → r y) (λ _ → r y)
                     (λ _ → r y) λ _ → r y
  help =
    S²ToSetElim (λ _ → isOfHLevelPathP' 2 (isOfHLevelPathP' 3 (hlev _ _) _ _) _ _)
               λ w j → hcomp (λ k → λ { (j = i0) → p k
                                        ; (j = i1) → p k
                                        ; (w = i0) → p k
                                        ; (w = i1) → p k})
                              (l (surf w j))

wedgeconFunS²Id : ∀ {ℓ} {P : S² → S² → Type ℓ}
         → (h : ((x y : _) → isOfHLevel 4 (P x y)))
         → (l : ((x : S²) → P x base))
         → (r : (x : S²) → P base x)
         → (p : l base ≡ r base)
         → (x : S²) → wedgeconFunS² h l r p x base ≡ l x
wedgeconFunS²Id h l r p base = sym p
wedgeconFunS²Id h l r p (surf i j) k =
  hcomp (λ w → λ {(i = i0) → p (~ k ∧ w)
                 ; (i = i1) → p (~ k ∧ w)
                 ; (j = i0) → p (~ k ∧ w)
                 ; (j = i1) → p (~ k ∧ w)
                 ; (k = i1) → l (surf i j)})
        (l (surf i j))

max_stars_repo_name: FernandoLarrain/cubical


text:
{-# OPTIONS --without-K --safe #-}
module PiFracDynDef where
open import Data.Bool
open import Data.Empty
open import Data.Unit
open import Data.Nat
open import Data.Nat.Properties
open import Data.Sum
open import Data.Product
open import Data.Maybe
open import Function
open import Relation.Binary.PropositionalEquality
  renaming ([_] to R[_])
open import Relation.Binary.Core
open import Relation.Nullary

infix  70 _×ᵤ_
infix  60 _+ᵤ_
infix  40 _↔_
infixr 50 _⊚_

data ◯ : Set where
  ○ : ◯

-- Pi

mutual
  data 𝕌 : Set where
    𝟘 : 𝕌
    𝟙 : 𝕌
    _+ᵤ_ : 𝕌 → 𝕌 → 𝕌
    _×ᵤ_ : 𝕌 → 𝕌 → 𝕌
    𝟙/_ : 𝕌 → 𝕌

  ⟦_⟧ : 𝕌 → Set
  ⟦ 𝟘 ⟧ = ⊥
  ⟦ 𝟙 ⟧ = ⊤
  ⟦ t₁ +ᵤ t₂ ⟧ = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧
  ⟦ t₁ ×ᵤ t₂ ⟧ = ⟦ t₁ ⟧ × ⟦ t₂ ⟧
  ⟦ 𝟙/ t ⟧ = ◯

  data _↔_ : 𝕌 → 𝕌 → Set where
    unite₊l : {t : 𝕌} → 𝟘 +ᵤ t ↔ t
    uniti₊l : {t : 𝕌} → t ↔ 𝟘 +ᵤ t
    unite₊r : {t : 𝕌} → t +ᵤ 𝟘 ↔ t
    uniti₊r : {t : 𝕌} → t ↔ t +ᵤ 𝟘
    swap₊   : {t₁ t₂ : 𝕌} → t₁ +ᵤ t₂ ↔ t₂ +ᵤ t₁
    assocl₊ : {t₁ t₂ t₃ : 𝕌} → t₁ +ᵤ (t₂ +ᵤ t₃) ↔ (t₁ +ᵤ t₂) +ᵤ t₃
    assocr₊ : {t₁ t₂ t₃ : 𝕌} → (t₁ +ᵤ t₂) +ᵤ t₃ ↔ t₁ +ᵤ (t₂ +ᵤ t₃)
    unite⋆l : {t : 𝕌} → 𝟙 ×ᵤ t ↔ t
    uniti⋆l : {t : 𝕌} → t ↔ 𝟙 ×ᵤ t
    unite⋆r : {t : 𝕌} → t ×ᵤ 𝟙 ↔ t
    uniti⋆r : {t : 𝕌} → t ↔ t ×ᵤ 𝟙
    swap⋆   : {t₁ t₂ : 𝕌} → t₁ ×ᵤ t₂ ↔ t₂ ×ᵤ t₁
    assocl⋆ : {t₁ t₂ t₃ : 𝕌} → t₁ ×ᵤ (t₂ ×ᵤ t₃) ↔ (t₁ ×ᵤ t₂) ×ᵤ t₃
    assocr⋆ : {t₁ t₂ t₃ : 𝕌} → (t₁ ×ᵤ t₂) ×ᵤ t₃ ↔ t₁ ×ᵤ (t₂ ×ᵤ t₃)
    absorbr : {t : 𝕌} → 𝟘 ×ᵤ t ↔ 𝟘
    absorbl : {t : 𝕌} → t ×ᵤ 𝟘 ↔ 𝟘
    factorzr : {t : 𝕌} → 𝟘 ↔ t ×ᵤ 𝟘
    factorzl : {t : 𝕌} → 𝟘 ↔ 𝟘 ×ᵤ t
    dist    : {t₁ t₂ t₃ : 𝕌} → (t₁ +ᵤ t₂) ×ᵤ t₃ ↔ (t₁ ×ᵤ t₃) +ᵤ (t₂ ×ᵤ t₃)
    factor  : {t₁ t₂ t₃ : 𝕌} → (t₁ ×ᵤ t₃) +ᵤ (t₂ ×ᵤ t₃) ↔ (t₁ +ᵤ t₂) ×ᵤ t₃
    distl   : {t₁ t₂ t₃ : 𝕌} → t₁ ×ᵤ (t₂ +ᵤ t₃) ↔ (t₁ ×ᵤ t₂) +ᵤ (t₁ ×ᵤ t₃)
    factorl : {t₁ t₂ t₃ : 𝕌 } → (t₁ ×ᵤ t₂) +ᵤ (t₁ ×ᵤ t₃) ↔ t₁ ×ᵤ (t₂ +ᵤ t₃)
    id↔     : {t : 𝕌} → t ↔ t
    _⊚_     : {t₁ t₂ t₃ : 𝕌} → (t₁ ↔ t₂) → (t₂ ↔ t₃) → (t₁ ↔ t₃)
    _⊕_     : {t₁ t₂ t₃ t₄ : 𝕌} → (t₁ ↔ t₃) → (t₂ ↔ t₄) → (t₁ +ᵤ t₂ ↔ t₃ +ᵤ t₄)
    _⊗_     : {t₁ t₂ t₃ t₄ : 𝕌} → (t₁ ↔ t₃) → (t₂ ↔ t₄) → (t₁ ×ᵤ t₂ ↔ t₃ ×ᵤ t₄)
    η : {t : 𝕌} {t≠0 : ¬ card t ≡ 0} → 𝟙 ↔ t ×ᵤ (𝟙/ t)
    ε : {t : 𝕌} {t≠0 : ¬ card t ≡ 0} → t ×ᵤ (𝟙/ t) ↔ 𝟙

-- Number of points in type
  card : (t : 𝕌) → ℕ
  card 𝟘 = 0
  card 𝟙 = 1
  card (t₁ +ᵤ t₂) = card t₁ + card t₂
  card (t₁ ×ᵤ t₂) = card t₁ * card t₂
  card (𝟙/ t) = 1

-- If number of points is zero then it is impossible to find a value
-- of the type
0empty : {t : 𝕌} → card t ≡ 0 → (v : ⟦ t ⟧) → ⊥
0empty {𝟘} _ ()
0empty {𝟙} () tt
0empty {t₁ +ᵤ t₂} s (inj₁ v₁)
  with card t₁ | card t₂ | inspect card t₁
0empty {t₁ +ᵤ t₂} refl (inj₁ v₁) | 0 | 0 | R[ s₁ ] =
  0empty {t₁} s₁ v₁
0empty {t₁ +ᵤ t₂} s (inj₂ v₂)
  with card t₁ | card t₂ | inspect card t₂
0empty {t₁ +ᵤ t₂} refl (inj₂ v₂) | ℕ.zero | ℕ.zero | R[ s₂ ] =
  0empty {t₂} s₂ v₂
0empty {t₁ ×ᵤ t₂} s (v₁ , v₂)
  with card t₁ | card t₂ | inspect card t₁ | inspect card t₂
0empty {t₁ ×ᵤ t₂} refl (v₁ , v₂) | ℕ.zero | _ | R[ s₁ ] | _ =
  0empty {t₁} s₁ v₁
0empty {t₁ ×ᵤ t₂} s (v₁ , v₂) | ℕ.suc n₁ | ℕ.zero | R[ s₁ ] | R[ s₂ ] =
  0empty {t₂} s₂ v₂
0empty {𝟙/ t} () f

default : (t : 𝕌) → {t≠0 : ¬ card t ≡ 0} → ⟦ t ⟧
default 𝟘 {t≠0} = ⊥-elim (t≠0 refl)
default 𝟙 = tt
default (t₁ +ᵤ t₂) {p≠0} with card t₁ | card t₂ | inspect card t₁ | inspect card t₂
... | 0 | 0 | R[ s₁ ] | R[ s₂ ] = ⊥-elim (p≠0 refl)
... | 0 | suc n | R[ s₁ ] | R[ s₂ ] =
  inj₂ (default t₂ {λ t2≡0 → ⊥-elim (p≠0 (trans (sym s₂) t2≡0))})
... | suc m | 0 | R[ s₁ ] | R[ s₂ ] =
  inj₁ (default t₁ {λ t1≡0 →
    ⊥-elim (p≠0 ((trans (sym (trans s₁ (sym (+-identityʳ (suc m))))) t1≡0)))})
... | suc m | suc n | R[ s₁ ] | R[ s₂ ] =
  inj₁ (default t₁ {λ t1≡0 → ⊥-elim (1+n≢0 (trans (sym s₁) t1≡0))})
default (t₁ ×ᵤ t₂) {p≠0} with card t₁ | card t₂ | inspect card t₁ | inspect card t₂
... | 0 | 0 | R[ s₁ ] | R[ s₂ ] = ⊥-elim (p≠0 refl)
... | 0 | suc n | R[ s₁ ] | R[ s₂ ] = ⊥-elim (p≠0 refl)
... | suc m | 0 | R[ s₁ ] | R[ s₂ ] = ⊥-elim (p≠0 (*-zeroʳ (suc m)))
... | suc m | suc n | R[ s₁ ] | R[ s₂ ] =
  default t₁ {λ t1≡0 → ⊥-elim (1+n≢0 (trans (sym s₁) t1≡0))},
  default t₂ {λ t2≡0 → ⊥-elim (1+n≢0 (trans (sym s₂) t2≡0))}
default (𝟙/ t) = ○

𝕌dec : (t : 𝕌) → Decidable (_≡_ {A = ⟦ t ⟧})
𝕌dec 𝟘 ()
𝕌dec 𝟙 tt tt = yes refl
𝕌dec (t₁ +ᵤ t₂) (inj₁ x) (inj₁ y) with 𝕌dec t₁ x y
𝕌dec (t₁ +ᵤ t₂) (inj₁ x) (inj₁ .x) | yes refl = yes refl
𝕌dec (t₁ +ᵤ t₂) (inj₁ x) (inj₁ y)  | no ¬p = no (λ {refl → ¬p refl})
𝕌dec (t₁ +ᵤ t₂) (inj₁ x) (inj₂ y) = no (λ ())
𝕌dec (t₁ +ᵤ t₂) (inj₂ x) (inj₁ y) = no (λ ())
𝕌dec (t₁ +ᵤ t₂) (inj₂ x) (inj₂ y) with 𝕌dec t₂ x y
𝕌dec (t₁ +ᵤ t₂) (inj₂ x) (inj₂ .x) | yes refl = yes refl
𝕌dec (t₁ +ᵤ t₂) (inj₂ x) (inj₂ y) | no ¬p = no (λ {refl → ¬p refl})
𝕌dec (t₁ ×ᵤ t₂) (x₁ , y₁) (x₂ , y₂) with 𝕌dec t₁ x₁ x₂ | 𝕌dec t₂ y₁ y₂
𝕌dec (t₁ ×ᵤ t₂) (x₁ , y₁) (.x₁ , .y₁) | yes refl | yes refl = yes refl
𝕌dec (t₁ ×ᵤ t₂) (x₁ , y₁) (.x₁ , y₂) | yes refl | no ¬p = no (λ p → ¬p (cong proj₂ p))
𝕌dec (t₁ ×ᵤ t₂) (x₁ , y₁) (x₂ , .y₁) | no ¬p | yes refl = no (λ p → ¬p (cong proj₁ p))
𝕌dec (t₁ ×ᵤ t₂) (x₁ , y₁) (x₂ , y₂) | no ¬p | no ¬p₁ = no (λ p → ¬p (cong proj₁ p))
𝕌dec (𝟙/ t) ○ ○ = yes refl

_≟ᵤ_ : {t : 𝕌} → Decidable (_≡_ {A = ⟦ t ⟧})
_≟ᵤ_ {t} v w = 𝕌dec t v w

interp : {t₁ t₂ : 𝕌} → (t₁ ↔ t₂) → ⟦ t₁ ⟧ → Maybe ⟦ t₂ ⟧
interp unite₊l (inj₁ ())
interp unite₊l (inj₂ v) = just v
interp uniti₊l v = just (inj₂ v)
interp unite₊r (inj₁ v) = just v
interp unite₊r (inj₂ ())
interp uniti₊r v = just (inj₁ v)
interp swap₊ (inj₁ v) = just (inj₂ v)
interp swap₊ (inj₂ v) = just (inj₁ v)
interp assocl₊ (inj₁ v) = just (inj₁ (inj₁ v))
interp assocl₊ (inj₂ (inj₁ v)) = just (inj₁ (inj₂ v))
interp assocl₊ (inj₂ (inj₂ v)) = just (inj₂ v)
interp assocr₊ (inj₁ (inj₁ v)) = just (inj₁ v)
interp assocr₊ (inj₁ (inj₂ v)) = just (inj₂ (inj₁ v))
interp assocr₊ (inj₂ v) = just (inj₂ (inj₂ v))
interp unite⋆l v = just (proj₂ v)
interp uniti⋆l v = just (tt , v)
interp unite⋆r v = just (proj₁ v)
interp uniti⋆r v = just (v , tt)
interp swap⋆ (v₁ , v₂) = just (v₂ , v₁)
interp assocl⋆ (v₁ , v₂ , v₃) = just ((v₁ , v₂) , v₃)
interp assocr⋆ ((v₁ , v₂) , v₃) = just (v₁ , v₂ , v₃)
interp absorbr (() , v)
interp absorbl (v , ())
interp factorzr ()
interp factorzl ()
interp dist (inj₁ v₁ , v₃) = just (inj₁ (v₁ , v₃))
interp dist (inj₂ v₂ , v₃) = just (inj₂ (v₂ , v₃))
interp factor (inj₁ (v₁ , v₃)) = just (inj₁ v₁ , v₃)
interp factor (inj₂ (v₂ , v₃)) = just (inj₂ v₂ , v₃)
interp distl (v₁ , inj₁ v₂) = just (inj₁ (v₁ , v₂))
interp distl (v₁ , inj₂ v₃) = just (inj₂ (v₁ , v₃))
interp factorl (inj₁ (v₁ , v₂)) = just (v₁ , inj₁ v₂)
interp factorl (inj₂ (v₁ , v₃)) = just (v₁ , inj₂ v₃)
interp id↔ v = just v
interp (c₁ ⊚ c₂) v = interp c₁ v >>= interp c₂
interp (c₁ ⊕ c₂) (inj₁ v) = interp c₁ v >>= just ∘ inj₁
interp (c₁ ⊕ c₂) (inj₂ v) = interp c₂ v >>= just ∘ inj₂
interp (c₁ ⊗ c₂) (v₁ , v₂) = interp c₁ v₁ >>= (λ v₁' → interp c₂ v₂ >>= λ v₂' → just (v₁' , v₂'))
interp (η {t} {t≠0}) tt = just (default t {t≠0} , ○)
interp (ε {t} {t≠0}) (v' , ○) with 𝕌dec t (default t {t≠0}) v'
interp (ε {t}) (v' , ○) | yes _ = just tt
interp (ε {t}) (v' , ○) | no  _ = nothing -- if v ≡ v' then tt else throw Error

--- Examples

𝟚 : 𝕌
𝟚 = 𝟙 +ᵤ 𝟙

𝔽 𝕋 : ⟦ 𝟚 ⟧
𝔽 = inj₁ tt
𝕋 = inj₂ tt

xorr xorl : 𝟚 ×ᵤ 𝟚 ↔ 𝟚 ×ᵤ 𝟚
xorr = dist ⊚ (id↔ ⊕ (id↔ ⊗ swap₊)) ⊚ factor
xorl = distl ⊚ (id↔ ⊕ (swap₊ ⊗ id↔)) ⊚ factorl

𝟚≠0 : ¬ (card 𝟚 ≡ 0)
𝟚≠0 ()

η𝟚 : 𝟙 ↔ 𝟚 ×ᵤ (𝟙/ 𝟚)
η𝟚 = η {t≠0 = 𝟚≠0}

ε𝟚 : 𝟚 ×ᵤ (𝟙/ 𝟚) ↔ 𝟙
ε𝟚 = ε {t≠0 = 𝟚≠0}

--   ─────┬────⊕───  ───────
--        |    |   ⨉
--     ┌──⊕────┴───  ───┐
--     └────────────────┘
id' : 𝟚 ↔ 𝟚
id' = uniti⋆r ⊚ (id↔ ⊗ η𝟚) ⊚ assocl⋆ ⊚
      ((xorr ⊚ xorl ⊚ swap⋆) ⊗ id↔) ⊚
      assocr⋆ ⊚ (id↔ ⊗ ε𝟚) ⊚ unite⋆r

ex1 : interp id' 𝕋 ≡ just 𝕋
ex1 = refl

ex2 : interp id' 𝔽 ≡ just 𝔽
ex2 = refl

--     ┌──────  ───────┐
--     └──────╲╱───────┘
--            ╱╲
--     ┌─────    ──────┐
--     └───────────────┘
switch : 𝟙 ↔ 𝟙
switch = uniti⋆r ⊚ (η𝟚 ⊗ η𝟚) ⊚ assocl⋆ ⊚
         (((swap⋆ ⊗ id↔) ⊚ assocr⋆ ⊚
         (id↔ ⊗ swap⋆) ⊚ assocl⋆ ⊚ (swap⋆ ⊗ id↔)) ⊗ id↔) ⊚
         assocr⋆ ⊚ (ε𝟚 ⊗ ε𝟚) ⊚ unite⋆r

bad : 𝟚 ↔ 𝟚
bad = uniti⋆r ⊚ (id↔ ⊗ η𝟚) ⊚ assocl⋆ ⊚
      ((xorr ⊚ swap⋆) ⊗ id↔) ⊚
      assocr⋆ ⊚ (id↔ ⊗ ε𝟚) ⊚ unite⋆r

ex3 : interp bad 𝔽 ≡ just 𝔽
ex3 = refl

ex4 : interp bad 𝕋 ≡ nothing
ex4 = refl

{--
shouldn't_type_check : 𝟙 ↔ 𝟙
shouldn't_type_check = η {v = 𝔽} ⊚ ε {v = 𝕋}

ex5 : interp shouldn't_type_check tt ≡ nothing
ex5 = refl

more : 𝟙 ↔ 𝟙
more = η {v = 𝔽} ⊚ (swap₊ ⊗ id↔) ⊚ ε {v = 𝕋}

ex6 : interp more tt ≡ just tt
ex6 = refl
--}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module Isomorphism where

open import Library

record Iso {a b}(A : Set a)(B : Set b) : Set (a ⊔ b) where
  field fun : A → B
        inv : B → A
        law1 : ∀ b → fun (inv b) ≅ b
        law2 : ∀ a → inv (fun a) ≅ a

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Equivalence

module HoTT.Identity.Product where

open variables
private variable x y : A × B

_=×_ : A × B → A × B → 𝒰 _
x =× y = pr₁ x == pr₁ y × pr₂ x == pr₂ y

-- Theorem 2.6.2
=× : x == y ≃ x =× y
=× {x = _ , _} {_ , _} = let open Iso in iso→eqv λ where
  .f refl → refl , refl
  .g (refl , refl) → refl
  .η refl → refl
  .ε (refl , refl) → refl

module _ {x y : A × B} where
  open Iso (eqv→iso (=× {x = x} {y})) public
    renaming (f to =×-elim ; g to =×-intro ; η to =×-η ; ε to =×-β)

×-pair⁼ = =×-intro

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
module Golden.RedBlack where

open import Prelude hiding (insert)

-- Version of comparison that lets us use instance search for the proof objects.
data Comparison! {a} {A : Set a} (_<_ : A → A → Set a) (x y : A) : Set a where
  less    : {{_ : x < y}} → Comparison! _<_ x y
  equal   : {{_ : x ≡ y}} → Comparison! _<_ x y
  greater : {{_ : y < x}} → Comparison! _<_ x y

compare! : ∀ {a} {A : Set a} {{_ : Ord A}} (x y : A) → Comparison! _<_ x y
compare! x y =
  case compare x y of λ where
    (less    lt) → less    {{lt}}
    (equal   eq) → equal   {{eq}}
    (greater gt) → greater {{gt}}

record Prf (A : Set) : Set where
  constructor !
  field
    {{prf}} : A

data Bound (A : Set) : Set where
  -∞ ∞ : Bound A
  # : A → Bound A

module _ {A : Set} {{_ : Ord A}} where
  LessBound : Bound A → Bound A → Set
  LessBound ∞ _ = ⊥
  LessBound _ ∞ = ⊤
  LessBound _ -∞ = ⊥
  LessBound -∞ _ = ⊤
  LessBound (# x) (# y) = x < y

  instance
    OrdBound : Ord (Bound A)
    OrdBound = defaultOrd compareBound
      where
        compareBound : (a b : Bound A) → Comparison LessBound a b
        compareBound -∞ -∞ = equal refl
        compareBound -∞ ∞ = less _
        compareBound -∞ (# x) = less _
        compareBound ∞ -∞ = greater tt
        compareBound ∞ ∞ = equal refl
        compareBound ∞ (# x) = greater tt
        compareBound (# x) -∞ = greater tt
        compareBound (# x) ∞ = less tt
        compareBound (# x) (# y) with compare x y
        ... | less lt = less lt
        ... | greater gt = greater gt
        compareBound (# x) (# .x) | equal refl = equal refl

Bounds : Set → Set
Bounds A = Bound A × Bound A

Rel : Set → Set₁
Rel A = Bounds A → Set

module _ {A : Set} where
  PrfR : Rel A → Rel A
  PrfR R b = Prf (R b)

  data _∧_ (S T : Rel A) : Rel A where
    pivot : ∀ {l u} p → S (l , # p) → T (# p , u) → (S ∧ T) (l , u)

  pattern -⟨_⟩- p = pivot p ! !
  pattern _⟨_⟩_ l p r = pivot p l r

module _ {A : Set} {{_ : Ord A}} where
  Less : Rel A
  Less = PrfR (uncurry _<_)

  Bounded : Rel A
  Bounded = Less ∧ Less

data Color : Set where
  red black : Color

module _ (A : Set) {{_ : Ord A}} where

  data Tree′ (b : Bounds A) : Nat → Color → Set

  Tree : Nat → Color → Rel A
  Tree n c b = Tree′ b n c

  data Tree′ b where
    leaf′  : Less b → Tree 0 black b
    red   : ∀ {n} → (Tree n black ∧ Tree n black) b → Tree n red b
    black : ∀ {c₁ c₂ n} → (Tree n c₁ ∧ Tree n c₂) b → Tree (suc n) black b

  pattern leaf = leaf′ !

  data PreTree′ (b : Bounds A) (n : Nat) : Color → Set

  PreTree : Nat → Color → Bounds A → Set
  PreTree n c b = PreTree′ b n c

  data PreTree′ b n where
    red         : ∀ {c₁ c₂} → (Tree n c₁ ∧ Tree n c₂) b → PreTree n red b
    maybe-black : ∀ {c} → Tree n c b → PreTree n black b

  pattern _b⟨_⟩_   l x r = black (l ⟨ x ⟩ r)
  pattern _r⟨_⟩_   l x r = red (l ⟨ x ⟩ r)
  pattern _pb⟨_⟩_  l x r = maybe-black (black (l ⟨ x ⟩ r))
  pattern _pbr⟨_⟩_ l x r = maybe-black (red   (l ⟨ x ⟩ r))
  pattern _rbb⟨_⟩_ l x r = red {c₁ = black} {c₂ = black} (l ⟨ x ⟩ r)

module _ {A : Set} {{_ : Ord A}} where

  balance-l : ∀ {b c₁ c₂ n} →
              (PreTree A n c₁ ∧ Tree A n c₂) b →
              PreTree A (suc n) black b
  balance-l (((l₁ r⟨ z ⟩ l₂) r⟨ x ⟩ l₃) ⟨ y ⟩ r) =
    (l₁ b⟨ z ⟩ l₂) pbr⟨ x ⟩ (l₃ b⟨ y ⟩ r)
  balance-l ((l₁ r⟨ z ⟩ (l₂ r⟨ x ⟩ l₃)) ⟨ y ⟩ r) =
    (l₁ b⟨ z ⟩ l₂) pbr⟨ x ⟩ (l₃ b⟨ y ⟩ r)
  balance-l ((l₁ rbb⟨ x ⟩ l₂) ⟨ y ⟩ r) =
    (l₁ r⟨ x ⟩ l₂) pb⟨ y ⟩ r
  balance-l (maybe-black l ⟨ y ⟩ r) = l pb⟨ y ⟩ r

  balance-r : ∀ {b c₁ c₂ n} →
              (Tree A n c₁ ∧ PreTree A n c₂) b →
              PreTree A (suc n) black b
  balance-r (l ⟨ y ⟩ ((r₁ r⟨ z ⟩ r₂) r⟨ x ⟩ r₃)) =
    (l b⟨ y ⟩ r₁) pbr⟨ z ⟩ (r₂ b⟨ x ⟩ r₃)
  balance-r (l ⟨ y ⟩ (r₁ r⟨ x ⟩ (r₂ r⟨ z ⟩ r₃))) =
    (l b⟨ y ⟩ r₁) pbr⟨ x ⟩ (r₂ b⟨ z ⟩ r₃)
  balance-r (l ⟨ y ⟩ (r₁ rbb⟨ x ⟩ r₂)) =
    l pb⟨ y ⟩ (r₁ r⟨ x ⟩ r₂)
  balance-r (l ⟨ y ⟩ maybe-black r) = l pb⟨ y ⟩ r

  ins : ∀ {b c n} → Bounded b → Tree A n c b → PreTree A n c b
  ins -⟨ x ⟩- leaf = leaf pbr⟨ x ⟩ leaf
  ins -⟨ x ⟩- (red (l ⟨ y ⟩ r)) =
    case compare! x y of λ where
      less    → case ins -⟨ x ⟩- l of λ { (maybe-black l′) → l′ r⟨ y ⟩ r }
      greater → case ins -⟨ x ⟩- r of λ { (maybe-black r′) → l r⟨ y ⟩ r′ }
      equal   → l r⟨ y ⟩ r
  ins -⟨ x ⟩- (black (l ⟨ y ⟩ r)) =
    case compare! x y of λ where
      less    → balance-l (ins -⟨ x ⟩- l ⟨ y ⟩ r)
      greater → balance-r (l ⟨ y ⟩ ins -⟨ x ⟩- r)
      equal   → l pb⟨ y ⟩ r

data RedBlackTree (A : Set) {{_ : Ord A}} : Set where
  mkT : ∀ {n} → Tree A n black (-∞ , ∞) → RedBlackTree A

module _ {A : Set} {{_ : Ord A}} where

  insert : A → RedBlackTree A → RedBlackTree A
  insert x (mkT t) with ins -⟨ x ⟩- t
  ... | l pbr⟨ y ⟩ r      = mkT $ l b⟨ y ⟩ r
  ... | l  pb⟨ y ⟩ r      = mkT $ l b⟨ y ⟩ r
  ... | maybe-black leaf = mkT leaf

  fromList : List A → RedBlackTree A
  fromList = foldr insert (mkT leaf)

  toList′ : ∀ {b n c} → Tree′ A b n c → List A → List A
  toList′ (leaf′ _)   xs = xs
  toList′ (l r⟨ x ⟩ r) xs = toList′ l (x ∷ toList′ r xs)
  toList′ (l b⟨ x ⟩ r) xs = toList′ l (x ∷ toList′ r xs)

  toList : RedBlackTree A → List A
  toList (mkT t) = toList′ t []

  treeSort : List A → List A
  treeSort = toList ∘ fromList

-- Example

test : List Nat
test = treeSort $ 5 ∷ 1 ∷ 2 ∷ 10 ∷ 13 ∷ 0 ∷ 141 ∷ 7 ∷ []

hest : String
hest = show test

main : IO Unit
main = putStrLn hest

max_stars_repo_name: agda/agda-ocaml

max_issues_repo_name: agda/agda-ocaml

max_forks_repo_name: agda/agda-ocaml


text:
-- Andreas, 2018-06-19, issue #3130

module Issue3130 where

-- A pattern variable should not shadow a postfix projection
-- in the same scope.

module Shadow where

  record R : Set₁ where
    field y : Set → Set
  open R

  -- Should succeed or maybe complain about pattern variable y,
  -- but not about the postfix projection pattern.

  test : R
  test .y y = y

-- Disambiguation

module Parens where

  record R : Set₁ where
    field p : Set
  open R

  data D : (R → Set) → Set₁ where
    c : D p

  test : (f : R → Set) (x : D f) → Set₁
  test .(p) c = Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Nat
open import Prelude
open import core
open import contexts
open import lemmas-disjointness
open import exchange

-- this module contains all the proofs of different weakening structural
-- properties that we use for the hypothetical judgements
module weakening where
  mutual
    weaken-subst-Δ : ∀{Δ1 Δ2 Γ σ Γ'} → Δ1 ## Δ2
                                     → Δ1 , Γ ⊢ σ :s: Γ'
                                     → (Δ1 ∪ Δ2) , Γ ⊢ σ :s: Γ'
    weaken-subst-Δ disj (STAId x) = STAId x
    weaken-subst-Δ disj (STASubst subst x) = STASubst (weaken-subst-Δ disj subst) (weaken-ta-Δ1 disj x)

    weaken-ta-Δ1 : ∀{Δ1 Δ2 Γ d τ} → Δ1 ## Δ2
                                  → Δ1 , Γ ⊢ d :: τ
                                  → (Δ1 ∪ Δ2) , Γ ⊢ d :: τ
    weaken-ta-Δ1 disj TAConst = TAConst
    weaken-ta-Δ1 disj (TAVar x₁) = TAVar x₁
    weaken-ta-Δ1 disj (TALam x₁ wt) = TALam x₁ (weaken-ta-Δ1 disj wt)
    weaken-ta-Δ1 disj (TAAp wt wt₁) = TAAp (weaken-ta-Δ1 disj wt) (weaken-ta-Δ1 disj wt₁)
    weaken-ta-Δ1 {Δ1} {Δ2} {Γ} disj (TAEHole {u = u} {Γ' = Γ'} x x₁) = TAEHole (x∈∪l Δ1 Δ2 u _ x ) (weaken-subst-Δ disj x₁)
    weaken-ta-Δ1 {Δ1} {Δ2} {Γ} disj (TANEHole {Γ' = Γ'} {u = u} x wt x₁) = TANEHole (x∈∪l Δ1 Δ2 u _ x) (weaken-ta-Δ1 disj wt) (weaken-subst-Δ disj x₁)
    weaken-ta-Δ1 disj (TACast wt x) = TACast (weaken-ta-Δ1 disj wt) x
    weaken-ta-Δ1 disj (TAFailedCast wt x x₁ x₂) = TAFailedCast (weaken-ta-Δ1 disj wt) x x₁ x₂

  -- this is a little bit of a time saver. since ∪ is commutative on
  -- disjoint contexts, and we need that premise anyway in both positions,
  -- there's no real reason to repeat the inductive argument above
  weaken-ta-Δ2 : ∀{Δ1 Δ2 Γ d τ} → Δ1 ## Δ2
                                → Δ2 , Γ ⊢ d :: τ
                                → (Δ1 ∪ Δ2) , Γ ⊢ d :: τ
  weaken-ta-Δ2 {Δ1} {Δ2} {Γ} {d} {τ} disj D = tr (λ q → q , Γ ⊢ d :: τ) (∪comm Δ2 Δ1 (##-comm disj)) (weaken-ta-Δ1 (##-comm disj) D)

  -- note that these statements are somewhat stronger than usual. this is
  -- because we don't have implcit α-conversion. this reifies the
  -- often-silent on paper assumption that if you collide with a bound
  -- variable you can just α-convert it away and not worry.
  mutual
    weaken-synth : ∀{ x Γ e τ τ'} → freshh x e
                                  → Γ ⊢ e => τ
                                  → (Γ ,, (x , τ')) ⊢ e => τ
    weaken-synth FRHConst SConst = SConst
    weaken-synth (FRHAsc frsh) (SAsc x₁) = SAsc (weaken-ana frsh x₁)
    weaken-synth {Γ = Γ} (FRHVar {x = x} x₁) (SVar {x = y} x₂) = SVar (x∈∪l Γ (■(x , _)) y _  x₂)
    weaken-synth {Γ = Γ} (FRHLam2 x₁ frsh) (SLam x₂ wt) =
                    SLam (apart-extend1 Γ (flip x₁) x₂)
                         (exchange-synth {Γ = Γ} (flip x₁) ((weaken-synth frsh wt)))
    weaken-synth FRHEHole SEHole = SEHole
    weaken-synth (FRHNEHole frsh) (SNEHole x₁ wt) = SNEHole x₁ (weaken-synth frsh wt)
    weaken-synth (FRHAp frsh frsh₁) (SAp x₁ wt x₂ x₃) = SAp x₁ (weaken-synth frsh wt) x₂ (weaken-ana frsh₁ x₃)

    weaken-ana : ∀{x Γ e τ τ'} → freshh x e
                               → Γ ⊢ e <= τ
                               → (Γ ,, (x , τ')) ⊢ e <= τ
    weaken-ana frsh (ASubsume x₁ x₂) = ASubsume (weaken-synth frsh x₁) x₂
    weaken-ana {Γ = Γ} (FRHLam1 neq frsh) (ALam x₂ x₃ wt) =
                     ALam (apart-extend1 Γ (flip neq) x₂)
                          x₃
                          (exchange-ana {Γ = Γ} (flip neq) (weaken-ana frsh wt))

  mutual
    weaken-subst-Γ : ∀{ x Γ Δ σ Γ' τ} →
                     envfresh x σ →
                     Δ , Γ ⊢ σ :s: Γ' →
                     Δ , (Γ ,, (x , τ)) ⊢ σ :s: Γ'
    weaken-subst-Γ {Γ = Γ} (EFId x₁) (STAId x₂) = STAId (λ x τ x₃ → x∈∪l Γ _ x τ (x₂ x τ x₃) )
    weaken-subst-Γ {x = x} {Γ = Γ} (EFSubst x₁ efrsh x₂) (STASubst {y = y} {τ = τ'} subst x₃) =
      STASubst (exchange-subst-Γ {Γ = Γ} (flip x₂) (weaken-subst-Γ {Γ = Γ ,, (y , τ')} efrsh subst))
               (weaken-ta x₁ x₃)

    weaken-ta : ∀{x Γ Δ d τ τ'} →
                fresh x d →
                Δ , Γ ⊢ d :: τ →
                Δ , Γ ,, (x , τ') ⊢ d :: τ
    weaken-ta _ TAConst = TAConst
    weaken-ta {x} {Γ} {_} {_} {τ} {τ'} (FVar x₂) (TAVar x₃) = TAVar (x∈∪l Γ (■ (x , τ')) _ _ x₃)
    weaken-ta {x = x} frsh (TALam {x = y} x₂ wt) with natEQ x y
    weaken-ta (FLam x₁ x₂) (TALam x₃ wt) | Inl refl = abort (x₁ refl)
    weaken-ta {Γ = Γ} {τ' = τ'} (FLam x₁ x₃) (TALam {x = y} x₄ wt) | Inr x₂ = TALam (apart-extend1 Γ (flip x₁) x₄) (exchange-ta-Γ {Γ = Γ} (flip x₁) (weaken-ta x₃ wt))
    weaken-ta (FAp frsh frsh₁) (TAAp wt wt₁) = TAAp (weaken-ta frsh wt) (weaken-ta frsh₁ wt₁)
    weaken-ta (FHole x₁) (TAEHole x₂ x₃) = TAEHole x₂ (weaken-subst-Γ x₁ x₃)
    weaken-ta (FNEHole x₁ frsh) (TANEHole x₂ wt x₃) = TANEHole x₂ (weaken-ta frsh wt) (weaken-subst-Γ x₁ x₃)
    weaken-ta (FCast frsh) (TACast wt x₁) = TACast (weaken-ta frsh wt) x₁
    weaken-ta (FFailedCast frsh) (TAFailedCast wt x₁ x₂ x₃) = TAFailedCast (weaken-ta frsh wt) x₁ x₂ x₃

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


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

module lib.Basics where

open import lib.Base public

open import lib.Equivalence public
open import lib.Function public
open import lib.Funext public
open import lib.NType public
open import lib.PathFunctor public
open import lib.PathGroupoid public
open import lib.PathOver public
open import lib.Relation public
open import lib.Univalence public

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
open import Data.Product using ( ∃ ; _×_ ; _,_ ; proj₁ ; proj₂ )
open import Relation.Unary using ( _∈_ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; cong )
open import Web.Semantic.DL.ABox.Interp using ( Interp ; _,_ ; ⌊_⌋ ; ind ; _*_ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox.Interp using
  ( Δ ; _⊨_≈_ ; ≈-refl ; ≈-sym ; ≈-trans ) renaming
  ( Interp to Interp′ )
open import Web.Semantic.DL.TBox.Interp.Morphism using
  ( ≲-image ; ≃-image ; ≃-image⁻¹ ; ≲-resp-≈ ; ≃-resp-≈ ; ≃-iso ) renaming
  ( _≲_ to _≲′_ ; _≃_ to _≃′_
  ; ≲-refl to ≲′-refl ; ≲-trans to ≲′-trans
  ; ≃-refl to ≃′-refl ; ≃-sym to ≃′-sym ; ≃-trans to ≃′-trans
  ; ≃-impl-≲ to ≃-impl-≲′ )
open import Web.Semantic.Util using
  ( _∘_ ; _⊕_⊕_ ; inode ; bnode ; enode ; →-dist-⊕ )

module Web.Semantic.DL.ABox.Interp.Morphism {Σ : Signature} where

infix 2 _≲_ _≃_ _≋_
infixr 4 _,_
infix 5 _**_

data _≲_ {X} (I J : Interp Σ X) : Set where
  _,_ : ∀ (I≲J : ⌊ I ⌋ ≲′ ⌊ J ⌋) →
    (i≲j : ∀ x → (⌊ J ⌋ ⊨ ≲-image I≲J (ind I x) ≈ ind J x)) →
      (I ≲ J)

≲⌊_⌋ : ∀ {X} {I J : Interp Σ X} → (I ≲ J) → (⌊ I ⌋ ≲′ ⌊ J ⌋)
≲⌊_⌋ (I≲J , i≲j) = I≲J

≲-resp-ind : ∀ {X} {I J : Interp Σ X} → (I≲J : I ≲ J) →
  ∀ x → (⌊ J ⌋ ⊨ ≲-image ≲⌊ I≲J ⌋ (ind I x) ≈ ind J x)
≲-resp-ind (I≲J , i≲j) = i≲j

≲-refl : ∀ {X} (I : Interp Σ X) → (I ≲ I)
≲-refl I = (≲′-refl ⌊ I ⌋ , λ x → ≈-refl ⌊ I ⌋)

≲-trans : ∀ {X} {I J K : Interp Σ X} → (I ≲ J) → (J ≲ K) → (I ≲ K)
≲-trans {X} {I} {J} {K} I≲J J≲K =
  (≲′-trans ≲⌊ I≲J ⌋ ≲⌊ J≲K ⌋ , λ x → ≈-trans ⌊ K ⌋ (≲-resp-≈ ≲⌊ J≲K ⌋ (≲-resp-ind I≲J x)) (≲-resp-ind J≲K x))

≡-impl-≈ : ∀ {X : Set} (I : Interp′ Σ) {i j : X → Δ I} →
  (i ≡ j) → (∀ x → I ⊨ i x ≈ j x)
≡-impl-≈ I refl x = ≈-refl I

≡³-impl-≈ : ∀ {V X Y : Set} (I : Interp′ Σ) (i j : (X ⊕ V ⊕ Y) → Δ I) →
  (→-dist-⊕ i ≡ →-dist-⊕ j) → (∀ x → I ⊨ i x ≈ j x)
≡³-impl-≈ I i j i≡j (inode x) = ≡-impl-≈ I (cong proj₁ i≡j) x
≡³-impl-≈ I i j i≡j (bnode v) = ≡-impl-≈ I (cong proj₁ (cong proj₂ i≡j)) v
≡³-impl-≈ I i j i≡j (enode y) = ≡-impl-≈ I (cong proj₂ (cong proj₂ i≡j)) y

≡-impl-≲ : ∀ {X : Set} (I : Interp Σ X) j →
  (ind I ≡ j) → (I ≲ (⌊ I ⌋ , j))
≡-impl-≲ (I , i) .i refl = ≲-refl (I , i)

≡³-impl-≲ : ∀ {V X Y : Set} (I : Interp Σ (X ⊕ V ⊕ Y)) j →
  (→-dist-⊕ (ind I) ≡ →-dist-⊕ j) → (I ≲ (⌊ I ⌋ , j))
≡³-impl-≲ (I , i) j i≡j = (≲′-refl I , ≡³-impl-≈ I i j i≡j)

_**_ : ∀ {X Y I J} (f : Y → X) → (I ≲ J) → (f * I ≲ f * J)
f ** I≲J = (≲⌊ I≲J ⌋ , λ x → ≲-resp-ind I≲J (f x))

_≋_ : ∀ {X} {I J : Interp Σ X} → (I ≲ J) → (I ≲ J) → Set
_≋_ {X} {I} {J} I≲₁J I≲₂J = ∀ x → (⌊ J ⌋ ⊨ ≲-image ≲⌊ I≲₁J ⌋ x ≈ ≲-image ≲⌊ I≲₂J ⌋ x)

data _≃_ {X} (I J : Interp Σ X) : Set₁ where
  _,_ : (I≃J : ⌊ I ⌋ ≃′ ⌊ J ⌋) →
    (∀ x → (⌊ J ⌋ ⊨ ≃-image I≃J (ind I x) ≈ ind J x)) →
      (I  ≃ J)

≃⌊_⌋ : ∀ {X} {I J : Interp Σ X} → (I ≃ J) → (⌊ I ⌋ ≃′ ⌊ J ⌋)
≃⌊_⌋ (I≃J , i≃j) = I≃J

≃-impl-≲ : ∀ {X} {I J : Interp Σ X} → (I ≃ J) → (I ≲ J)
≃-impl-≲ (I≃J , i≃j) = (≃-impl-≲′ I≃J , i≃j)

≃-resp-ind : ∀ {X} {I J : Interp Σ X} → (I≃J : I ≃ J) →
  ∀ x → (⌊ J ⌋ ⊨ ≃-image ≃⌊ I≃J ⌋ (ind I x) ≈ ind J x)
≃-resp-ind (I≃J , i≃j) = i≃j

≃-resp-ind⁻¹ : ∀ {X} {I J : Interp Σ X} → (I≃J : I ≃ J) →
  ∀ x → (⌊ I ⌋ ⊨ ≃-image⁻¹ ≃⌊ I≃J ⌋ (ind J x) ≈ ind I x)
≃-resp-ind⁻¹ {X} {I , i} {J , j} (I≃J , i≃j) x =
  ≈-trans I (≃-resp-≈ (≃′-sym I≃J) (≈-sym J (i≃j x))) (≃-iso I≃J (i x))

≃-refl : ∀ {X} (I : Interp Σ X) → (I ≃ I)
≃-refl (I , i) = (≃′-refl I , λ x → ≈-refl I)

≃-symm : ∀ {X} {I J : Interp Σ X} → (I ≃ J) → (J ≃ I)
≃-symm {X} {I , i} {J , j} (I≃J , i≃j) =
  (≃′-sym I≃J , ≃-resp-ind⁻¹ {X} {I , i} {J , j} (I≃J , i≃j))

≃-trans : ∀ {X} {I J K : Interp Σ X} → (I ≃ J) → (J ≃ K) → (I ≃ K)
≃-trans {X} {I , i} {J , j} {K , k} (I≃J , i≃j) (J≃K , j≃k) =
  (≃′-trans I≃J J≃K , λ x → ≈-trans K (≃-resp-≈ J≃K (i≃j x)) (j≃k x))

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
module _ where

record R : Set₁ where
  field
    overlap A :  Set


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Identity
open import HoTT.Equivalence

module HoTT.Identity.Sigma where

open variables

_=Σ_ : Σ A P → Σ A P → 𝒰 _
_=Σ_ {P = P} x y = Σ[ p ∶ x₁ == y₁ ] transport P p x₂ == y₂
  where
  open Σ x renaming (pr₁ to x₁ ; pr₂ to x₂)
  open Σ y renaming (pr₁ to y₁ ; pr₂ to y₂)

pair⁼' : {x y : Σ A P} → Σ[ p ∶ pr₁ x == pr₁ y ] pr₂ x == transport P (p ⁻¹) (pr₂ y) → x == y
pair⁼' {x = _ , _} {y = _ , _} (refl , refl) = refl

=Σ-equiv : {x y : Σ A P} → (x == y) ≃ x =Σ y
=Σ-equiv {x = _ , _} {y = _ , _} = let open Iso in iso→eqv λ where
  .f refl → (refl , refl)
  .g (refl , refl) → refl
  .η refl → refl
  .ε (refl , refl) → refl

pair⁼ : {x y : Σ A P} → x =Σ y → x == y
pair⁼ = Iso.g (eqv→iso =Σ-equiv)


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

-- Some basic theorems on paths and path compositions.
module hott.core.equality.theorems where

open import hott.core

-- The path refl is the left identity under path concatnation.
refl∙p≡p : ∀ {ℓ} {A : Type ℓ}  {x y : A}
                      → ∀ (p : x ≡ y)
                      → refl ∙ p ≡ p
refl∙p≡p refl = refl

-- Alternate form of refl being left identity.
p≡refl∙p : ∀ {ℓ} {A : Type ℓ}  {x y : A}
         → ∀ (p : x ≡ y)
         → p ≡ refl ∙ p
p≡refl∙p p = refl∙p≡p p ⁻¹

-- The path refl is the right identity under path concatnation.
p∙refl≡p : ∀ {ℓ} {A : Type ℓ}  {x y : A}
         → ∀ (p : x ≡ y)
         → p ∙ refl ≡ p

p∙refl≡p refl = refl

-- Alternate form of refl being the right identity.
p≡p∙refl : ∀ {ℓ} {A : Type ℓ}  {x y : A}
         → ∀ (p : x ≡ y)
         → p ≡ p ∙ refl

p≡p∙refl p = p∙refl≡p p ⁻¹

-- The inverse of inverse is identity
p⁻¹⁻¹≡p  : ∀ {ℓ} {A : Type ℓ}  {x y : A}
         → ∀ (p : x ≡ y)
         → (p ⁻¹)⁻¹ ≡ p
p⁻¹⁻¹≡p refl = refl

-- Alternate form of the theorem inverse of inverse is identity.
p≡p⁻¹⁻¹  : ∀ {ℓ} {A : Type ℓ}  {x y : A}
         → ∀ (p : x ≡ y)
         → p ≡ (p ⁻¹)⁻¹
p≡p⁻¹⁻¹ p = p⁻¹⁻¹≡p p ⁻¹

-- Inverse is actually right inverse.
p∙p⁻¹≡refl : ∀ {ℓ} {A : Type ℓ}  {x y : A}
          → ∀ (p : x ≡ y)
          → p ∙ p ⁻¹ ≡ refl
p∙p⁻¹≡refl refl = refl

-- Inverse is actually left inverse.
p⁻¹∙p≡refl : ∀ {ℓ} {A : Type ℓ}  {x y : A}
          → ∀ (p : x ≡ y)
          → p ⁻¹ ∙ p ≡ refl
p⁻¹∙p≡refl refl = refl

-- The associativity of path composition.
assoc :  ∀ {ℓ} {A : Type ℓ}  {u v w x : A}
      → (p : u ≡ v)
      → (q : v ≡ w)
      → (r : w ≡ x)
      → (p ∙ q) ∙ r ≡ p ∙ (q ∙ r)
assoc refl refl refl = refl

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.Abstract.Types
open import LibraBFT.Impl.NetworkMsg
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.Yasm.System     ConcSysParms
open import LibraBFT.Yasm.Properties ConcSysParms

-- This module collects the implementation obligations for our (fake/simple, for now)
-- "implementation" into the structure required by Concrete.Properties.

open import LibraBFT.Concrete.Obligations

module LibraBFT.Impl.Properties where

  open import LibraBFT.Impl.Properties.Aux
  open import LibraBFT.Concrete.System impl-sps-avp
  import      LibraBFT.Impl.Properties.VotesOnce   as VO
  import      LibraBFT.Impl.Properties.LockedRound as LR

  theImplObligations : ImplObligations
  theImplObligations = record { sps-cor = impl-sps-avp
                              ; vo₁     = VO.vo₁
                              ; vo₂     = VO.vo₂
                              ; lr₁     = LR.lr₁ }


text:
module LC.Subst where

open import LC.Base
open import LC.Subst.Var
open import LC.Subst.Term
open import LC.Subst.Term public using (lift)

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Nullary

--------------------------------------------------------------------------------
-- substitution

infixl 10 _[_/_]
_[_/_] : Term → Term → ℕ → Term
(var x) [ N / i ] = subst-var (match x i) N
(ƛ M)   [ N / i ] = ƛ (M [ N / suc i ])
(L ∙ M) [ N / i ] = L [ N / i ] ∙ M [ N / i ]

-- substitute the 0th var in M for N
infixl 10 _[_]
_[_] : Term → Term → Term
M [ N ] = M [ N / 0 ]

--------------------------------------------------------------------------------
-- properties regarding substitution

open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary.Negation using (contradiction)
open ≡-Reasoning

subst-< : ∀ x i N → x < i → (var x) [ N / i ] ≡ var x
subst-< x i N x<i with match x i
... | Under x<i' = refl
... | Exact x≡i  = contradiction x≡i (<⇒≢ x<i)
... | Above v x≥i = contradiction (≤-step (≤-pred x≥i)) (<⇒≱ x<i)

subst-≡ : ∀ x i N → x ≡ i → (var x) [ N / i ] ≡ lift 0 i N
subst-≡ x i N x≡i with match x i
... | Under x<i  = contradiction x≡i (<⇒≢ x<i)
... | Exact x≡i' = refl
... | Above v x≥i = contradiction (sym x≡i) (<⇒≢ x≥i)

subst-> : ∀ x i N → suc x > i → (var suc x) [ N / i ] ≡ var x
subst-> x i N x≥i with match (suc x) i
... | Under x<i = contradiction (≤-pred (≤-step x<i)) (<⇒≱ x≥i)
... | Exact x≡i  = contradiction (sym x≡i) (<⇒≢ x≥i)
... | Above v x≥i' = refl

subst-[]-var : ∀ m n i x N
  → subst-var (match (lift-var n m x) (n + m + i)) N
  ≡ lift n m (subst-var (match x (n + i)) N)
subst-[]-var m n i x N with inspectBinding n x
subst-[]-var m n i x N | Free n≤x with match x (n + i)
subst-[]-var m n i x N | Free n≤x | Under x<n+i =
    begin
        subst-var (match (m + x) (n + m + i)) N
    ≡⟨ subst-var-match-< {m + x} {n + m + i} N (LC.Subst.Var.INEQ.l+m+n>m+x n m i x x<n+i) ⟩
        var (m + x)
    ≡⟨ cong var_ (sym (LC.Subst.Var.lift-var-≤ n≤x)) ⟩
        var lift-var n m x
    ∎
subst-[]-var m n i x N | Free n≤x | Exact x≡n+i =
    begin
        subst-var (match (m + x) (n + m + i)) N
    ≡⟨ subst-var-match-≡ {m + x} {n + m + i} N (sym (LC.Subst.Var.EQ.l+m+n≡m+x n m i x (sym x≡n+i))) ⟩
        lift 0 (n + m + i) N
    ≡⟨ lift-lemma 0 m n i N ⟩
        lift n m (lift 0 (n + i) N)
    ∎
subst-[]-var m n i .(suc v) N | Free n≤x | Above v x≥n+i =
    begin
        subst-var (match (m + suc v) (n + m + i)) N
    ≡⟨ cong (λ w → subst-var (match w (n + m + i)) N) (+-suc m v) ⟩
        subst-var (match (suc m + v) (n + m + i)) N
    ≡⟨ subst-var-match-> {m + v} {n + m + i} N (s≤s (LC.Subst.Var.INEQ.l+m+n≤m+x n m i v (≤-pred x≥n+i))) ⟩
        var (m + v)
    ≡⟨ cong var_ (sym (LC.Subst.Var.lift-var-≤ {n} {m} {v} (≤-trans (m≤m+n n i) (≤-pred x≥n+i)))) ⟩
        var lift-var n m v
    ∎
subst-[]-var m n i x N | Bound n>x =
    begin
        subst-var (match x (n + m + i)) N
    ≡⟨ subst-var-match-< N (≤-trans n>x (≤-trans (m≤m+n n m) (m≤m+n (n + m) i))) ⟩
        var x
    ≡⟨ cong var_ (sym (LC.Subst.Var.lift-var-> n>x)) ⟩
        var lift-var n m x
    ≡⟨⟩
        lift n m (var x)
    ≡⟨ cong (lift n m) (sym (subst-var-match-< N (≤-trans n>x (m≤m+n n i)))) ⟩
        lift n m (subst-var (match x (n + i)) N)
    ∎

lemma : ∀ {m n i} M N
  → lift (suc ((m + n))) i M [ lift n i N / m ]
  ≡ lift (m + n)         i (M [ N / m ])
lemma {m} {n} {i} (var x) N = LC.Subst.Term.subst-var-lift _ _ _ x N
lemma (ƛ M)   N = cong  ƛ_   (lemma M N)
lemma (K ∙ M) N = cong₂ _∙_  (lemma K N) (lemma M N)

lift-[] : ∀ n m i M N → lift n m (M [ N / n + i ]) ≡ lift n m M [ N / n + m + i ]
lift-[] n m i (var x) N = sym (subst-[]-var m n i x N)
lift-[] n m i (ƛ M) N = cong ƛ_ (lift-[] (suc n) m i M N)
lift-[] n m i (M ∙ M') N = cong₂ _∙_ (lift-[] n m i M N) (lift-[] n m i M' N)

lift-subst-var : ∀ l m n i x N → n ≥ i → i ≥ m → lift (l + m) (suc n) (var x) [ N / l + i ] ≡ lift (l + m) n (var x)
lift-subst-var l m n i x N n≥i i≥m with inspectBinding (l + m) x
... | Free l+m≤x =
  begin
      subst-var (match (suc (n + x)) (l + i)) N
  ≡⟨ subst-var-match-> {n + x} {l + i} N (s≤s prop) ⟩
      var (n + x)
  ∎
  where
    prop : l + i ≤ n + x
    prop = ≤-trans (≤-reflexive (+-comm l i)) (+-mono-≤ n≥i (≤-trans (m≤m+n l m) l+m≤x))

... | Bound l+m>x =
    begin
        subst-var (match x (l + i)) N
    ≡⟨ subst-var-match-< {x} {l + i} N prop ⟩
        var x
    ∎
    where
      prop : x < l + i
      prop = ≤-trans l+m>x (+-monoʳ-≤ l i≥m)

lift-subst : ∀ l m n i M N → n ≥ i → i ≥ m → lift (l + m) (suc n) M [ N / l + i ] ≡ lift (l + m) n M
lift-subst l m n i (var x) N n≥i i≥m = lift-subst-var l m n i x N n≥i i≥m
lift-subst l m n i (ƛ M)   N n≥i i≥m = cong ƛ_ (lift-subst (suc l) m n i M N n≥i i≥m)
lift-subst l m n i (L ∙ M) N n≥i i≥m = cong₂ _∙_ (lift-subst l m n i L N n≥i i≥m) (lift-subst l m n i M N n≥i i≥m)

subst-var-match-[] : ∀ {m i} x M N
    → subst-var (match x (suc (m + i))) N [ M [ N / i ] / m     ]
    ≡ subst-var (match x       m      ) M [ N           / m + i ]
subst-var-match-[] {m} {i} x M N with match x m
... | Under x<m =
    begin
        subst-var (match x (suc (m + i))) N [ M [ N / i ] / m ]
    ≡⟨ (cong (_[ M [ N / i ] / m ])) (LC.Subst.Term.subst-var-match-< N (≤-trans x<m (≤-step (m≤m+n m i)))) ⟩
        (var x) [ M [ N / i ] / m ]
    ≡⟨ subst-< x m (M [ N / i ]) x<m ⟩
        var x
    ≡⟨ sym (LC.Subst.Term.subst-var-match-< N (≤-trans x<m (m≤m+n m i))) ⟩
        subst-var (match x (m + i)) N
    ∎
... | Exact x≡m =
    begin
        subst-var (match x (suc (m + i))) N [ M [ N / i ] / m ]
    ≡⟨ cong (_[ M [ N / i ] / m ]) (LC.Subst.Term.subst-var-match-< N (≤-trans (s≤s (≤-reflexive x≡m)) (s≤s (m≤m+n m i)))) ⟩
        (var x) [ M [ N / i ] / m ]
    ≡⟨ subst-≡ x m (M [ N / i ]) x≡m ⟩
        lift 0 m (M [ N / i ])
    ≡⟨ lift-[] 0 m i M N ⟩
        lift 0 m M [ N / m + i ]
    ∎
... | Above v v≥m with match v (m + i)
... | Under v<m+i =
    begin
        subst-var (match (suc v) (suc (m + i))) N [ M [ N / i ] / m ]
    ≡⟨ cong (_[ M [ N / i ] / m ]) (LC.Subst.Term.subst-var-match-< {suc v} {suc m + i} N (s≤s v<m+i)) ⟩
        (var suc v) [ M [ N / i ] / m ]
    ≡⟨ subst-> v m (M [ N / i ]) v≥m ⟩
        var v
    ∎
... | Exact v≡m+i =
    begin
        subst-var (match (suc v) (suc (m + i))) N [ M [ N / i ] / m ]
    ≡⟨ cong (_[ M [ N / i ] / m ]) (LC.Subst.Term.subst-var-match-≡ {suc v} {suc m + i} N (cong suc v≡m+i)) ⟩
        lift 0 (suc m + i) N [ M [ N / i ] / m ]
    ≡⟨ lift-subst 0 0 (m + i) m N (M [ N / i ]) (m≤m+n m i) z≤n ⟩
        lift 0 (m + i) N
    ∎
... | Above v' v>m+i =
    begin
        subst-var (match (suc (suc v')) (suc (m + i))) N [ M [ N / i ] / m ]
    ≡⟨ cong (_[ M [ N / i ] / m ]) (LC.Subst.Term.subst-var-match-> {suc v'} {suc m + i} N (s≤s v>m+i)) ⟩
        (var (suc v')) [ M [ N / i ] / m ]
    ≡⟨ subst-> v' m (M [ N / i ]) (≤-trans (s≤s (m≤m+n m i)) v>m+i) ⟩
        var v'
    ∎

subst-lemma : ∀ {m i} M N O
    → M [ O / suc m + i ] [ N [ O / i ] / m     ]
    ≡ M [ N /     m     ] [ O           / m + i ]
subst-lemma (var x) N O = subst-var-match-[] x N O
subst-lemma (ƛ M)   N O = cong ƛ_ (subst-lemma M N O)
subst-lemma (M ∙ L) N O = cong₂ _∙_ (subst-lemma M N O) (subst-lemma L N O)

max_stars_repo_name: banacorn/bidirectional

max_issues_repo_name: banacorn/bidirectional

max_forks_repo_name: banacorn/bidirectional


text:
open import Level hiding ( suc ; zero )
open import Algebra
module Solvable {n m : Level} (G : Group n m ) where

open import Data.Unit
open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
open import Function
open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
open import Relation.Nullary
open import Data.Empty
open import Data.Product
open import  Relation.Binary.PropositionalEquality hiding ( [_] ; sym )

open Group G
open import Gutil G

[_,_] :  Carrier   → Carrier   → Carrier
[ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h

data Commutator (P : Carrier → Set (Level.suc n ⊔ m)) : (f : Carrier) → Set (Level.suc n ⊔ m) where
  comm  : {g h : Carrier} → P g → P h  → Commutator P [ g , h ]
  ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g

deriving : ( i : ℕ ) → Carrier → Set (Level.suc n ⊔ m)
deriving 0 x = Lift (Level.suc n ⊔ m) ⊤
deriving (suc i) x = Commutator (deriving i) x

open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )

deriving-subst : { i : ℕ } → {x y : Carrier } → x ≈ y → (dx : deriving i x ) → deriving i y
deriving-subst {zero} {x} {y} x=y dx = lift tt
deriving-subst {suc i} {x} {y} x=y dx = ccong x=y dx

record solvable : Set (Level.suc n ⊔ m) where
  field
     dervied-length : ℕ
     end : (x : Carrier ) → deriving dervied-length x →  x ≈ ε

-- deriving stage is closed on multiplication and inversion

import Relation.Binary.Reasoning.Setoid as EqReasoning

open EqReasoning (Algebra.Group.setoid G)

lemma4 : (g h : Carrier ) → [ h , g ] ≈ [ g , h ] ⁻¹
lemma4 g h = begin
       [ h , g ]                               ≈⟨ grefl ⟩
       (h ⁻¹ ∙ g ⁻¹ ∙   h ) ∙ g                ≈⟨ assoc _ _ _ ⟩
       h ⁻¹ ∙ g ⁻¹ ∙  (h ∙ g)                  ≈⟨ ∙-cong grefl (gsym (∙-cong lemma6 lemma6))  ⟩
       h ⁻¹ ∙  g ⁻¹ ∙ ((h ⁻¹) ⁻¹ ∙ (g ⁻¹) ⁻¹)  ≈⟨  ∙-cong grefl (lemma5 _ _ )  ⟩
       h ⁻¹ ∙  g ⁻¹ ∙  (g ⁻¹ ∙ h ⁻¹) ⁻¹        ≈⟨ assoc _ _ _ ⟩
       h ⁻¹ ∙ (g ⁻¹ ∙  (g ⁻¹ ∙ h ⁻¹) ⁻¹)       ≈⟨ ∙-cong grefl (lemma5 (g ⁻¹ ∙ h ⁻¹ ) g ) ⟩
       h ⁻¹ ∙ (g ⁻¹ ∙   h ⁻¹ ∙ g) ⁻¹           ≈⟨ lemma5 (g ⁻¹ ∙ h ⁻¹ ∙ g) h ⟩
       (g ⁻¹ ∙ h ⁻¹ ∙   g ∙ h) ⁻¹              ≈⟨ grefl ⟩
       [ g , h ]  ⁻¹
     ∎

deriving-inv : { i : ℕ } → { x  : Carrier } → deriving i x → deriving i ( x ⁻¹ )
deriving-inv {zero} {x} (lift tt) = lift tt
deriving-inv {suc i} {_} (comm x x₁ )   = ccong (lemma4 _ _) (comm x₁ x)
deriving-inv {suc i} {x} (ccong eq ix ) = ccong (⁻¹-cong eq) ( deriving-inv ix )

idcomtr : (g  : Carrier ) → [ g , ε  ] ≈ ε
idcomtr g  = begin
       (g ⁻¹ ∙ ε  ⁻¹ ∙   g ∙ ε )              ≈⟨ ∙-cong (∙-cong (∙-cong grefl (sym lemma3 )) grefl ) grefl ⟩
       (g ⁻¹ ∙ ε   ∙   g ∙ ε )                ≈⟨ ∙-cong (∙-cong (proj₂ identity _) grefl)  grefl ⟩
       (g ⁻¹   ∙   g ∙ ε     )                ≈⟨ ∙-cong (proj₁ inverse _ )   grefl ⟩
       (  ε  ∙ ε     )                        ≈⟨  proj₂ identity _  ⟩
       ε
     ∎

idcomtl : (g  : Carrier ) → [ ε ,  g ] ≈ ε
idcomtl g  = begin
       (ε ⁻¹ ∙ g  ⁻¹ ∙   ε ∙ g )              ≈⟨ ∙-cong (proj₂ identity _) grefl ⟩
       (ε ⁻¹ ∙ g  ⁻¹ ∙    g )                ≈⟨ ∙-cong (∙-cong (sym lemma3 ) grefl ) grefl ⟩
       (ε  ∙ g  ⁻¹ ∙    g )                  ≈⟨ ∙-cong (proj₁ identity _) grefl ⟩
       (g ⁻¹   ∙    g     )                ≈⟨  proj₁ inverse _ ⟩
       ε
     ∎

deriving-ε : { i : ℕ } → deriving i ε
deriving-ε {zero} = lift tt
deriving-ε {suc i} = ccong (idcomtr ε) (comm deriving-ε deriving-ε)

comm-refl : {f g : Carrier } → f ≈ g  → [ f ,  g ] ≈ ε
comm-refl {f} {g} f=g = begin
       f ⁻¹ ∙ g ⁻¹ ∙   f ∙ g
     ≈⟨ ∙-cong (∙-cong (∙-cong (⁻¹-cong f=g ) grefl ) f=g ) grefl ⟩
       g ⁻¹ ∙ g ⁻¹ ∙   g ∙ g
     ≈⟨ ∙-cong (assoc _ _ _ ) grefl  ⟩
       g ⁻¹ ∙ (g ⁻¹ ∙   g ) ∙ g
     ≈⟨ ∙-cong (∙-cong grefl (proj₁ inverse _) ) grefl ⟩
       g ⁻¹ ∙ ε  ∙ g
     ≈⟨ ∙-cong (proj₂ identity _) grefl  ⟩
       g ⁻¹ ∙  g
     ≈⟨  proj₁ inverse _  ⟩
       ε
     ∎

comm-resp : {g h g1 h1  : Carrier } → g ≈ g1  → h ≈ h1 → [ g , h ] ≈ [ g1 , h1 ]
comm-resp {g} {h} {g1} {h1} g=g1 h=h1 =  ∙-cong (∙-cong (∙-cong (⁻¹-cong g=g1 ) (⁻¹-cong h=h1 )) g=g1 ) h=h1

max_stars_repo_name: shinji-kono/Galois

max_issues_repo_name: shinji-kono/Galois

max_forks_repo_name: shinji-kono/Galois