text:
------------------------------------------------------------------------
-- Tactics for proving instances of Σ-cong (and Surjection.Σ-cong)
-- with "better" computational behaviour
------------------------------------------------------------------------

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

open import Equality

module Tactic.Sigma-cong
  {e⁺} (eq : ∀ {a p} → Equality-with-J a p e⁺) where

open Derived-definitions-and-properties eq

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

open import Bijection eq as B using (_↔_)
open import Equivalence eq as Eq using (_≃_)
open import Function-universe eq as F hiding (id; _∘_)
open import Monad eq
open import Surjection eq as S using (_↠_)
open import TC-monad eq hiding (Type)

private

  variable
    a b                 : Level
    A B                 : Type a
    f g k k₁ k₂ p q x y : A
    P Q                 : A → Type p

------------------------------------------------------------------------
-- Σ-cong-refl

-- Building blocks used to construct the proofs in Σ-cong-refl.

record Σ-cong-refl-proofs
         (k : Kind)
         (A : Type a) (B : Type b) (P : A → Type p) (Q : B → Type q) :
         Type (lsuc (a ⊔ b ⊔ p ⊔ q)) where
  field
    refl₁ : (x : Σ B Q) → x ≡ x
    refl₂ : (x : Σ A P) → x ≡ x

    cong-refl₃ :
      (f : Σ A P → Σ B Q)
      (p : Σ A P) →
      cong f (refl p) ≡ refl (f p)

    →↝ :
      (A⇔B : A ⇔ B)
      (P→Q : ∀ x → P x → Q (_⇔_.to A⇔B x))
      (Q→P : ∀ x → Q x → P (_⇔_.from A⇔B x)) →
      (eq₁ : (p : Σ B Q) →
             Σ-map (_⇔_.to A⇔B) (P→Q _)
               (Σ-map (_⇔_.from A⇔B) (Q→P _) p) ≡
             p) →
      (eq₂ : (p : Σ A P) →
             Σ-map (_⇔_.from A⇔B) (Q→P _)
               (Σ-map (_⇔_.to A⇔B) (P→Q _) p) ≡
             p) →
      ((p : Σ A P) →
       cong (Σ-map (_⇔_.to A⇔B) (P→Q _)) (eq₂ p) ≡
       eq₁ (Σ-map (_⇔_.to A⇔B) (P→Q _) p)) →
      Σ A P ↝[ k ] Σ B Q

instance

  -- The building blocks can be proved.

  instance-of-Σ-cong-refl-proofs :
    Σ-cong-refl-proofs k A B P Q
  instance-of-Σ-cong-refl-proofs = λ where
      .refl₁ _              → refl _
      .refl₂ _              → refl _
      .cong-refl₃ _ _       → cong-refl _
      .→↝ A⇔B P→Q Q→P p q r →
        from-equivalence $
        Eq.⟨   Σ-map (_⇔_.to   A⇔B) (P→Q _)
           , ( Σ-map (_⇔_.from A⇔B) (Q→P _)
             , p
             , q
             , r
             )
           ⟩
    where
    open Σ-cong-refl-proofs

private

  -- Used to implement Σ-cong-refl.
  --
  -- The constructed term is returned.

  Σ-cong-refl-tactic :
    Σ-cong-refl-proofs k A B P Q →
    (A⇔B : A ⇔ B) → (∀ x → P x ⇔ Q (_⇔_.to A⇔B x)) →
    Term → TC Term
  Σ-cong-refl-tactic proofs A⇔B P⇔Q goal = do
    refl₁      ← quoteTC (Σ-cong-refl-proofs.refl₁      proofs)
    refl₂      ← quoteTC (Σ-cong-refl-proofs.refl₂      proofs)
    cong-refl₃ ← quoteTC (Σ-cong-refl-proofs.cong-refl₃ proofs
                            (Σ-map (_⇔_.to A⇔B) (_⇔_.to (P⇔Q _))))
    proofs     ← quoteTC proofs
    P→Q        ← quoteTC (_⇔_.to   ∘ P⇔Q)
    Q→P        ← quoteTC (_⇔_.from ∘ P⇔Q ∘ _⇔_.from A⇔B)
    A⇔B        ← quoteTC A⇔B
    let t = def (quote Σ-cong-refl-proofs.→↝)
                (varg proofs ∷
                 varg A⇔B ∷
                 varg P→Q ∷
                 varg Q→P ∷
                 varg refl₁ ∷
                 varg refl₂ ∷
                 varg cong-refl₃ ∷
                 [])
    unify goal t
    return t

macro

  -- A macro that tries to prove Σ A P ↝[ k₃ ] Σ B Q.
  --
  -- If k₃ is symmetric, then the two directions of the proof are
  -- constructed in the following way:
  --
  -- * The forward direction is a function from Σ A P to Σ B Q,
  --   constructed in the "obvious" way using the forward directions
  --   of the two supplied proofs.
  --
  -- * The other direction is a function from Σ B (Q ∘ f ∘ g) to
  --   Σ A P, where f and g are the two directions of the first proof.
  --   This function is also constructed in the "obvious" way, using
  --   the right-to-left directions of the two supplied proofs. It is
  --   assumed that Q ∘ f ∘ g is definitionally equal to Q.
  --
  -- The two functions are assumed to be definitionally equal, so that
  -- they can be proved to be inverses of each other (pointwise) using
  -- reflexivity.

  Σ-cong-refl :
    {k₁ k₂ : Symmetric-kind} {k₃ : Kind}
    ⦃ proofs : Σ-cong-refl-proofs k₃ A B P Q ⦄ →
    (A↝B : A ↝[ ⌊ k₁ ⌋-sym ] B) →
    (∀ x → P x ↝[ ⌊ k₂ ⌋-sym ] Q (_⇔_.to (sym→⇔ A↝B) x)) →
    Term → TC ⊤
  Σ-cong-refl ⦃ proofs = proofs ⦄ A↝B P↝Q goal = do
    Σ-cong-refl-tactic proofs (sym→⇔ A↝B) (sym→⇔ ∘ P↝Q) goal
    return _

private

  -- Some unit tests.

  t₁ : (A × A) ≃ (A × A)
  t₁ = Σ-cong-refl L.id λ _ → B.id

  _ : _≃_.to t₁ p ≡ p
  _ = refl _

  _ : _≃_.from t₁ p ≡ p
  _ = refl _

  _ :
    {p : A × A} →
    _≃_.right-inverse-of t₁ p ≡ refl _
  _ = refl _

  _ :
    {p : A × A} →
    _≃_.left-inverse-of t₁ p ≡ refl _
  _ = refl _

  t₂ : (A × A) ↔ (A × A)
  t₂ = Σ-cong-refl Eq.id λ _ → L.id

  _ : _↔_.to t₂ p ≡ p
  _ = refl _

  _ : _↔_.from t₂ p ≡ p
  _ = refl _

  _ :
    {p : A × A} →
    _↔_.right-inverse-of t₂ p ≡ refl _
  _ = refl _

  _ :
    {p : A × A} →
    _↔_.left-inverse-of t₂ p ≡ refl _
  _ = refl _

  t₃ :
    {P : A → B → Type p} {Q : A → B → (∀ x y → P x y) → Type q} →
    (∃ λ (f : ∀ x y → P x y) → ∀ x y → Q x y f) ≃
    (∃ λ (f : ∀ y x → P x y) → ∀ y x → Q x y (flip f))
  t₃ = Σ-cong-refl Π-comm λ _ → Π-comm

  _ : _≃_.to t₃ p ≡ Σ-map flip flip p
  _ = refl _

  _ : _≃_.from t₃ p ≡ Σ-map flip flip p
  _ = refl _

  _ :
    {P : A → B → Type p} {Q : A → B → (∀ x y → P x y) → Type q}
    {p : ∃ λ (f : ∀ y x → P x y) → ∀ y x → Q x y (flip f)} →
    _≃_.right-inverse-of (t₃ {Q = Q}) p ≡ refl _
  _ = refl _

  _ :
    {P : A → B → Type p} {Q : A → B → (∀ x y → P x y) → Type q}
    {p : ∃ λ (f : ∀ x y → P x y) → ∀ x y → Q x y f} →
    _≃_.left-inverse-of (t₃ {Q = Q}) p ≡ refl _
  _ = refl _

  -- The following proof—implemented using Σ-cong—is, at the time of
  -- writing, "worse".

  t₃′ :
    {P : A → B → Type p} {Q : A → B → (∀ x y → P x y) → Type q} →
    (∃ λ (f : ∀ x y → P x y) → ∀ x y → Q x y f) ≃
    (∃ λ (f : ∀ y x → P x y) → ∀ y x → Q x y (flip f))
  t₃′ = Eq.↔⇒≃ $ Σ-cong Π-comm λ _ → Π-comm

  _ : _≃_.to t₃′ p ≡ Σ-map flip flip p
  _ = refl _

  _ :
    ∀ {P : A → B → Type p} {Q : A → B → (∀ x y → P x y) → Type q} {p} →
    _≃_.from (t₃′ {Q = Q}) p ≡
    Σ-map flip
      (flip ∘ subst (λ f → ∀ y x → Q x y (flip f)) (sym (refl _)))
      p
  _ = refl _

------------------------------------------------------------------------
-- Σ-cong-id

-- Building blocks used to construct the proofs in Σ-cong-id.

record Σ-cong-id-proofs
         (k : Kind) (A : Type a) (B : Type b) (P : B → Type p) :
         Type (lsuc (a ⊔ b ⊔ p)) where
  field
    refl₁ : (x : Σ B P) → x ≡ x

    subst-refl₂ :
      (A≃B : A ≃ B)
      ((x , y) : Σ A (P ∘ _≃_.to A≃B)) →
      subst P (refl (_≃_.to A≃B x)) y ≡ y

    →↝ :
      (A≃B : A ≃ B)
      (g : ∀ x → P x → P (_≃_.to A≃B (_≃_.from A≃B x))) →
      ((p : Σ B P) →
       Σ-map (_≃_.to A≃B) id (Σ-map (_≃_.from A≃B) (g _) p) ≡ p) →
      (((x , y) : Σ A (P ∘ _≃_.to A≃B)) →
       subst P (_≃_.right-inverse-of A≃B (_≃_.to A≃B x)) (g _ y) ≡ y) →
      Σ A (P ∘ _≃_.to A≃B) ↝[ k ] Σ B P

instance

  -- The building blocks can be proved.

  instance-of-Σ-cong-id-proofs : Σ-cong-id-proofs k A B P
  instance-of-Σ-cong-id-proofs {P = P} = λ where
      .refl₁           → refl
      .subst-refl₂ _ _ → subst-refl _ _
      .→↝ A≃B g p q    →
        let open _≃_ A≃B in
        from-equivalence $
        Eq.↔→≃
          (Σ-map to id)
          (Σ-map from (g _))
          p
          (λ (x , y) →
             Σ-≡,≡→≡ (left-inverse-of _)
               (subst (P ∘ to) (left-inverse-of x) (g _ y)     ≡⟨ subst-∘ _ _ _ ⟩
                subst P (cong to (left-inverse-of x)) (g _ y)  ≡⟨ cong (λ eq → subst P eq _) (left-right-lemma x) ⟩
                subst P (right-inverse-of (to x)) (g _ y)      ≡⟨ q _ ⟩∎
                y                                              ∎))
    where
    open Σ-cong-id-proofs

private

  -- Used to implement Σ-cong-id.
  --
  -- The constructed term is returned.

  Σ-cong-id-tactic :
    Σ-cong-id-proofs k A B P →
    A ≃ B → Term → TC Term
  Σ-cong-id-tactic proofs A≃B goal = do
    refl₁       ← quoteTC (Σ-cong-id-proofs.refl₁       proofs)
    subst-refl₂ ← quoteTC (Σ-cong-id-proofs.subst-refl₂ proofs A≃B)
    proofs      ← quoteTC proofs
    A≃B         ← quoteTC A≃B
    let t = def (quote Σ-cong-id-proofs.→↝)
                (varg proofs ∷
                 varg A≃B ∷
                 varg (lam visible $ abs "_" $
                       lam visible $ abs "x" $
                       var 0 []) ∷
                 varg refl₁ ∷
                 varg subst-refl₂ ∷
                 [])
    unify goal t
    return t

macro

  -- A macro that tries to prove
  -- Σ A (P ∘ from-isomorphism eq) ↝[ k₂ ] Σ B P, given that there is
  -- a proof eq : A ↔[ k₁ ] B for which the "right inverse of" proof
  -- is definitionally equal to reflexivity. If k₂ is surjection,
  -- bijection or equivalence, then the "right inverse of" component
  -- of the resulting proof is reflexivity.

  Σ-cong-id :
    ⦃ proofs : Σ-cong-id-proofs k₂ A B P ⦄ →
    A ↔[ k₁ ] B → Term → TC ⊤
  Σ-cong-id ⦃ proofs = proofs ⦄ A↝B goal = do
    Σ-cong-id-tactic proofs (from-isomorphism A↝B) goal
    return _

private

  -- Some unit tests.

  t₄ : (A × A) ↔ (A × A)
  t₄ = Σ-cong-id B.id

  _ : _↔_.to t₄ p ≡ p
  _ = refl _

  _ : _↔_.from t₄ p ≡ p
  _ = refl _

  _ :
    {p : A × A} →
    _↔_.right-inverse-of t₄ p ≡ refl _
  _ = refl _

  t₅ : (∃ λ (x : ⊥₀ ⊎ A) → _↔_.to ⊎-left-identity x ≡ y) ≃
       (∃ λ (x : A) → x ≡ y)
  t₅ = Σ-cong-id ⊎-left-identity

  _ : _≃_.to t₅ (inj₂ x , p) ≡ (x , p)
  _ = refl _

  _ : _≃_.from t₅ p ≡ Σ-map inj₂ id p
  _ = refl _

  _ :
    {p : ∃ λ (x : A) → x ≡ y} →
    _≃_.right-inverse-of t₅ p ≡ refl _
  _ = refl _

  -- The following proof—implemented using Σ-cong—is, at the time of
  -- writing, "worse".

  t₅′ : (∃ λ (x : ⊥₀ ⊎ A) → _↔_.to ⊎-left-identity x ≡ y) ≃
        (∃ λ (x : A) → x ≡ y)
  t₅′ = Eq.↔⇒≃ $ Σ-cong ⊎-left-identity λ _ → F.id

  _ : _≃_.to t₅′ (inj₂ x , p) ≡ (x , p)
  _ = refl _

  _ : _≃_.from t₅′ p ≡
      Σ-map inj₂ (subst (_≡ y) (sym (refl _))) p
  _ = refl _

------------------------------------------------------------------------
-- Σ-cong-id-↠

-- Building blocks used to construct the proofs in Σ-cong-id-↠.

record Σ-cong-id-↠-proofs
         (A : Type a) (B : Type b) (P : B → Type p) :
         Type (lsuc (a ⊔ b ⊔ p)) where
  field
    refl₁ : (x : Σ B P) → x ≡ x

    →↠ :
      (A↠B : A ↠ B)
      (g : ∀ x → P x → P (_↠_.to A↠B (_↠_.from A↠B x))) →
      ((p : Σ B P) →
       Σ-map (_↠_.to A↠B) id (Σ-map (_↠_.from A↠B) (g _) p) ≡ p) →
      Σ A (P ∘ _↠_.to A↠B) ↠ Σ B P

instance

  -- The building blocks can be proved.

  instance-of-Σ-cong-id-↠-proofs : Σ-cong-id-↠-proofs A B P
  instance-of-Σ-cong-id-↠-proofs {P = P} = λ where
      .refl₁      → refl
      .→↠ A↠B g p → record
        { logical-equivalence = record
          { to   = Σ-map (_↠_.to   A↠B) id
          ; from = Σ-map (_↠_.from A↠B) (g _)
          }
        ; right-inverse-of = p
        }
    where
    open Σ-cong-id-↠-proofs

private

  -- Used to implement Σ-cong-id-↠.
  --
  -- The constructed term is returned.

  Σ-cong-id-↠-tactic :
    Σ-cong-id-↠-proofs A B P →
    A ↠ B → Term → TC Term
  Σ-cong-id-↠-tactic proofs A↠B goal = do
    refl₁  ← quoteTC (Σ-cong-id-↠-proofs.refl₁ proofs)
    proofs ← quoteTC proofs
    A↠B    ← quoteTC A↠B
    let t = def (quote Σ-cong-id-↠-proofs.→↠)
                (varg proofs ∷
                 varg A↠B ∷
                 varg (lam visible $ abs "_" $
                       lam visible $ abs "x" $
                       var 0 []) ∷
                 varg refl₁ ∷
                 [])
    unify goal t
    return t

macro

  -- A macro that tries to prove Σ A (P ∘ _↠_.to eq) ↠ Σ B P, given a
  -- proof eq for which _↠_.to eq ∘ _↠_.from eq is definitionally
  -- equal to the identity function. The right-inverse-of component of
  -- the resulting proof is reflexivity.

  Σ-cong-id-↠ :
    ⦃ proofs : Σ-cong-id-↠-proofs A B P ⦄ →
    A ↠ B → Term → TC ⊤
  Σ-cong-id-↠ ⦃ proofs = proofs ⦄ A↠B goal = do
    Σ-cong-id-↠-tactic proofs A↠B goal
    return _

private

  -- Some unit tests.

  t₆ : (A × A) ↠ (A × A)
  t₆ = Σ-cong-id-↠ S.id

  _ : _↠_.to t₆ p ≡ p
  _ = refl _

  _ : _↠_.from t₆ p ≡ p
  _ = refl _

  _ :
    {p : A × A} →
    _↠_.right-inverse-of t₆ p ≡ refl _
  _ = refl _

  t₇ :
    (∃ λ (f : (x : A ⊎ B) → P x) → (f ∘ inj₁ , f ∘ inj₂) ≡ q) ↠
    (∃ λ (p : ((x : A) → P (inj₁ x)) ×
              ((y : B) → P (inj₂ y))) →
       p ≡ q)
  t₇ = Σ-cong-id-↠ Π⊎↠Π×Π

  _ : _↠_.to t₇ (f , p) ≡ ((f ∘ inj₁ , f ∘ inj₂) , p)
  _ = refl _

  _ : _↠_.from t₇ ((f , g) , p) ≡ ([ f , g ] , p)
  _ = refl _

  _ :
    ∀ {P : A ⊎ B → Type p} {q}
      {p : ∃ λ (p : ((x : A) → P (inj₁ x)) ×
                    ((y : B) → P (inj₂ y))) →
             p ≡ q} →
    _↠_.right-inverse-of (t₇ {P = P}) p ≡ refl p
  _ = refl _

  -- The following proof—implemented using S.Σ-cong—is, at the time of
  -- writing, "worse".

  t₇′ :
    (∃ λ (f : (x : A ⊎ B) → P x) → (f ∘ inj₁ , f ∘ inj₂) ≡ q) ↠
    (∃ λ (p : ((x : A) → P (inj₁ x)) ×
              ((y : B) → P (inj₂ y))) →
       p ≡ q)
  t₇′ = S.Σ-cong Π⊎↠Π×Π λ _ → F.id

  _ : _↠_.to t₇′ (f , p) ≡ ((f ∘ inj₁ , f ∘ inj₂) , p)
  _ = refl _

  _ : _↠_.from t₇′ ((f , g) , p) ≡
      ([ f , g ] , subst (_≡ q) (sym (refl _)) p)
  _ = refl _

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module #3 where

open import Relation.Binary.PropositionalEquality

{-
  Exercise 2.3 Give a fourth, different, proof of Lemma 2.1.2, and prove that it is equal to the others.
-}

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

-- Uses based path induction
composite''' : ∀ {i} {A : Set i}{x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
composite''' {i} {A} {x}{y}{_} p = based-ind₌ D d where
  D : (z : A) → (q : y ≡ z) → Set i
  D z _ = x ≡ z

  d : D _ refl
  d = p

ext: agda

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
module plfa-code.Isomorphism where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; cong-app)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm)

_∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
(g ∘ f) x  =  g (f x)

_∘′_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
g ∘′ f = λ x → g (f x)

postulate
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

_+′_ : ℕ → ℕ → ℕ
m +′ zero  = m
m +′ suc n = suc (m +′ n)

same-app : ∀ (m n : ℕ) → m +′ n ≡ m + n
same-app m n rewrite +-comm m n = helper m n
  where
  helper : ∀ (m n : ℕ) → m +′ n ≡ n + m
  helper m zero    = refl
  helper m (suc n) = cong suc (helper m n)

same : _+′_ ≡ _+_
same = extensionality (λ m → extensionality (λ n → same-app m n))

infix 0 _≃_
record _≃_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_

-- equal to
data _≃′_ (A B : Set): Set where
  mk-≃′ : ∀ (to : A → B) →
          ∀ (from : B → A) →
          ∀ (from∘to : (∀ (x : A) → from (to x) ≡ x)) →
          ∀ (to∘from : (∀ (y : B) → to (from y) ≡ y)) →
          A ≃′ B

to′ : ∀ {A B : Set} → (A ≃′ B) → (A → B)
to′ (mk-≃′ f g g∘f f∘g) = f

from′ : ∀ {A B : Set} → (A ≃′ B) → (B → A)
from′ (mk-≃′ f g g∘f f∘g) = g

from∘to′ : ∀ {A B : Set} → (A≃B : A ≃′ B) → (∀ (x : A) → from′ A≃B (to′ A≃B x) ≡ x)
from∘to′ (mk-≃′ f g g∘f f∘g) = g∘f

to∘from′ : ∀ {A B : Set} → (A≃B : A ≃′ B) → (∀ (y : B) → to′ A≃B (from′ A≃B y) ≡ y)
to∘from′ (mk-≃′ f g g∘f f∘g) = f∘g
-- which means `field record` will take the field

≃-refl : ∀ {A : Set}
    -----
  → A ≃ A
≃-refl =
  record
    { to = λ{x → x}
    ; from = λ{y → y}
    ; from∘to = λ{x → refl}
    ; to∘from = λ{y → refl}
    }

≃-sym : ∀ {A B : Set}
  → A ≃ B
    -----
  → B ≃ A
≃-sym A≃B =
  record
    { to = from A≃B
    ; from = to A≃B
    ; from∘to = to∘from A≃B
    ; to∘from = from∘to A≃B
    }

≃-trans : ∀ {A B C : Set}
  → A ≃ B
  → B ≃ C
    -----
  → A ≃ C
≃-trans A≃B B≃C =
  record
    { to      =   to   B≃C ∘ to   A≃B
    ; from    =   from A≃B ∘ from B≃C
    ; from∘to = λ{x →
      begin
        (from A≃B ∘ from B≃C) ((to B≃C ∘ to A≃B) x)
      ≡⟨⟩
        from A≃B (from B≃C (to B≃C (to A≃B x)))
      ≡⟨ cong (from A≃B) (from∘to B≃C (to A≃B x)) ⟩
        from A≃B (to A≃B x)
      ≡⟨ from∘to A≃B x ⟩
        x
      ∎
      }
    ; to∘from = λ{y →
        begin
          (to B≃C ∘ to A≃B) ((from A≃B ∘ from B≃C) y)
        ≡⟨⟩
          to B≃C (to A≃B (from A≃B (from B≃C y)))
        ≡⟨ cong (to B≃C) (to∘from A≃B (from B≃C y)) ⟩
          to B≃C (from B≃C y)
        ≡⟨ to∘from B≃C y ⟩
          y
        ∎}
    }

module ≃-Reasoning where

  infix  1 ≃-begin_
  infixr 2 _≃⟨_⟩_
  infix  3 _≃-∎

  ≃-begin_ : ∀ {A B : Set}
    → A ≃ B
      -----
    → A ≃ B
  ≃-begin A≃B = A≃B

  _≃⟨_⟩_ : ∀ (A : Set) {B C : Set}
    → A ≃ B
    → B ≃ C
      -----
    → A ≃ C
  A ≃⟨ A≃B ⟩ B≃C = ≃-trans A≃B B≃C

  _≃-∎ : ∀ (A : Set)
      -----
    → A ≃ A
  A ≃-∎ = ≃-refl

open ≃-Reasoning

infix 0 _≲_
record _≲_ (A B : Set) : Set where
  field
    to      : A → B
    from    : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
open _≲_

≲-refl : ∀ {A : Set} → A ≲ A
≲-refl =
  record
    { to      = λ{x → x}
    ; from    = λ{y → y}
    ; from∘to = λ{x → refl}
    }

≲-trans : ∀ {A B C : Set} → A ≲ B → B ≲ C → A ≲ C
≲-trans A≲B B≲C =
  record
    { to      = λ{x → to   B≲C (to   A≲B x)}
    ; from    = λ{y → from A≲B (from B≲C y)}
    ; from∘to = λ{x →
        begin
          from A≲B (from B≲C (to B≲C (to A≲B x)))
        ≡⟨ cong (from A≲B) (from∘to B≲C (to A≲B x)) ⟩
          from A≲B (to A≲B x)
        ≡⟨ from∘to A≲B x ⟩
          x
        ∎}
     }

≲-antisym : ∀ {A B : Set}
  → (A≲B : A ≲ B)
  → (B≲A : B ≲ A)
  → (to A≲B ≡ from B≲A)
  → (from A≲B ≡ to B≲A)
    -------------------
  → A ≃ B
≲-antisym A≲B B≲A to≡from from≡to =
  record
  { to      = to A≲B
  ; from    = from A≲B
  ; from∘to = from∘to A≲B
  ; to∘from = λ{y →
      begin
        to A≲B (from A≲B y)
      ≡⟨ cong (to A≲B) (cong-app from≡to y) ⟩
        to A≲B (to B≲A y)
      ≡⟨ cong-app to≡from (to B≲A y) ⟩
        from B≲A (to B≲A y)
      ≡⟨ from∘to B≲A y ⟩
        y
      ∎
    }
  }

module ≲-Reasoning where

  infix  1 ≲-begin_
  infixr 2 _≲⟨_⟩_
  infix  3 _≲-∎

  ≲-begin_ : ∀ {A B : Set}
    → A ≲ B
      -----
    → A ≲ B
  ≲-begin A≲B = A≲B

  _≲⟨_⟩_ : ∀ (A : Set) {B C : Set}
    → A ≲ B
    → B ≲ C
      -----
    → A ≲ C
  A ≲⟨ A≲B ⟩ B≲C = ≲-trans A≲B B≲C

  _≲-∎ : ∀ (A : Set)
      -----
    → A ≲ A
  A ≲-∎ = ≲-refl

open ≲-Reasoning

---------- practice ----------

≃-implies-≲ : ∀ {A B : Set}
  → A ≃ B
    -----
  → A ≲ B

≃-implies-≲ A≃B =
  record
  { to = to A≃B
  ; from = from A≃B
  ; from∘to = from∘to A≃B
  }

record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A

open _⇔_

⇔-refl : ∀ {A : Set} → A ⇔ A
⇔-refl = record { to = λ z → z ; from = λ z → z }

⇔-sym : ∀ {A B : Set} → A ⇔ B → B ⇔ A
⇔-sym A⇔B = record { to = from A⇔B ; from = to A⇔B }

⇔-trans : ∀ {A B C : Set} → A ⇔ B → B ⇔ C → A ⇔ C
⇔-trans A⇔B B⇔C =
  record
    { to   = to B⇔C ∘ to A⇔B
    ; from = from A⇔B ∘ from B⇔C
    }

data Bin : Set where
  nil : Bin
  x0_ : Bin → Bin
  x1_ : Bin → Bin

postulate
  toB : ℕ → Bin
  fromB : Bin → ℕ
  from-to-const : ∀ (n : ℕ) → fromB (toB n) ≡ n

ℕ-embedding-Bin : ℕ ≲ Bin
ℕ-embedding-Bin =
  record
    { to      = toB
    ; from    = fromB
    ; from∘to = from-to-const
    }

max_stars_repo_name: chirsz-ever/plfa-code

max_issues_repo_name: chirsz-ever/plfa-code

max_forks_repo_name: chirsz-ever/plfa-code


text:
module Base where
open import Relation.Binary.PropositionalEquality

is-prop : Set → Set
is-prop X = (x y : X) → x ≡ y

_∼_ : {A B : Set} → (f g : A → B) → Set
f ∼ g = ∀ a → f a ≡ g a


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

open import Fragment.Algebra.Signature

module Fragment.Algebra.Free (Σ : Signature) where

open import Fragment.Algebra.Free.Base Σ public
open import Fragment.Algebra.Free.Properties Σ public
open import Fragment.Algebra.Free.Monad Σ public
open import Fragment.Algebra.Free.Evaluation Σ public

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
{-

Half adjoint equivalences ([HAEquiv])

- Iso to HAEquiv ([iso→HAEquiv])
- Equiv to HAEquiv ([equiv→HAEquiv])
- Cong is an equivalence ([congEquiv])

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.HAEquiv where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.GroupoidLaws

open import Cubical.Data.Nat

record isHAEquiv {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) : Type (ℓ-max ℓ ℓ') where
  field
    g : B → A
    sec : ∀ a → g (f a) ≡ a
    ret : ∀ b → f (g b) ≡ b
    com : ∀ a → cong f (sec a) ≡ ret (f a)

  -- from redtt's ha-equiv/symm
  com-op : ∀ b → cong g (ret b) ≡ sec (g b)
  com-op b j i = hcomp (λ k → λ { (i = i0) → sec (g b) (j ∧ (~ k))
                                ; (j = i0) → g (ret b i)
                                ; (j = i1) → sec (g b) (i ∨ (~ k))
                                ; (i = i1) → g b })
                       (cap1 j i)

    where cap0 : Square {- (i = i0) -} (λ j → f (sec (g b) j))
                        {- (j = i0) -} (λ i → f (g (ret b i)))
                        {- (j = i1) -} (λ i → ret b i)
                        {- (i = i1) -} (λ j → ret b j)

          cap0 j i = hcomp (λ k → λ { (i = i0) → com (g b) (~ k) j
                                    ; (j = i0) → f (g (ret b i))
                                    ; (j = i1) → ret b i
                                    ; (i = i1) → ret b j })
                           (ret (ret b i) j)

          filler : I → I → A
          filler j i = hfill (λ k → λ { (i = i0) → g (ret b k)
                                      ; (i = i1) → g b })
                             (inS (sec (g b) i)) j

          cap1 : Square {- (i = i0) -} (λ j → sec (g b) j)
                        {- (j = i0) -} (λ i → g (ret b i))
                        {- (j = i1) -} (λ i → g b)
                        {- (i = i1) -} (λ j → g b)

          cap1 j i = hcomp (λ k → λ { (i = i0) → sec (sec (g b) j) k
                                    ; (j = i0) → sec (g (ret b i)) k
                                    ; (j = i1) → filler i k
                                    ; (i = i1) → filler j k })
                           (g (cap0 j i))

HAEquiv : ∀ {ℓ ℓ'} (A : Type ℓ) (B : Type ℓ') → Type (ℓ-max ℓ ℓ')
HAEquiv A B = Σ (A → B) λ f → isHAEquiv f

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ
    B : Type ℓ'

iso→HAEquiv : Iso A B → HAEquiv A B
iso→HAEquiv {A = A} {B = B} (iso f g ε η) = f , (record { g = g ; sec = η ; ret = ret ; com = com })
  where
    sides : ∀ b i j → Partial (~ i ∨ i) B
    sides b i j = λ { (i = i0) → ε (f (g b)) j
                    ; (i = i1) → ε b j }

    bot : ∀ b i → B
    bot b i = cong f (η (g b)) i

    ret : (b : B) → f (g b) ≡ b
    ret b i = hcomp (sides b i) (bot b i)

    com : (a : A) → cong f (η a) ≡ ret (f a)
    com a i j = hcomp (λ k → λ { (i = i0) → ε (f (η a j)) k
                               ; (i = i1) → hfill (sides (f a) j) (inS (bot (f a) j)) k
                               ; (j = i0) → ε (f (g (f a))) k
                               ; (j = i1) → ε (f a) k})
                      (cong (cong f) (sym (Hfa≡fHa (λ x → g (f x)) η a)) i j)

equiv→HAEquiv : A ≃ B → HAEquiv A B
equiv→HAEquiv e = iso→HAEquiv (equivToIso e)

congEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {x y : A} (e : A ≃ B) → (x ≡ y) ≃ (e .fst x ≡ e .fst y)
congEquiv {A = A} {B} {x} {y} e = isoToEquiv (iso intro elim intro-elim elim-intro)
  where
    e' : HAEquiv A B
    e' = equiv→HAEquiv e

    f : A → B
    f = e' .fst

    g : B → A
    g = isHAEquiv.g (e' .snd)

    sec : ∀ a → g (f a) ≡ a
    sec = isHAEquiv.sec (e' .snd)

    ret : ∀ b → f (g b) ≡ b
    ret = isHAEquiv.ret (e' .snd)

    com : ∀ a → cong f (sec a) ≡ ret (f a)
    com = isHAEquiv.com (e' .snd)

    intro : x ≡ y → f x ≡ f y
    intro = cong f

    elim-sides : ∀ p i j → Partial (~ i ∨ i) A
    elim-sides p i j = λ { (i = i0) → sec x j
                         ; (i = i1) → sec y j }

    elim-bot : ∀ p i → A
    elim-bot p i = cong g p i

    elim : f x ≡ f y → x ≡ y
    elim p i = hcomp (elim-sides p i) (elim-bot p i)

    intro-elim : ∀ p → intro (elim p) ≡ p
    intro-elim p i j =
      hcomp (λ k → λ { (i = i0) → f (hfill (elim-sides p j)
                                    (inS (elim-bot p j)) k)
                     ; (i = i1) → ret (p j) k
                     ; (j = i0) → com x i k
                     ; (j = i1) → com y i k })
            (f (g (p j)))

    elim-intro : ∀ p → elim (intro p) ≡ p
    elim-intro p i j =
      hcomp (λ k → λ { (i = i0) → hfill (λ l → λ { (j = i0) → secEq e x l
                                                 ; (j = i1) → secEq e y l })
                                        (inS (cong (λ z → g (f z)) p j)) k
                     ; (i = i1) → p j
                     ; (j = i0) → secEq e x (i ∨ k)
                     ; (j = i1) → secEq e y (i ∨ k) })
            (secEq e (p j) i)

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
module monad-instances where
open import lib
open import general-util

instance
  IO-monad : monad IO
  IO-monad = record {returnM = return; bindM = _>>=_}

instance
  id-monad : monad id
  id-monad = record {returnM = id; bindM = λ a f → f a}

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
{-# OPTIONS --cubical --safe #-}

module Relation.Nullary.Discrete where

open import Relation.Nullary.Discrete.Base public

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
{-# OPTIONS --cubical-compatible #-}

module Issue712 where

data _≡_ {A : Set} : A → A → Set where
  refl : (x : A) → x ≡ x

record _×_ (A B : Set) : Set where
  field
    p1 : A
    p2 : B
open _×_

lemma : {A B : Set} {u v : A × B} (p : u ≡ v) → p1 u ≡ p1 v
lemma (refl _) = refl _


text:
data ⊥ : Set where

_ : @0 ⊥ → Set
_ = λ @0 { () }

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Zero-cost coercion to cross the FFI boundary
------------------------------------------------------------------------

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

module Foreign.Haskell.Coerce where

------------------------------------------------------------------------
-- Motivation

-- Problem: No COMPILE directives for common inductive types

-- In order to guarantee that the vast majority of the libary is
-- considered safe by Agda, we had to remove the COMPILE pragmas
-- associated to common inductive types.
-- These directives cannot possibly be checked by the compiler and
-- the user could define unsound mappings (e.g. swapping Bool's
-- true and false).

-- Solution: Essentially identical definitions + zero-cost coercions

-- To solve this problem, we have introduced a number of essentially
-- identical definitions in the Foreign.Haskell.* modules. However
-- converting back and forth between the FFI-friendly type and its
-- safe counterpart would take linear time.
-- This module defines zero cost coercions between these types.

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

open import Level using (Level; _⊔_)
open import Agda.Builtin.Nat
open import Agda.Builtin.Int

import IO.Primitive    as STD
import Data.List.Base  as STD
import Data.Maybe.Base as STD
import Data.Product    as STD
import Data.Sum        as STD

import Foreign.Haskell.Maybe  as FFI
import Foreign.Haskell.Pair   as FFI
import Foreign.Haskell.Either as FFI

private
  variable
    a b c d e f : Level
    A : Set a
    B : Set b
    C : Set c
    D : Set d

-- We define a simple indexed datatype `Coercible`. A value of `Coercible A B`
-- is a proof that ̀A` and `B` have the same underlying runtime representation.
-- The only possible proof is an incantation from the implementer begging to
-- be trusted.

-- We need this type to be concrete so that overlapping instances can be checked
-- for equality: we do not care what proof we get as long as we get one.

-- We need for it to be a data type rather than a record type so that Agda does
-- not mistakenly build arbitrary instances by η-expansion.

data Coercible (A : Set a) (B : Set b) : Set where
  TrustMe : Coercible A B

{-# FOREIGN GHC data AgdaCoercible l1 l2 a b = TrustMe #-}
{-# COMPILE GHC Coercible = data AgdaCoercible (TrustMe) #-}

-- Once we get our hands on a proof that `Coercible A B` we postulate that it
-- is safe to convert an `A` into a `B`. This is done under the hood by using
-- `unsafeCoerce`.

postulate coerce : {{_ : Coercible A B}} → A → B

{-# FOREIGN GHC import Unsafe.Coerce #-}
{-# COMPILE GHC coerce = \ _ _ _ _ _ -> unsafeCoerce #-}

------------------------------------------------------------------------
-- Unary and binary variants for covariant type constructors

Coercible₁ : ∀ a c → (T : Set a → Set b) (U : Set c → Set d) → Set _
Coercible₁ _ _ T U = ∀ {A B} → {{_ : Coercible A B}} → Coercible (T A) (U B)

Coercible₂ : ∀ a b d e → (T : Set a → Set b → Set c) (U : Set d → Set e → Set f) → Set _
Coercible₂ _ _ _ _ T U = ∀ {A B} → {{_ : Coercible A B}} → Coercible₁ _ _ (T A) (U B)

------------------------------------------------------------------------
-- Instances

-- Nat

-- Our first instance reveals one of Agda's secrets: natural numbers are
-- represented by (arbitrary precision) integers at runtime! Note that we
-- may only coerce in one direction: arbitrary integers may actually be
-- negative and will not do as mere natural numbers.

instance

  nat-toInt : Coercible Nat Int
  nat-toInt = TrustMe

-- We then proceed to state that data types from the standard library
-- can be converted to their FFI equivalents which are bound to actual
-- Haskell types.

-- Maybe

  maybe-toFFI : Coercible₁ a b STD.Maybe FFI.Maybe
  maybe-toFFI = TrustMe

  maybe-fromFFI : Coercible₁ a b FFI.Maybe STD.Maybe
  maybe-fromFFI = TrustMe

-- Product

  pair-toFFI : Coercible₂ a b c d STD._×_ FFI.Pair
  pair-toFFI = TrustMe

  pair-fromFFI : Coercible₂ a b c d FFI.Pair STD._×_
  pair-fromFFI = TrustMe

-- Sum

  either-toFFI : Coercible₂ a b c d STD._⊎_ FFI.Either
  either-toFFI = TrustMe

  either-fromFFI : Coercible₂ a b c d FFI.Either STD._⊎_
  either-fromFFI = TrustMe

-- We follow up with purely structural rules for builtin data types which
-- already have known low-level representations.

-- List

  coerce-list : Coercible₁ a b STD.List STD.List
  coerce-list = TrustMe

-- IO

  coerce-IO : Coercible₁ a b STD.IO STD.IO
  coerce-IO = TrustMe

-- Function
-- Note that functions are contravariant in their domain.

  coerce-fun : {{_ : Coercible A B}} → Coercible₁ c d (λ C → B → C) (λ D → A → D)
  coerce-fun = TrustMe

-- Finally we add a reflexivity proof to discharge all the dangling constraints
-- involving type variables and concrete builtin types such as `Bool`.

-- This rule overlaps with the purely structural ones: when attempting to prove
-- `Coercible (List A) (List A)`, should Agda use the proof obtained by `coerce-refl`
-- or the one obtained by `coerce-list coerce-refl`? Because we are using a
-- datatype with a single constructor these distinctions do not matter: both proofs
-- are definitionally equal.

  coerce-refl : Coercible A A
  coerce-refl = TrustMe


text:
------------------------------------------------------------------------------
-- The gcd program is correct
------------------------------------------------------------------------------

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

-- This module proves the correctness of the gcd program using
-- the Euclid's algorithm.

module FOTC.Program.GCD.Total.CorrectnessProofI where

open import FOTC.Base
open import FOTC.Data.Nat.Type
open import FOTC.Program.GCD.Total.CommonDivisorI using ( gcdCD )
open import FOTC.Program.GCD.Total.Definitions using ( gcdSpec )
open import FOTC.Program.GCD.Total.DivisibleI using ( gcdDivisible )
open import FOTC.Program.GCD.Total.GCD using ( gcd )

------------------------------------------------------------------------------
-- The gcd is correct.
gcdCorrect : ∀ {m n} → N m → N n → gcdSpec m n (gcd m n)
gcdCorrect Nm Nn = gcdCD Nm Nn , gcdDivisible Nm Nn

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Basic types related to coinduction
------------------------------------------------------------------------

module Coinduction where

import Level

------------------------------------------------------------------------
-- A type used to make recursive arguments coinductive

infix 1000 ♯_

postulate
  ∞  : ∀ {a} (A : Set a) → Set a
  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
  ♭  : ∀ {a} {A : Set a} → ∞ A → A

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

------------------------------------------------------------------------
-- Rec, a type which is analogous to the Rec type constructor used in
-- ΠΣ (see Altenkirch, Danielsson, Löh and Oury. ΠΣ: Dependent Types
-- without the Sugar. FLOPS 2010, LNCS 6009.)

data Rec {a} (A : ∞ (Set a)) : Set a where
  fold : (x : ♭ A) → Rec A

unfold : ∀ {a} {A : ∞ (Set a)} → Rec A → ♭ A
unfold (fold x) = x

{-

  -- If --guardedness-preserving-type-constructors is enabled one can
  -- define types like ℕ by recursion:

  open import Data.Sum
  open import Data.Unit

  ℕ : Set
  ℕ = ⊤ ⊎ Rec (♯ ℕ)

  zero : ℕ
  zero = inj₁ _

  suc : ℕ → ℕ
  suc n = inj₂ (fold n)

  ℕ-rec : (P : ℕ → Set) →
          P zero →
          (∀ n → P n → P (suc n)) →
          ∀ n → P n
  ℕ-rec P z s (inj₁ _)        = z
  ℕ-rec P z s (inj₂ (fold n)) = s n (ℕ-rec P z s n)

  -- This feature is very experimental, though: it may lead to
  -- inconsistencies.

-}


text:
module tree-test where

open import tree
open import nat
open import bool
open import bool-to-string
open import list

test-tree = node 2 ( (leaf 3) :: (node 4 ( (leaf 5) :: (leaf 7) :: [] )) :: (leaf 6) :: (leaf 7) :: [])

perfect3 = perfect-binary-tree 3 tt

perfect3-string = 𝕋-to-string 𝔹-to-string perfect3

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


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

open import lib.Basics
open import lib.types.Bool
open import lib.types.Coproduct
open import lib.types.Paths
open import lib.types.Span
open import lib.types.Pushout
open import lib.types.Cofiber
open import lib.types.Sigma
open import lib.types.Wedge

module lib.types.Smash {i j} where

module _ (X : Ptd i) (Y : Ptd j) where

  ⊙∧-span : ⊙Span
  ⊙∧-span = ⊙span (X ⊙× Y) ⊙Bool (X ⊙⊔ Y)
    (⊔-rec (_, pt Y) (pt X ,_) , idp)
    (⊙⊔-fmap {Y = Y} ⊙cst ⊙cst)

  ∧-span : Span
  ∧-span = ⊙Span-to-Span ⊙∧-span

  _∧_ = Pushout ∧-span
  _⊙∧_ = ⊙Pushout ⊙∧-span
  Smash = _∧_
  ⊙Smash = _⊙∧_

module _ {X : Ptd i} {Y : Ptd j} where

  smin : de⊙ X → de⊙ Y → Smash X Y
  smin x y = left (x , y)

  smbasel : Smash X Y
  smbasel = right true

  smbaser : Smash X Y
  smbaser = right false

  smgluel : (x : de⊙ X) → smin x (pt Y) == smbasel
  smgluel x = glue (inl x)

  smgluer : (y : de⊙ Y) → smin (pt X) y == smbaser
  smgluer y = glue (inr y)

  module SmashElim {k} {P : Smash X Y → Type k}
    (smin* : (x : de⊙ X) (y : de⊙ Y) → P (smin x y))
    (smbasel* : P smbasel) (smbaser* : P smbaser)
    (smgluel* : (x : de⊙ X) → smin* x (pt Y) == smbasel* [ P ↓ smgluel x ])
    (smgluer* : (y : de⊙ Y) → smin* (pt X) y == smbaser* [ P ↓ smgluer y ]) where

    private
      module M = PushoutElim
        (uncurry smin*)
        (Coprod-elim (λ _ → smbasel*) (λ _ → smbaser*))
        (Coprod-elim smgluel* smgluer*)
    f = M.f
    smgluel-β = M.glue-β ∘ inl
    smgluer-β = M.glue-β ∘ inr

  Smash-elim = SmashElim.f

  module SmashRec {k} {C : Type k}
    (smin* : (x : de⊙ X) (y : de⊙ Y) → C)
    (smbasel* smbaser* : C)
    (smgluel* : (x : de⊙ X) → smin* x (pt Y) == smbasel*)
    (smgluer* : (y : de⊙ Y) → smin* (pt X) y == smbaser*) where

    private
      module M = PushoutRec {d = ∧-span X Y}
        (uncurry smin*)
        (Coprod-rec (λ _ → smbasel*) (λ _ → smbaser*))
        (Coprod-elim smgluel* smgluer*)
    f = M.f
    smgluel-β = M.glue-β ∘ inl
    smgluer-β = M.glue-β ∘ inr

  Smash-rec = SmashRec.f

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude

private
  variable
    ℓ ℓ' ℓ'' : Level
    S : Type ℓ → Type ℓ'

-- A structure is a type-family S : Type ℓ → Type ℓ', i.e. for X : Type ℓ and s : S X,
-- the pair (X , s) : TypeWithStr ℓ S means that X is equipped with a S-structure, witnessed by s.

TypeWithStr : (ℓ : Level) (S : Type ℓ → Type ℓ') → Type (ℓ-max (ℓ-suc ℓ) ℓ')
TypeWithStr ℓ S = Σ[ X ∈ Type ℓ ] S X

typ : TypeWithStr ℓ S → Type ℓ
typ = fst

str : (A : TypeWithStr ℓ S) → S (typ A)
str = snd

-- Alternative notation for typ
⟨_⟩ : TypeWithStr ℓ S → Type ℓ
⟨_⟩ = typ

-- An S-structure should have a notion of S-homomorphism, or rather S-isomorphism.
-- This will be implemented by a function ι : StrEquiv S ℓ'
-- that gives us for any two types with S-structure (X , s) and (Y , t) a family:
--    ι (X , s) (Y , t) : (X ≃ Y) → Type ℓ''
StrEquiv : (S : Type ℓ → Type ℓ'') (ℓ' : Level) → Type (ℓ-max (ℓ-suc (ℓ-max ℓ ℓ')) ℓ'')
StrEquiv {ℓ} S ℓ' = (A B : TypeWithStr ℓ S) → typ A ≃ typ B → Type ℓ'

-- An S-structure may instead be equipped with an action on equivalences, which will
-- induce a notion of S-homomorphism

EquivAction : (S : Type ℓ → Type ℓ'') → Type (ℓ-max (ℓ-suc ℓ) ℓ'')
EquivAction {ℓ} S = {X Y : Type ℓ} → X ≃ Y → S X ≃ S Y

EquivAction→StrEquiv : {S : Type ℓ → Type ℓ''}
  → EquivAction S → StrEquiv S ℓ''
EquivAction→StrEquiv α (X , s) (Y , t) e = equivFun (α e) s ≡ t

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{-# OPTIONS --type-in-type #-}

open import Agda.Primitive

test : Set
test = Setω

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Oscar.Prelude
open import Oscar.Class

module Oscar.Class.Transitivity where

module Transitivity'
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  x y z
  = ℭLASS (x ,, y ,, z ,, _∼_) (x ∼ y → y ∼ z → x ∼ z)

module Transitivity
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  where
  class = ∀ {x y z} → Transitivity'.class _∼_ x y z
  type = ∀ {x y z} → Transitivity'.type _∼_ x y z
  method : ⦃ _ : class ⦄ → type
  method {x = x} {y} {z} = Transitivity'.method _∼_ x y z

module _
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} {_∼_ : 𝔒 → 𝔒 → Ø 𝔯}
  where
  transitivity = Transitivity.method _∼_

module _
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  ⦃ _ : Transitivity.class _∼_ ⦄
  where
  transitivity[_] = λ {x y z} (x∼y : x ∼ y) (y∼z : y ∼ z) → Transitivity.method _∼_ x∼y y∼z
  infixr 9 ∙[]-syntax
  ∙[]-syntax = transitivity[_]
  syntax ∙[]-syntax _⊸_ f g = g ∙[ _⊸_ ] f

module FlipTransitivity
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  where
  class = Transitivity.class _∼_
  type = ∀ {x y z} → y ∼ z → x ∼ y → x ∼ z
  method : ⦃ _ : class ⦄ → type
  method = flip transitivity

module _
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} {_∼_ : 𝔒 → 𝔒 → Ø 𝔯}
  ⦃ _ : Transitivity.class _∼_ ⦄
  where
  infixr 9 _∙_
  _∙_ : ∀ {x y z} (y∼z : y ∼ z) (x∼y : x ∼ y) → x ∼ z
  g ∙ f = transitivity f g

module _
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔭} {𝔓 : 𝔒 → Ø 𝔭}
  where

  open import Oscar.Data.Proposequality

  ≡̇-transitivity = transitivity[ Proposextensequality⟦ 𝔓 ⟧ ]

  infixr 9 ≡̇-transitivity
  syntax ≡̇-transitivity f g = g ≡̇-∙ f

  infixr 9 ≡̇-transitivity-syntax
  ≡̇-transitivity-syntax = ≡̇-transitivity
  syntax ≡̇-transitivity-syntax f g = g ⟨≡̇⟩ f


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Machine words
------------------------------------------------------------------------

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

module Data.Word where

------------------------------------------------------------------------
-- Re-export base definitions and decidability of equality

open import Data.Word.Base public
open import Data.Word.Properties using (_≈?_; _<?_; _≟_; _==_) public


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

module Level where

open import Agda.Primitive
  using (Level)
  renaming ( _⊔_ to _ℓ⊔_
           ; lzero to ℓzero
           ; lsuc  to ℓsuc
           ; Set to Type
           )
  public

variable
  a b c : Level
  A  : Type a
  B  : Type b
  C  : Type c

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module negation where

open import level
open import empty

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

infix 7 ¬

----------------------------------------------------------------------
-- defined types
----------------------------------------------------------------------

¬ : ∀{ℓ}(x : Set ℓ) → Set ℓ
¬ {ℓ} x = x → (⊥ {ℓ})

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
{-# OPTIONS --without-K #-}
module hott.loop.properties where

open import sum
open import equality
open import function.core
open import function.extensionality
open import function.isomorphism.core
open import function.overloading
open import pointed
open import sets.nat.core
open import hott.loop.core

mapΩ₁-const : ∀ {i j}{𝓧 : PSet i}{𝓨 : PSet j}
            → mapΩ₁ (constP 𝓧 𝓨) ≡ constP _ _
mapΩ₁-const = apply≅ pmap-eq (ap-const _ , refl)
  where
    ap-const : ∀ {i j}{X : Set i}{Y : Set j}(y : Y)
             → {x x' : X}(p : x ≡ x') → ap (λ _ → y) p ≡ refl
    ap-const y refl = refl

mapΩP-const : ∀ {i j} n → {𝓧 : PSet i}{𝓨 : PSet j}
            → mapΩP n (constP 𝓧 𝓨) ≡ constP _ _
mapΩP-const zero = refl
mapΩP-const (suc n) = ap (mapΩP n) mapΩ₁-const · mapΩP-const n

mapΩ-const : ∀ {i j} n → {X : Set i}{Y : Set j}(y : Y)
           → (x : X) (p : Ω n x)
           → mapΩ n (λ _ → y) p ≡ refl' n y
mapΩ-const n y x p = funext-inv (ap proj₁ (mapΩP-const n)) p

mapΩ₁-hom : ∀ {i j k}{𝓧 : PSet i}{𝓨 : PSet j}{𝓩 : PSet k}
          → (f : PMap 𝓧 𝓨)(g : PMap 𝓨 𝓩)
          → mapΩ₁ g ∘ mapΩ₁ f ≡ mapΩ₁ (g ∘ f)
mapΩ₁-hom (f , refl) (g , refl) = apply≅ pmap-eq (ap-hom f g , refl)

mapΩP-hom : ∀ {i j k} n → {𝓧 : PSet i}{𝓨 : PSet j}{𝓩 : PSet k}
          → (f : PMap 𝓧 𝓨)(g : PMap 𝓨 𝓩)
          → mapΩP n g ∘ mapΩP n f ≡ mapΩP n (g ∘ f)
mapΩP-hom zero f g = refl
mapΩP-hom (suc n) f g = mapΩP-hom n (mapΩ₁ f) (mapΩ₁ g)
                      · ap (mapΩP n) (mapΩ₁-hom f g)

mapΩ-hom : ∀ {i j k} n {X : Set i}{Y : Set j}{Z : Set k}
         → (f : X → Y)(g : Y → Z){x : X}(p : Ω n x)
         → mapΩ n g (mapΩ n f p) ≡ mapΩ n (g ∘ f) p
mapΩ-hom n f g = proj₁ (invert≅ pmap-eq (mapΩP-hom n (f , refl) (g , refl)))

mapΩ-refl : ∀ {i j} n {X : Set i}{Y : Set j}
          → (f : X → Y){x : X}
          → mapΩ n f (refl' n x) ≡ refl' n (f x)
mapΩ-refl n f = proj₂ (mapΩP n (f , refl))

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
------------------------------------------------------------------------
-- Containers, including a definition of bag equivalence
------------------------------------------------------------------------

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

open import Equality

module Container {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude hiding (id; List)

open import Bag-equivalence eq using (Kind); open Kind
open import Bijection eq as Bijection using (_↔_; module _↔_)
open import Equivalence eq as Eq
  using (Is-equivalence; _≃_; ⟨_,_⟩; module _≃_)
open import Function-universe eq as Function-universe
  hiding (inverse; Kind) renaming (_∘_ to _⟨∘⟩_)
open import H-level eq
open import H-level.Closure eq
open import Surjection eq using (module _↠_)

------------------------------------------------------------------------
-- Containers

record Container c : Type (lsuc c) where
  constructor _▷_
  field
    Shape    : Type c
    Position : Shape → Type c

open Container public

-- Interpretation of containers.

⟦_⟧ : ∀ {c ℓ} → Container c → Type ℓ → Type _
⟦ S ▷ P ⟧ A = ∃ λ (s : S) → (P s → A)

------------------------------------------------------------------------
-- Some projections

-- The shape of something.

shape : ∀ {a c} {A : Type a} {C : Container c} → ⟦ C ⟧ A → Shape C
shape = proj₁

-- Finds the value at the given position.

index : ∀ {a c} {A : Type a} {C : Container c}
        (xs : ⟦ C ⟧ A) → Position C (shape xs) → A
index = proj₂

------------------------------------------------------------------------
-- Map

-- Containers are functors.

map : ∀ {c x y} {C : Container c} {X : Type x} {Y : Type y} →
      (X → Y) → ⟦ C ⟧ X → ⟦ C ⟧ Y
map f = Σ-map id (f ∘_)

module Map where

  identity : ∀ {c x} {C : Container c} {X : Type x}
             (xs : ⟦ C ⟧ X) → map id xs ≡ xs
  identity xs = refl _

  composition :
    ∀ {c x y z}
      {C : Container c} {X : Type x} {Y : Type y} {Z : Type z}
    (f : Y → Z) (g : X → Y) (xs : ⟦ C ⟧ X) →
    map f (map g xs) ≡ map (f ∘ g) xs
  composition f g xs = refl _

-- Naturality.

Natural : ∀ {c₁ c₂ a} {C₁ : Container c₁} {C₂ : Container c₂} →
          ({A : Type a} → ⟦ C₁ ⟧ A → ⟦ C₂ ⟧ A) → Type (c₁ ⊔ c₂ ⊔ lsuc a)
Natural function =
  ∀ {A B} (f : A → B) xs →
  map f (function xs) ≡ function (map f xs)

-- Natural transformations.

infixr 4 _[_]⟶_

record _[_]⟶_ {c₁ c₂} (C₁ : Container c₁) ℓ (C₂ : Container c₂) :
              Type (c₁ ⊔ c₂ ⊔ lsuc ℓ) where
  field
    function : {A : Type ℓ} → ⟦ C₁ ⟧ A → ⟦ C₂ ⟧ A
    natural  : Natural function

-- Natural isomorphisms.

record _[_]↔_ {c₁ c₂} (C₁ : Container c₁) ℓ (C₂ : Container c₂) :
              Type (c₁ ⊔ c₂ ⊔ lsuc ℓ) where
  field
    isomorphism : {A : Type ℓ} → ⟦ C₁ ⟧ A ↔ ⟦ C₂ ⟧ A
    natural     : Natural (_↔_.to isomorphism)

  -- Natural isomorphisms are natural transformations.

  natural-transformation : C₁ [ ℓ ]⟶ C₂
  natural-transformation = record
    { function = _↔_.to isomorphism
    ; natural  = natural
    }

  -- Natural isomorphisms can be inverted.

  inverse : C₂ [ ℓ ]↔ C₁
  inverse = record
    { isomorphism = Function-universe.inverse isomorphism
    ; natural     = λ f xs →
        map f (from xs)              ≡⟨ sym $ left-inverse-of _ ⟩
        from (to (map f (from xs)))  ≡⟨ sym $ cong from $ natural f (from xs) ⟩
        from (map f (to (from xs)))  ≡⟨ cong (from ∘ map f) $ right-inverse-of _ ⟩∎
        from (map f xs)              ∎
    }
    where open module I {A : Type ℓ} = _↔_ (isomorphism {A = A})

open Function-universe using (inverse)

------------------------------------------------------------------------
-- Any, _∈_, bag equivalence and similar relations

-- Definition of Any for containers.

Any : ∀ {a c p} {A : Type a} {C : Container c} →
      (A → Type p) → (⟦ C ⟧ A → Type (c ⊔ p))
Any {C = S ▷ P} Q (s , f) = ∃ λ (p : P s) → Q (f p)

-- Membership predicate.

infix 4 _∈_

_∈_ : ∀ {a c} {A : Type a} {C : Container c} → A → ⟦ C ⟧ A → Type _
x ∈ xs = Any (λ y → x ≡ y) xs

-- Bag equivalence etc. Note that the containers can be different as
-- long as the elements they contain have equal types.

infix 4 _∼[_]_

_∼[_]_ : ∀ {a c₁ c₂}
           {A : Type a} {C₁ : Container c₁} {C₂ : Container c₂} →
         ⟦ C₁ ⟧ A → Kind → ⟦ C₂ ⟧ A → Type _
xs ∼[ k ] ys = ∀ z → z ∈ xs ↝[ k ] z ∈ ys

-- Bag equivalence.

infix 4 _≈-bag_

_≈-bag_ : ∀ {a c₁ c₂}
            {A : Type a} {C₁ : Container c₁} {C₂ : Container c₂} →
          ⟦ C₁ ⟧ A → ⟦ C₂ ⟧ A → Type _
xs ≈-bag ys = xs ∼[ bag ] ys

------------------------------------------------------------------------
-- Various properties related to Any, _∈_ and _∼[_]_

-- Lemma relating Any to map.

Any-map : ∀ {a b c p} {A : Type a} {B : Type b} {C : Container c}
          (P : B → Type p) (f : A → B) (xs : ⟦ C ⟧ A) →
          Any P (map f xs) ↔ Any (P ∘ f) xs
Any-map P f xs = Any P (map f xs) □

-- Any can be expressed using _∈_.

Any-∈ : ∀ {a c p} {A : Type a} {C : Container c}
        (P : A → Type p) (xs : ⟦ C ⟧ A) →
        Any P xs ↔ ∃ λ x → P x × x ∈ xs
Any-∈ P (s , f) =
  (∃ λ p → P (f p))                ↔⟨ ∃-cong (λ p → ∃-intro P (f p)) ⟩
  (∃ λ p → ∃ λ x → P x × x ≡ f p)  ↔⟨ ∃-comm ⟩
  (∃ λ x → ∃ λ p → P x × x ≡ f p)  ↔⟨ ∃-cong (λ _ → ∃-comm) ⟩
  (∃ λ x → P x × ∃ λ p → x ≡ f p)  □

-- Using this property we can prove that Any and _⊎_ commute.

Any-⊎ : ∀ {a c p q} {A : Type a} {C : Container c}
        (P : A → Type p) (Q : A → Type q) (xs : ⟦ C ⟧ A) →
        Any (λ x → P x ⊎ Q x) xs ↔ Any P xs ⊎ Any Q xs
Any-⊎ P Q xs =
  Any (λ x → P x ⊎ Q x) xs                         ↔⟨ Any-∈ (λ x → P x ⊎ Q x) xs ⟩
  (∃ λ x → (P x ⊎ Q x) × x ∈ xs)                   ↔⟨ ∃-cong (λ x → ×-⊎-distrib-right) ⟩
  (∃ λ x → P x × x ∈ xs ⊎ Q x × x ∈ xs)            ↔⟨ ∃-⊎-distrib-left ⟩
  (∃ λ x → P x × x ∈ xs) ⊎ (∃ λ x → Q x × x ∈ xs)  ↔⟨ inverse $ Any-∈ P xs ⊎-cong Any-∈ Q xs ⟩
  Any P xs ⊎ Any Q xs                              □

-- Any preserves functions of various kinds and respects bag
-- equivalence and similar relations.

Any-cong : ∀ {k a c d p q}
             {A : Type a} {C : Container c} {D : Container d}
           (P : A → Type p) (Q : A → Type q)
           (xs : ⟦ C ⟧ A) (ys : ⟦ D ⟧ A) →
           (∀ x → P x ↝[ k ] Q x) → xs ∼[ k ] ys →
           Any P xs ↝[ k ] Any Q ys
Any-cong P Q xs ys P↔Q xs∼ys =
  Any P xs                ↔⟨ Any-∈ P xs ⟩
  (∃ λ z → P z × z ∈ xs)  ↝⟨ ∃-cong (λ z → P↔Q z ×-cong xs∼ys z) ⟩
  (∃ λ z → Q z × z ∈ ys)  ↔⟨ inverse (Any-∈ Q ys) ⟩
  Any Q ys                □

-- Map preserves the relations.

map-cong :
  ∀ {k a b c d}
    {A : Type a} {B : Type b} {C : Container c} {D : Container d}
  (f : A → B)
  (xs : ⟦ C ⟧ A) (ys : ⟦ D ⟧ A) →
  xs ∼[ k ] ys → map f xs ∼[ k ] map f ys
map-cong f xs ys xs∼ys = λ z →
  z ∈ map f xs            ↔⟨ Any-map (_≡_ z) f xs ⟩
  Any (λ x → z ≡ f x) xs  ↝⟨ Any-cong _ _ xs ys (λ x → z ≡ f x □) xs∼ys ⟩
  Any (λ x → z ≡ f x) ys  ↔⟨ inverse (Any-map (_≡_ z) f ys) ⟩
  z ∈ map f ys            □

-- Lemma relating Any to if_then_else_.

Any-if : ∀ {a c p} {A : Type a} {C : Container c}
         (P : A → Type p) (xs ys : ⟦ C ⟧ A) b →
         Any P (if b then xs else ys) ↔
         T b × Any P xs ⊎ T (not b) × Any P ys
Any-if P xs ys =
  inverse ∘ if-lemma (λ b → Any P (if b then xs else ys)) id id

-- One can reconstruct (up to natural isomorphism) the shape set and
-- the position predicate from the interpretation and the Any
-- predicate transformer.
--
-- (The following lemmas were suggested by an anonymous reviewer.)

Shape′ : ∀ {c} → (Type → Type c) → Type c
Shape′ F = F ⊤

Shape-⟦⟧ : ∀ {c} (C : Container c) →
           Shape C ↔ Shape′ ⟦ C ⟧
Shape-⟦⟧ C =
  Shape C                                 ↔⟨ inverse ×-right-identity ⟩
  Shape C × ⊤                             ↔⟨ ∃-cong (λ _ → inverse →-right-zero) ⟩
  (∃ λ (s : Shape C) → Position C s → ⊤)  □

Position′ : ∀ {c} (F : Type → Type c) →
            ({A : Type} → (A → Type) → (F A → Type c)) →
            Shape′ F → Type c
Position′ _ Any = Any (λ (_ : ⊤) → ⊤)

Position-Any : ∀ {c} {C : Container c} (s : Shape C) →
               Position C s ↔
               Position′ ⟦ C ⟧ Any (_↔_.to (Shape-⟦⟧ C) s)
Position-Any {C = C} s =
  Position C s      ↔⟨ inverse ×-right-identity ⟩
  Position C s × ⊤  □

expressed-in-terms-of-interpretation-and-Any :
  ∀ {c ℓ} (C : Container c) →
  C [ ℓ ]↔ (⟦ C ⟧ ⊤ ▷ Any (λ _ → ⊤))
expressed-in-terms-of-interpretation-and-Any C = record
  { isomorphism = λ {A} →
      (∃ λ (s : Shape C) → Position C s → A)                ↔⟨ Σ-cong (Shape-⟦⟧ C) (λ _ → lemma) ⟩
      (∃ λ (s : Shape′ ⟦ C ⟧) → Position′ ⟦ C ⟧ Any s → A)  □
  ; natural = λ _ _ → refl _
  }
  where
  -- If equality of functions had been extensional, then the following
  -- lemma could have been replaced by a congruence lemma applied to
  -- Position-Any.
  lemma : ∀ {a b} {A : Type a} {B : Type b} → (B → A) ↔ (B × ⊤ → A)
  lemma = record
    { surjection = record
      { logical-equivalence = record
        { to   = λ { f (p , tt) → f p }
        ; from = λ f p → f (p , tt)
        }
      ; right-inverse-of = λ _ → refl _
      }
    ; left-inverse-of = λ _ → refl _
    }

------------------------------------------------------------------------
-- Alternative definition of bag equivalence

-- Two things are bag equivalent if there is a bijection (or
-- equivalence) between their positions that relates equal things.

infix 4 _≈[_]′_

_≈[_]′_ : ∀ {a c d} {A : Type a} {C : Container c} {D : Container d} →
          ⟦ C ⟧ A → Isomorphism-kind → ⟦ D ⟧ A → Type _
_≈[_]′_ {C = C} {D} (s , f) k (s′ , f′) =
  ∃ λ (P↔P : Position C s ↔[ k ] Position D s′) →
      (∀ p → f p ≡ f′ (to-implication P↔P p))

-- If the position sets are sets (have H-level two), then the two
-- instantiations of _≈[_]′_ are isomorphic (assuming extensionality).

≈′↔≈′ : ∀ {a c d} {A : Type a} {C : Container c} {D : Container d} →
        Extensionality (c ⊔ d) (c ⊔ d) →
        (∀ s → Is-set (Position C s)) →
        (xs : ⟦ C ⟧ A) (ys : ⟦ D ⟧ A) →
        xs ≈[ bag ]′ ys ↔ xs ≈[ bag-with-equivalence ]′ ys
≈′↔≈′ ext P-set (s , f) (s′ , f′) =
  (∃ λ P↔P → ∀ p → f p ≡ f′ (to-implication P↔P p))  ↔⟨ Σ-cong (Eq.↔↔≃ ext (P-set s)) (λ _ → Bijection.id) ⟩
  (∃ λ P↔P → ∀ p → f p ≡ f′ (to-implication P↔P p))  □

-- The definition _≈[_]′_ is also logically equivalent to the one
-- given above. The proof is very similar to the one given in
-- Bag-equivalence.

-- Membership can be expressed as "there is an index which points to
-- the element". In fact, membership /is/ expressed in this way, so
-- this proof is unnecessary.

∈-index : ∀ {a c} {A : Type a} {C : Container c} {z}
          (xs : ⟦ C ⟧ A) → z ∈ xs ↔ ∃ λ p → z ≡ index xs p
∈-index {z = z} xs = z ∈ xs □

-- The index which points to the element (not used below).

index-of : ∀ {a c} {A : Type a} {C : Container c} {z}
           (xs : ⟦ C ⟧ A) → z ∈ xs → Position C (shape xs)
index-of xs = proj₁ ∘ to-implication (∈-index xs)

-- The positions for a given shape can be expressed in terms of the
-- membership predicate.

Position-shape :
  ∀ {a c} {A : Type a} {C : Container c} (xs : ⟦ C ⟧ A) →
  (∃ λ z → z ∈ xs) ↔ Position C (shape xs)
Position-shape {C = C} (s , f) =
  (∃ λ z → ∃ λ p → z ≡ f p)  ↔⟨ ∃-comm ⟩
  (∃ λ p → ∃ λ z → z ≡ f p)  ↔⟨⟩
  (∃ λ p → Singleton (f p))  ↔⟨ ∃-cong (λ _ → _⇔_.to contractible⇔↔⊤ (singleton-contractible _)) ⟩
  Position C s × ⊤           ↔⟨ ×-right-identity ⟩
  Position C s               □

-- Position _ ∘ shape respects the various relations.

Position-shape-cong :
  ∀ {k a c d} {A : Type a} {C : Container c} {D : Container d}
  (xs : ⟦ C ⟧ A) (ys : ⟦ D ⟧ A) →
  xs ∼[ k ] ys → Position C (shape xs) ↝[ k ] Position D (shape ys)
Position-shape-cong {C = C} {D} xs ys xs∼ys =
  Position C (shape xs)  ↔⟨ inverse $ Position-shape xs ⟩
  ∃ (λ z → z ∈ xs)       ↝⟨ ∃-cong xs∼ys ⟩
  ∃ (λ z → z ∈ ys)       ↔⟨ Position-shape ys ⟩
  Position D (shape ys)  □

-- Furthermore Position-shape-cong relates equal elements.

Position-shape-cong-relates :
  ∀ {k a c d} {A : Type a} {C : Container c} {D : Container d}
  (xs : ⟦ C ⟧ A) (ys : ⟦ D ⟧ A) (xs≈ys : xs ∼[ k ] ys) p →
  index xs p ≡
    index ys (to-implication (Position-shape-cong xs ys xs≈ys) p)
Position-shape-cong-relates {bag} xs ys xs≈ys p =
  index xs p                                                     ≡⟨ proj₂ $ to-implication (xs≈ys (index xs p)) (p , refl _) ⟩
  index ys (proj₁ $ to-implication (xs≈ys (index xs p))
                                   (p , refl _))                 ≡⟨⟩
  index ys (_↔_.to (Position-shape ys) $
            Σ-map id (λ {z} → to-implication (xs≈ys z)) $
            _↔_.from (Position-shape xs) $ p)                    ≡⟨⟩
  index ys (_↔_.to (Position-shape ys) $
            to-implication (∃-cong xs≈ys) $
            _↔_.from (Position-shape xs) $ p)                    ≡⟨⟩
  index ys (to-implication
              ((from-bijection (Position-shape ys) ⟨∘⟩
                ∃-cong xs≈ys) ⟨∘⟩
               from-bijection (inverse $ Position-shape xs))
              p)                                                 ≡⟨⟩
  index ys (to-implication (Position-shape-cong xs ys xs≈ys) p)  ∎

Position-shape-cong-relates {bag-with-equivalence} xs ys xs≈ys p =
  proj₂ $ to-implication (xs≈ys (index xs p)) (p , refl _)
Position-shape-cong-relates {bag-with-equivalenceᴱ} xs ys xs≈ys p =
  proj₂ $ to-implication (xs≈ys (index xs p)) (p , refl _)
Position-shape-cong-relates {subbag} xs ys xs≈ys p =
  proj₂ $ to-implication (xs≈ys (index xs p)) (p , refl _)
Position-shape-cong-relates {set} xs ys xs≈ys p =
  proj₂ $ to-implication (xs≈ys (index xs p)) (p , refl _)
Position-shape-cong-relates {subset} xs ys xs≈ys p =
  proj₂ $ to-implication (xs≈ys (index xs p)) (p , refl _)
Position-shape-cong-relates {embedding} xs ys xs≈ys p =
  proj₂ $ to-implication (xs≈ys (index xs p)) (p , refl _)
Position-shape-cong-relates {surjection} xs ys xs≈ys p =
  proj₂ $ to-implication (xs≈ys (index xs p)) (p , refl _)

-- We get that the two definitions of bag equivalence are logically
-- equivalent.

≈⇔≈′ : ∀ {k a c d} {A : Type a} {C : Container c} {D : Container d}
       (xs : ⟦ C ⟧ A) (ys : ⟦ D ⟧ A) →
       xs ∼[ ⌊ k ⌋-iso ] ys ⇔ xs ≈[ k ]′ ys
≈⇔≈′ {k} xs ys = record
  { to   = λ xs≈ys → ( Position-shape-cong xs ys xs≈ys
                     , Position-shape-cong-relates xs ys xs≈ys
                     )
  ; from = from
  }
  where
  from : xs ≈[ k ]′ ys → xs ∼[ ⌊ k ⌋-iso ] ys
  from (P↔P , related) = λ z →
    z ∈ xs                    ↔⟨⟩
    ∃ (λ p → z ≡ index xs p)  ↔⟨ Σ-cong P↔P (λ p → _↠_.from (Π≡↔≡-↠-≡ k _ _) (related p) z) ⟩
    ∃ (λ p → z ≡ index ys p)  ↔⟨⟩
    z ∈ ys                    □

-- If equivalences are used, then the definitions are isomorphic
-- (assuming extensionality).
--
-- Thierry Coquand helped me with this proof: At first I wasn't sure
-- if it was true or not, but then I managed to prove it for singleton
-- lists, Thierry found a proof for lists of length two, I found one
-- for streams, and finally I could complete a proof of the statement
-- below.

≈↔≈′ : ∀ {a c d} {A : Type a} {C : Container c} {D : Container d} →
       Extensionality (a ⊔ c ⊔ d) (a ⊔ c ⊔ d) →
       (xs : ⟦ C ⟧ A) (ys : ⟦ D ⟧ A) →
       xs ∼[ bag-with-equivalence ] ys ↔
       xs ≈[ bag-with-equivalence ]′ ys
≈↔≈′ {a} {c} {d} {C = C} {D} ext xs ys = record
  { surjection = record
    { logical-equivalence = equiv
    ; right-inverse-of    = λ { (⟨ f , f-eq ⟩ , related) →
      let
        P : (Position C (shape xs) → Position D (shape ys)) →
            Type (a ⊔ c)
        P f = ∀ p → index xs p ≡ index ys (f p)

        f-eq′ : Is-equivalence f
        f-eq′ = _

        irr : f-eq′ ≡ f-eq
        irr = proj₁ $ +⇒≡ $
          Eq.propositional (lower-extensionality a a ext) f

        f≡f : ⟨ f , f-eq′ ⟩ ≡ ⟨ f , f-eq ⟩
        f≡f = cong (⟨_,_⟩ f) irr

        cong-to-f≡f : cong _≃_.to f≡f ≡ refl f
        cong-to-f≡f =
          cong _≃_.to f≡f              ≡⟨ cong-∘ _≃_.to (⟨_,_⟩ f) irr ⟩
          cong (_≃_.to ∘ ⟨_,_⟩ f) irr  ≡⟨ cong-const irr ⟩∎
          refl _                       ∎
      in
      Σ-≡,≡→≡ f≡f
        (subst (P ∘ _≃_.to) f≡f (trans (refl _) ∘ related)  ≡⟨ cong (subst (P ∘ _≃_.to) f≡f)
                                                                    (apply-ext (lower-extensionality (a ⊔ d) (c ⊔ d) ext) λ _ → trans-reflˡ _) ⟩
         subst (P ∘ _≃_.to) f≡f related                     ≡⟨ subst-∘ P _≃_.to f≡f ⟩
         subst P (cong _≃_.to f≡f) related                  ≡⟨ cong (λ eq → subst P eq related) cong-to-f≡f ⟩
         subst P (refl _) related                           ≡⟨ subst-refl P related ⟩∎
         related                                            ∎) }
    }
  ; left-inverse-of = λ xs≈ys →
      apply-ext (lower-extensionality (c ⊔ d) a ext) λ z →
        Eq.lift-equality ext $
          apply-ext (lower-extensionality d c ext) λ { (p , z≡xs[p]) →

              let xs[p]≡ys[-] : ∃ λ p′ → index xs p ≡ index ys p′
                  xs[p]≡ys[-] = _≃_.to (xs≈ys (index xs p)) (p , refl _)
              in

            Σ-map id (trans z≡xs[p]) xs[p]≡ys[-]      ≡⟨ elim₁ (λ {z} z≡xs[p] → Σ-map id (trans z≡xs[p]) xs[p]≡ys[-] ≡
                                                                          _≃_.to (xs≈ys z) (p , z≡xs[p]))
              (Σ-map id (trans (refl _)) xs[p]≡ys[-]              ≡⟨ cong (_,_ _) (trans-reflˡ _) ⟩∎
               xs[p]≡ys[-]                                        ∎)
                                                               z≡xs[p] ⟩∎
            _≃_.to (xs≈ys z) (p , z≡xs[p])            ∎ }
  }
  where
  equiv = ≈⇔≈′ {k = equivalence} xs ys

  open _⇔_ equiv

------------------------------------------------------------------------
-- Another alternative definition of bag equivalence

-- A higher-order variant of _∼[_]_. Note that this definition is
-- large (due to the quantification over predicates).

infix 4 _∼[_]″_

_∼[_]″_ : ∀ {a c d} {A : Type a} {C : Container c} {D : Container d} →
          ⟦ C ⟧ A → Kind → ⟦ D ⟧ A → Type (lsuc a ⊔ c ⊔ d)
_∼[_]″_ {a} {A = A} xs k ys =
  (P : A → Type a) → Any P xs ↝[ k ] Any P ys

-- This definition is logically equivalent to _∼[_]_.

∼⇔∼″ : ∀ {k a c d} {A : Type a} {C : Container c} {D : Container d}
       (xs : ⟦ C ⟧ A) (ys : ⟦ D ⟧ A) →
       xs ∼[ k ] ys ⇔ xs ∼[ k ]″ ys
∼⇔∼″ xs ys = record
  { to   = λ xs∼ys P → Any-cong P P xs ys (λ _ → id) xs∼ys
  ; from = λ Any-xs↝Any-ys z → Any-xs↝Any-ys (λ x → z ≡ x)
  }

------------------------------------------------------------------------
-- The ⟦_⟧₂ operator

-- Lifts a family of binary relations from A to ⟦ C ⟧ A.

⟦_⟧₂ :
  ∀ {a c r} {A : Type a} (C : Container c) →
  (A → A → Type r) →
  ⟦ C ⟧ A → ⟦ C ⟧ A → Type (c ⊔ r)
⟦ C ⟧₂ R (s , f) (t , g) =
  ∃ λ (eq : s ≡ t) →
  (p : Position C s) →
  R (f p) (g (subst (Position C) eq p))
  where
  open Container

-- A map function for ⟦_⟧₂.

⟦⟧₂-map :
  ∀ {a b c r s} {A : Type a} {B : Type b} {C : Container c}
  (R : A → A → Type r) (S : B → B → Type s) (f : A → B) →
  (∀ x y → R x y → S (f x) (f y)) →
  (∀ x y → ⟦ C ⟧₂ R x y → ⟦ C ⟧₂ S (map f x) (map f y))
⟦⟧₂-map _ _ _ f _ _ = Σ-map id (f _ _ ∘_)

-- ⟦_⟧₂ preserves reflexivity.

⟦⟧₂-reflexive :
  ∀ {a c r} {A : Type a} {C : Container c}
  (R : A → A → Type r) →
  (∀ x → R x x) →
  (∀ x → ⟦ C ⟧₂ R x x)
⟦⟧₂-reflexive {C = C} R r (xs , f) =
    refl _
  , λ p →                                           $⟨ r _ ⟩
      R (f p) (f p)                                 ↝⟨ subst (R _ ∘ f) (sym $ subst-refl _ _) ⟩□
      R (f p) (f (subst (Position C) (refl xs) p))  □

-- ⟦_⟧₂ preserves symmetry.

⟦⟧₂-symmetric :
  ∀ {a c r} {A : Type a} {C : Container c}
  (R : A → A → Type r) →
  (∀ {x y} → R x y → R y x) →
  (∀ {x y} → ⟦ C ⟧₂ R x y → ⟦ C ⟧₂ R y x)
⟦⟧₂-symmetric {C = C} R r {_ , f} {_ , g} (eq , h) =
    sym eq
  , λ p →                                                            $⟨ h (subst (Position C) (sym eq) p) ⟩
      R (f (subst (Position C) (sym eq) p))
        (g (subst (Position C) eq (subst (Position C) (sym eq) p)))  ↝⟨ subst (R (f (subst (Position C) (sym eq) p)) ∘ g) $ subst-subst-sym _ _ _ ⟩

      R (f (subst (Position C) (sym eq) p)) (g p)                    ↝⟨ r ⟩□

      R (g p) (f (subst (Position C) (sym eq) p))                    □

-- ⟦_⟧₂ preserves transitivity.

⟦⟧₂-transitive :
  ∀ {a c r} {A : Type a} {C : Container c}
  (R : A → A → Type r) →
  (∀ {x y z} → R x y → R y z → R x z) →
  (∀ {x y z} → ⟦ C ⟧₂ R x y → ⟦ C ⟧₂ R y z → ⟦ C ⟧₂ R x z)
⟦⟧₂-transitive {C = C}
               R r {_ , f} {_ , g} {_ , h} (eq₁ , f₁) (eq₂ , f₂) =
    trans eq₁ eq₂
  , λ p →                                                             $⟨ f₂ _ ⟩
      R (g (subst (Position C) eq₁ p))
        (h (subst (Position C) eq₂ (subst (Position C) eq₁ p)))       ↝⟨ subst (R (g (subst (Position C) _ _)) ∘ h) $ subst-subst _ _ _ _ ⟩

      R (g (subst (Position C) eq₁ p))
        (h (subst (Position C) (trans eq₁ eq₂) p))                    ↝⟨ f₁ _ ,_ ⟩

      R (f p) (g (subst (Position C) eq₁ p)) ×
      R (g (subst (Position C) eq₁ p))
        (h (subst (Position C) (trans eq₁ eq₂) p))                    ↝⟨ uncurry r ⟩□

      R (f p) (h (subst (Position C) (trans eq₁ eq₂) p))              □


text:
{-

Descriptor language for easily defining structures

-}
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Structures.Macro where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.SIP
open import Cubical.Functions.FunExtEquiv
open import Cubical.Data.Sigma
open import Cubical.Data.Maybe

open import Cubical.Structures.Constant
open import Cubical.Structures.Maybe
open import Cubical.Structures.NAryOp
open import Cubical.Structures.Parameterized
open import Cubical.Structures.Pointed
open import Cubical.Structures.Product
open import Cubical.Structures.Functorial

data FuncDesc (ℓ : Level) : Typeω where
  -- constant structure: X ↦ A
  constant : ∀ {ℓ'} → Type ℓ' → FuncDesc ℓ
  -- pointed structure: X ↦ X
  var : FuncDesc ℓ
  -- join of structures S,T : X ↦ (S X × T X)
  _,_ : FuncDesc ℓ  → FuncDesc ℓ  → FuncDesc ℓ
  -- structure S parameterized by constant A : X ↦ (A → S X)
  param : ∀ {ℓ'} → (A : Type ℓ') → FuncDesc ℓ  → FuncDesc ℓ
  -- structure S parameterized by variable argument: X ↦ (X → S X)
  maybe : FuncDesc ℓ → FuncDesc ℓ

data Desc (ℓ : Level) : Typeω where
  -- constant structure: X ↦ A
  constant : ∀ {ℓ'} → Type ℓ' → Desc ℓ
  -- pointed structure: X ↦ X
  var : Desc ℓ
  -- join of structures S,T : X ↦ (S X × T X)
  _,_ : Desc ℓ  → Desc ℓ  → Desc ℓ
  -- structure S parameterized by constant A : X ↦ (A → S X)
  param : ∀ {ℓ'} → (A : Type ℓ') → Desc ℓ  → Desc ℓ
  -- structure S parameterized by variable argument: X ↦ (X → S X)
  recvar : Desc ℓ  → Desc ℓ
  -- Maybe on a structure S: X ↦ Maybe (S X)
  maybe : Desc ℓ → Desc ℓ
  -- SNS from functorial action
  functorial : FuncDesc ℓ → Desc ℓ
  -- arbitrary standard notion of structure
  foreign : ∀ {ℓ' ℓ''} {S : Type ℓ → Type ℓ'} (ι : StrEquiv S ℓ'') → UnivalentStr S ι → Desc ℓ

infixr 4 _,_

{- Functorial structures -}

funcMacroLevel : ∀ {ℓ} → FuncDesc ℓ → Level
funcMacroLevel (constant {ℓ'} x) = ℓ'
funcMacroLevel {ℓ} var = ℓ
funcMacroLevel {ℓ} (d₀ , d₁) = ℓ-max (funcMacroLevel d₀) (funcMacroLevel d₁)
funcMacroLevel (param {ℓ'} A d) = ℓ-max ℓ' (funcMacroLevel d)
funcMacroLevel (maybe d) = funcMacroLevel d

-- Structure defined by a functorial descriptor
FuncMacroStructure : ∀ {ℓ} (d : FuncDesc ℓ) → Type ℓ → Type (funcMacroLevel d)
FuncMacroStructure (constant A) X = A
FuncMacroStructure var X = X
FuncMacroStructure (d₀ , d₁) X = FuncMacroStructure d₀ X × FuncMacroStructure d₁ X
FuncMacroStructure (param A d) X = A → FuncMacroStructure d X
FuncMacroStructure (maybe d) = MaybeStructure (FuncMacroStructure d)

-- Action defined by a functorial descriptor
funcMacroAction : ∀ {ℓ} (d : FuncDesc ℓ)
  {X Y : Type ℓ} → (X → Y) → FuncMacroStructure d X → FuncMacroStructure d Y
funcMacroAction (constant A) _ = idfun A
funcMacroAction var f = f
funcMacroAction (d₀ , d₁) f (s₀ , s₁) = funcMacroAction d₀ f s₀ , funcMacroAction d₁ f s₁
funcMacroAction (param A d) f s a = funcMacroAction d f (s a)
funcMacroAction (maybe d) f = map-Maybe (funcMacroAction d f)

-- Proof that the action preserves the identity
funcMacroId : ∀ {ℓ} (d : FuncDesc ℓ)
  {X : Type ℓ} → ∀ s → funcMacroAction d (idfun X) s ≡ s
funcMacroId (constant A) _ = refl
funcMacroId var _ = refl
funcMacroId (d₀ , d₁) (s₀ , s₁) = ΣPath≃PathΣ .fst (funcMacroId d₀ s₀ , funcMacroId d₁ s₁)
funcMacroId (param A d) s = funExt λ a → funcMacroId d (s a)
funcMacroId (maybe d) s = cong₂ map-Maybe (funExt (funcMacroId d)) refl ∙ map-Maybe-id s

{- General structures -}

macroStrLevel : ∀ {ℓ} → Desc ℓ → Level
macroStrLevel (constant {ℓ'} x) = ℓ'
macroStrLevel {ℓ} var = ℓ
macroStrLevel {ℓ} (d₀ , d₁) = ℓ-max (macroStrLevel d₀) (macroStrLevel d₁)
macroStrLevel (param {ℓ'} A d) = ℓ-max ℓ' (macroStrLevel d)
macroStrLevel {ℓ} (recvar d) = ℓ-max ℓ (macroStrLevel d)
macroStrLevel (maybe d) = macroStrLevel d
macroStrLevel (functorial d) = funcMacroLevel d
macroStrLevel (foreign {ℓ'} _ _) = ℓ'

macroEquivLevel : ∀ {ℓ} → Desc ℓ → Level
macroEquivLevel (constant {ℓ'} x) = ℓ'
macroEquivLevel {ℓ} var = ℓ
macroEquivLevel {ℓ} (d₀ , d₁) = ℓ-max (macroEquivLevel d₀) (macroEquivLevel d₁)
macroEquivLevel (param {ℓ'} A d) = ℓ-max ℓ' (macroEquivLevel d)
macroEquivLevel {ℓ} (recvar d) = ℓ-max ℓ (macroEquivLevel d)
macroEquivLevel (maybe d) = macroEquivLevel d
macroEquivLevel (functorial d) = funcMacroLevel d
macroEquivLevel (foreign {ℓ'' = ℓ''} _ _) = ℓ''

-- Structure defined by a descriptor
MacroStructure : ∀ {ℓ} (d : Desc ℓ) → Type ℓ → Type (macroStrLevel d)
MacroStructure (constant A) X = A
MacroStructure var X = X
MacroStructure (d₀ , d₁) X = MacroStructure d₀ X × MacroStructure d₁ X
MacroStructure (param A d) X = A → MacroStructure d X
MacroStructure (recvar d) X = X → MacroStructure d X
MacroStructure (maybe d) = MaybeStructure (MacroStructure d)
MacroStructure (functorial d) = FuncMacroStructure d
MacroStructure (foreign {S = S} _ _) = S

-- Notion of structured equivalence defined by a descriptor
MacroEquivStr : ∀ {ℓ} → (d : Desc ℓ) → StrEquiv {ℓ} (MacroStructure d) (macroEquivLevel d)
MacroEquivStr (constant A) = ConstantEquivStr A
MacroEquivStr var = PointedEquivStr
MacroEquivStr (d₀ , d₁) = ProductEquivStr (MacroEquivStr d₀) (MacroEquivStr d₁)
MacroEquivStr (param A d) = ParamEquivStr A λ _ → MacroEquivStr d
MacroEquivStr (recvar d) = UnaryFunEquivStr (MacroEquivStr d)
MacroEquivStr (maybe d) = MaybeEquivStr (MacroEquivStr d)
MacroEquivStr (functorial d) = FunctorialEquivStr (funcMacroAction d)
MacroEquivStr (foreign ι _) = ι

-- Proof that structure induced by descriptor is univalent
MacroUnivalentStr : ∀ {ℓ} → (d : Desc ℓ) → UnivalentStr (MacroStructure d) (MacroEquivStr d)
MacroUnivalentStr (constant A) = constantUnivalentStr A
MacroUnivalentStr var = pointedUnivalentStr
MacroUnivalentStr (d₀ , d₁) =
  ProductUnivalentStr (MacroEquivStr d₀) (MacroUnivalentStr d₀) (MacroEquivStr d₁) (MacroUnivalentStr d₁)
MacroUnivalentStr (param A d) = ParamUnivalentStr A (λ _ → MacroEquivStr d) (λ _ → MacroUnivalentStr d)
MacroUnivalentStr (recvar d) = unaryFunUnivalentStr (MacroEquivStr d) (MacroUnivalentStr d)
MacroUnivalentStr (maybe d) = maybeUnivalentStr (MacroEquivStr d) (MacroUnivalentStr d)
MacroUnivalentStr (functorial d) = functorialUnivalentStr (funcMacroAction d) (funcMacroId d)
MacroUnivalentStr (foreign _ θ) = θ

-- Module for easy importing
module Macro ℓ (d : Desc ℓ) where

  structure = MacroStructure d
  equiv = MacroEquivStr d
  univalent = MacroUnivalentStr d

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
{-# OPTIONS --sized-types #-}
module SNat.Order where

open import Size
open import SNat

data _≤_ : {ι ι' : Size} → SNat {ι} → SNat {ι'} → Set where
  z≤n : {ι ι' : Size}
                   → (n : SNat {ι'})
                   →  _≤_ (zero {ι}) n
  s≤s : {ι ι' : Size}{m : SNat {ι}}{n : SNat {ι'}}
                   → m ≤ n
                   → (succ m) ≤ (succ n)

data _≅_ : {ι ι' : Size} → SNat {ι} → SNat {ι'} → Set where
  z≅z : {ι ι' : Size}
                   → zero {ι} ≅ zero {ι'}
  s≅s : {ι ι' : Size}{m : SNat {ι}}{n : SNat {ι'}}
                   → m ≅ n
                   → succ m ≅ succ n

data _≤′_ : {ι ι' : Size} → SNat {ι} → SNat {ι'} → Set where
  ≤′-eq : {ι ι' : Size}{m : SNat {ι}}{n : SNat {ι'}}
                   → m ≅ n
                   → m ≤′ n
  ≤′-step : {ι ι' : Size}{m : SNat {ι}}{n : SNat {ι'}}
                   → m ≤′ n
                   → m ≤′ succ n

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Oscar.Data.List where

open import Agda.Builtin.List public using (List; []; _∷_)


text:
module FinMap where

open import Level using () renaming (zero to ℓ₀)
open import Data.Nat using (ℕ ; zero ; suc)
open import Data.Maybe using (Maybe ; just ; nothing ; maybe′)
open import Data.Fin using (Fin ; zero ; suc)
open import Data.Fin.Properties using (_≟_)
open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr ; zip ; toList) renaming (lookup to lookupVec ; map to mapV)
open import Data.Vec.Equality using ()
open import Data.Product using (_×_ ; _,_)
open import Data.List.All as All using (All)
import Data.List.All.Properties as AllP
import Data.List.Any as Any
open import Function using (id ; _∘_ ; flip ; const)
open import Function.Equality using (module Π)
open import Function.Surjection using (module Surjection)
open import Relation.Nullary using (yes ; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary.Core using (_≡_ ; refl ; _≢_ ; Decidable)
open import Relation.Binary.PropositionalEquality as P using (cong ; sym ; _≗_ ; trans ; cong₂)
open P.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)

open import Generic using (just-injective)

_∈_ : {A : Set} {n : ℕ} → A → Vec A n → Set
_∈_ {A} x xs = Any.Membership._∈_ (P.setoid A) x (toList xs)

_∉_ : {A : Set} {n : ℕ} → A → Vec A n → Set
_∉_ {A} x xs = All (_≢_ x) (toList xs)

data Dec∈ {A : Set} {n : ℕ} (x : A) (xs : Vec A n) : Set where
  yes-∈ : x ∈ xs → Dec∈ x xs
  no-∉ : x ∉ xs → Dec∈ x xs

is-∈ : {A : Set} {n : ℕ} → Decidable (_≡_ {A = A}) → (x : A) → (xs : Vec A n) → Dec∈ x xs
is-∈ eq? x xs with Any.any (eq? x) (toList xs)
...     | yes x∈xs = yes-∈ x∈xs
...     | no  x∉xs = no-∉ (Π._⟨$⟩_ (Surjection.to AllP.¬Any↠All¬) x∉xs)

FinMapMaybe : ℕ → Set → Set
FinMapMaybe n A = Vec (Maybe A) n

lookupM : {A : Set} {n : ℕ} → Fin n → FinMapMaybe n A → Maybe A
lookupM = lookupVec

insert : {A : Set} {n : ℕ} → Fin n → A → FinMapMaybe n A → FinMapMaybe n A
insert f a m = m [ f ]≔ (just a)

empty : {A : Set} {n : ℕ} → FinMapMaybe n A
empty = replicate nothing

fromAscList : {A : Set} {n m : ℕ} → Vec (Fin n × A) m → FinMapMaybe n A
fromAscList []             = empty
fromAscList ((f , a) ∷ xs) = insert f a (fromAscList xs)

fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMapMaybe n A
fromFunc = tabulate ∘ _∘_ Maybe.just

reshape : {n : ℕ} {A : Set} → FinMapMaybe n A → (l : ℕ) → FinMapMaybe l A
reshape m        zero    = []
reshape []       (suc l) = nothing ∷ (reshape [] l)
reshape (x ∷ xs) (suc l) = x ∷ (reshape xs l)

union : {A : Set} {n : ℕ} → FinMapMaybe n A → FinMapMaybe n A → FinMapMaybe n A
union m1 m2 = tabulate (λ f → maybe′ just (lookupM f m2) (lookupM f m1))

restrict : {A : Set} {n m : ℕ} → (Fin n → A) → Vec (Fin n) m → FinMapMaybe n A
restrict f is = fromAscList (zip is (mapV f is))

delete : {A : Set} {n : ℕ} → Fin n → FinMapMaybe n A → FinMapMaybe n A
delete i m = m [ i ]≔ nothing

delete-many : {A : Set} {n m : ℕ} → Vec (Fin n) m → FinMapMaybe n A → FinMapMaybe n A
delete-many = flip (foldr (const _) delete)

lemma-insert-same : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → (f : Fin n) → {a : A} → lookupM f m ≡ just a → m ≡ insert f a m
lemma-insert-same         []       ()      p
lemma-insert-same {suc n} (x ∷ xs) zero    p = cong (flip _∷_ xs) p
lemma-insert-same         (x ∷ xs) (suc i) p = cong (_∷_ x) (lemma-insert-same xs i p)

lemma-lookupM-empty : {A : Set} {n : ℕ} → (i : Fin n) → lookupM {A} i empty ≡ nothing
lemma-lookupM-empty zero    = refl
lemma-lookupM-empty (suc i) = lemma-lookupM-empty i

lemma-lookupM-insert : {A : Set} {n : ℕ} → (i : Fin n) → (a : A) → (m : FinMapMaybe n A) → lookupM i (insert i a m) ≡ just a
lemma-lookupM-insert zero    a (x ∷ xs) = refl
lemma-lookupM-insert (suc i) a (x ∷ xs) = lemma-lookupM-insert i a xs

lemma-lookupM-insert-other : {A : Set} {n : ℕ} → (i j : Fin n) → (a : A) → (m : FinMapMaybe n A) → i ≢ j → lookupM i (insert j a m) ≡ lookupM i m
lemma-lookupM-insert-other zero    zero    a m        p = contradiction refl p
lemma-lookupM-insert-other zero    (suc j) a (x ∷ xs) p = refl
lemma-lookupM-insert-other (suc i) zero    a (x ∷ xs) p = refl
lemma-lookupM-insert-other (suc i) (suc j) a (x ∷ xs) p = lemma-lookupM-insert-other i j a xs (p ∘ cong suc)

lemma-lookupM-restrict : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (is : Vec (Fin n) m) → {a : A} → lookupM i (restrict f is) ≡ just a → f i ≡ a
lemma-lookupM-restrict i f []            p = contradiction (trans (sym p) (lemma-lookupM-empty i)) (λ ())
lemma-lookupM-restrict i f (i' ∷ is)     p with i ≟ i'
lemma-lookupM-restrict i f (.i ∷ is) {a} p | yes refl = just-injective (begin
   just (f i)
     ≡⟨ sym (lemma-lookupM-insert i (f i) (restrict f is)) ⟩
   lookupM i (insert i (f i) (restrict f is))
     ≡⟨ p ⟩
   just a ∎)
lemma-lookupM-restrict i f (i' ∷ is) {a} p | no i≢i' = lemma-lookupM-restrict i f is (begin
  lookupM i (restrict f is)
    ≡⟨ sym (lemma-lookupM-insert-other i i' (f i') (restrict f is) i≢i') ⟩
  lookupM i (insert i' (f i') (restrict f is))
    ≡⟨ p ⟩
  just a ∎)
lemma-lookupM-restrict-∈ : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (js : Vec (Fin n) m) → i ∈ js → lookupM i (restrict f js) ≡ just (f i)
lemma-lookupM-restrict-∈ i f [] ()
lemma-lookupM-restrict-∈ i f (j ∷ js)  p             with i ≟ j
lemma-lookupM-restrict-∈ i f (.i ∷ js) p             | yes refl = lemma-lookupM-insert i (f i) (restrict f js)
lemma-lookupM-restrict-∈ i f (j ∷ js) (Any.here i≡j) | no i≢j = contradiction i≡j i≢j
lemma-lookupM-restrict-∈ i f (j ∷ js) (Any.there p)  | no i≢j =
  trans (lemma-lookupM-insert-other i j (f j) (restrict f js) i≢j)
        (lemma-lookupM-restrict-∈ i f js p)

lemma-lookupM-restrict-∉ : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (js : Vec (Fin n) m) → i ∉ js → lookupM i (restrict f js) ≡ nothing
lemma-lookupM-restrict-∉ i f []       i∉[]  = lemma-lookupM-empty i
lemma-lookupM-restrict-∉ i f (j ∷ js) i∉jjs =
  trans (lemma-lookupM-insert-other i j (f j) (restrict f js) (All.head i∉jjs))
        (lemma-lookupM-restrict-∉ i f js (All.tail i∉jjs))

lemma-tabulate-∘ : {n : ℕ} {A : Set} → {f g : Fin n → A} → f ≗ g → tabulate f ≡ tabulate g
lemma-tabulate-∘ {zero}  {_} {f} {g} f≗g = refl
lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = cong₂ _∷_ (f≗g zero) (lemma-tabulate-∘ (f≗g ∘ suc))

lemma-lookupM-fromFunc : {n : ℕ} {A : Set} → (f : Fin n → A) → flip lookupM (fromFunc f) ≗ Maybe.just ∘ f
lemma-lookupM-fromFunc f zero = refl
lemma-lookupM-fromFunc f (suc i) = lemma-lookupM-fromFunc (f ∘ suc) i

lemma-lookupM-delete : {n : ℕ} {A : Set} {i j : Fin n} → (f : FinMapMaybe n A) → i ≢ j → lookupM i (delete j f) ≡ lookupM i f
lemma-lookupM-delete {i = zero}  {j = zero}  (_ ∷ _)  p = contradiction refl p
lemma-lookupM-delete {i = zero}  {j = suc j} (_ ∷ _)  p = refl
lemma-lookupM-delete {i = suc i} {j = zero}  (x ∷ xs) p = refl
lemma-lookupM-delete {i = suc i} {j = suc j} (x ∷ xs) p = lemma-lookupM-delete xs (p ∘ cong suc)

lemma-lookupM-delete-many : {n m : ℕ} {A : Set} (h : FinMapMaybe n A) → (i : Fin n) → (js : Vec (Fin n) m) → i ∉ js → lookupM i (delete-many js h) ≡ lookupM i h
lemma-lookupM-delete-many {n} h i []       i∉[]  = refl
lemma-lookupM-delete-many {n} h i (j ∷ js) i∉jjs =
  trans (lemma-lookupM-delete (delete-many js h) (All.head i∉jjs))
        (lemma-lookupM-delete-many h i js (All.tail i∉jjs))

lemma-reshape-id : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → reshape m n ≡ m
lemma-reshape-id []       = refl
lemma-reshape-id (x ∷ xs) = cong (_∷_ x) (lemma-reshape-id xs)

lemma-disjoint-union : {n m : ℕ} {A : Set} → (f : Fin n → A) → (t : Vec (Fin n) m) → union (restrict f t) (delete-many t (fromFunc f)) ≡ fromFunc f
lemma-disjoint-union {n} f t = lemma-tabulate-∘ inner
  where inner : (x : Fin n) → maybe′ just (lookupM x (delete-many t (fromFunc f))) (lookupM x (restrict f t)) ≡ just (f x)
        inner x with is-∈ _≟_ x t
        inner x | yes-∈ x∈t = cong (maybe′ just (lookupM x (delete-many t (fromFunc f)))) (lemma-lookupM-restrict-∈ x f t x∈t)
        inner x | no-∉ x∉t = begin
          maybe′ just (lookupM x (delete-many t (fromFunc f))) (lookupM x (restrict f t))
            ≡⟨ cong₂ (maybe′ just) (lemma-lookupM-delete-many (fromFunc f) x t x∉t) (lemma-lookupM-restrict-∉ x f t x∉t) ⟩
          maybe′ just (lookupM x (fromFunc f)) nothing
            ≡⟨ lemma-lookupM-fromFunc f x ⟩
          just (f x) ∎

lemma-exchange-maps : {n m : ℕ} → {A : Set} → {h h′ : FinMapMaybe n A} → {P : Fin n → Set} → (∀ j → P j → lookupM j h ≡ lookupM j h′) → {is : Vec (Fin n) m} → All P (toList is) → mapV (flip lookupM h) is ≡ mapV (flip lookupM h′) is
lemma-exchange-maps h≈h′ {[]}     All.[]         = refl
lemma-exchange-maps h≈h′ {i ∷ is} (pi All.∷ pis) = cong₂ _∷_ (h≈h′ i pi) (lemma-exchange-maps h≈h′ pis)

max_stars_repo_name: jvoigtlaender/bidiragda

max_issues_repo_name: jvoigtlaender/bidiragda

max_forks_repo_name: jvoigtlaender/bidiragda


text:
module HasDecidableValidation where

open import OscarPrelude
open import 𝓐ssertion
open import HasSatisfaction
open import Validation

record HasDecidableValidation (A : Set) ⦃ _ : HasSatisfaction A ⦄ : Set₁
 where
  field
    ⊨?_ : (x : A) → Dec $ ⊨ x

open HasDecidableValidation ⦃ … ⦄ public


text:
-- Andreas, 2015-06-29, issue reported by Nisse

-- {-# OPTIONS -v tc.polarity:20 -v tc.pos:10 #-}
-- {-# OPTIONS -v tc.conv.elim:25 --show-implicit #-}

data ⊥ : Set where

data _≡_ {a} {A : Set a} : A → A → Set a where
  refl : ∀ x → x ≡ x

subst : ∀ {a p} {A : Set a} (P : A → Set p) {x y : A} →
        x ≡ y → P x → P y
subst P (refl x) p = p

record _∼_ (A B : Set₁) : Set₁ where
  field
    to               : A → B
    from             : B → A
    right-inverse-of : ∀ x → x ≡ to (from x)

mutual

  record R (c : ⊥) : Set₂ where
    field
      P : F c → Set₁
      Q : {I J : F c} → S c I J → P I → P J → Set₁

    Q′ : ∀ {I J} → S c I J → P I → P J → Set₁
    Q′ s x y = subst P (_∼_.to (S∼≡ c) s) x ≡ y

    field

      Q∼Q′ : ∀ {I J} (s : S c I J) {x y} → Q s x y ∼ Q′ s x y

  F : ⊥ → Set₁
  F ()

  S : (c : ⊥) → F c → F c → Set₁
  S ()

  S∼≡ : (c : ⊥) {I J : F c} → S c I J ∼ (I ≡ J)
  S∼≡ ()

s : ∀ c I → S c I I
s c I = _∼_.from (S∼≡ c) (refl I)

q : ∀ c e I x → R.Q e (s c I) x x
q c e I x =
  _∼_.from (R.Q∼Q′ e (s c I))
           (subst (λ eq → subst (R.P e) eq x ≡ x)
                  (_∼_.right-inverse-of (S∼≡ c) (refl I))
                  (refl x))

-- ERROR WAS (due to faulty positivity analysis for projections):
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/Conversion.hs:770


text:
module Natural where

open import Equality
open import Cubical.Data.Nat.Properties public
open import Data.Empty
open import Data.Nat as ℕ public hiding (_+_; _*_; _^_)
open import Data.Nat.Properties public hiding (+-assoc; +-suc)
open import Data.Unit
open import Function
open import Syntax

instance
  ℕ-plus-syntax : plus-syntax-simple ℕ ℕ ℕ
  ℕ-plus-syntax = record { _+_ = ℕ._+_ }

  ℕ-times-syntax : times-syntax-simple ℕ ℕ ℕ
  ℕ-times-syntax = record { _*_ = ℕ._*_ }

  ℕ-raise-syntax : raise-syntax-simple ℕ ℕ ℕ
  ℕ-raise-syntax = record { _^_ = ℕ._^_ }

+-cross : (a b c d : ℕ) → (a + b) + (c + d) ≡ (a + c) + (b + d)
+-cross a b c d =
    (a + b) + (c + d)
  ≡⟨ sym (+-assoc a _ _) ⟩
    a + (b + (c + d))
  ≡⟨ cong (a +_) (+-assoc b _ _) ⟩
    a + ((b + c) + d)
  ≡⟨ cong (a +_) (cong (_+ d) ⟨ +-comm b c ⟩) ⟩
    a + ((c + b) + d)
  ≡⟨ cong (a +_) (sym (+-assoc c _ _)) ⟩
    a + (c + (b + d))
  ≡⟨ +-assoc a _ _ ⟩
    (a + c) + (b + d)
  ∎

instance
  ℕ-Number : Number ℕ
  ℕ-Number = record { Constraint = λ _ → ⊤ ; fromNat = λ x → x }


text:
{-# OPTIONS --universe-polymorphism #-}

module Issue286 where

open import Common.Level

data Bool : Set where
  true false : Bool

{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  true  #-}
{-# BUILTIN FALSE false #-}

data _≡_ {ℓ : Level} {A : Set ℓ} : A → A → Set ℓ where
  refl : {a : A} → a ≡ a

{-# BUILTIN EQUALITY _≡_  #-}

primitive
  primEraseEquality : ∀ {a} {A : Set a} {x y : A} → x ≡ y → x ≡ y

{-# BUILTIN STRING String #-}

primitive
  primStringEquality : String → String → Bool

data Maybe (A : Set) : Set where
  just    : A → Maybe A
  nothing : Maybe A

_≟_ : (s₁ s₂ : String) → Maybe (s₁ ≡ s₂)
s₁ ≟ s₂ with primStringEquality s₁ s₂
... | true  = just (primEraseEquality trustMe)
  where postulate trustMe : _ ≡ _
... | false = nothing

_≟′_ : (s₁ s₂ : String) → Maybe (s₁ ≡ s₂)
s₁ ≟′ s₂ with s₁ ≟ s₂
s  ≟′ .s | just refl = just refl
_  ≟′ _  | nothing   = nothing

test : Maybe ("" ≡ "")
test = "" ≟′ ""

ok : test ≡ just refl
ok = refl

max_stars_repo_name: bennn/agda

max_issues_repo_name: bennn/agda

max_forks_repo_name: bennn/agda


text:
{-# OPTIONS -v5 #-}

module Debug where

postulate Foo : Set


text:
{-# OPTIONS --cubical --no-exact-split --safe #-}
module Cubical.Data.Queue.Base where

open import Cubical.Foundations.Everything

open import Cubical.Foundations.SIP
open import Cubical.Structures.Queue

open import Cubical.Data.Unit
open import Cubical.Data.Sum
open import Cubical.Data.List
open import Cubical.Data.Prod.Base hiding (_×_) renaming (_×Σ_ to _×_)

module _ (A : Type ℓ) (Aset : isSet A) where
 open Queues-on A Aset

 -- following Cavallo we can now define 1Lists and 2Lists as Queues on A
 -- and prove that there is a queue-iso between them, this then gives us a path
 1List : Queue
 1List = (Q , emp , push , pop)
  where
   Q = List A
   emp = []
   push = _∷_
   pop : Q → Unit ⊎ (Q × A)
   pop [] = inl tt
   pop (x ∷ []) = inr ([] , x)
   pop (x ∷ x' ∷ xs) = pop-map-forward (push x) (pop (x' ∷ xs))

 -- for later convenience
 Q₁ = typ 1List
 emp₁ = str 1List .fst
 push₁ = str 1List .snd .fst
 pop₁ = str 1List .snd .snd

 -- Now for 2Lists
 data Q₂ : Set ℓ where
   Q₂⟨_,_⟩ : (xs ys : List A) → Q₂
   tilt : ∀ xs ys z → Q₂⟨ xs ++ [ z ] , ys ⟩ ≡ Q₂⟨ xs , ys ++ [ z ] ⟩
   trunc : (q q' : Q₂) (α β : q ≡ q') → α ≡ β

 multitilt : (xs ys zs : List A) → Q₂⟨ xs ++ rev zs , ys ⟩ ≡ Q₂⟨ xs , ys ++ zs ⟩
 multitilt xs ys [] = cong₂ Q₂⟨_,_⟩ (++-unit-r xs) (sym (++-unit-r ys))
 multitilt xs ys (z ∷ zs) =
   cong (λ ws → Q₂⟨ ws , ys ⟩) (sym (++-assoc xs (rev zs) [ z ]))
   ∙ tilt (xs ++ rev zs) ys z
   ∙ multitilt xs (ys ++ [ z ]) zs
   ∙ cong (λ ws → Q₂⟨ xs , ws ⟩) (++-assoc ys [ z ] zs)

  -- push into the first list, pop from the second if possible

 emp₂ : Q₂
 emp₂ = Q₂⟨ [] , [] ⟩

 push₂ : A → Q₂ → Q₂
 push₂ a Q₂⟨ xs , ys ⟩ = Q₂⟨ a ∷ xs , ys ⟩
 push₂ a (tilt xs ys z i) = tilt (a ∷ xs) ys z i
 push₂ a (trunc q q' α β i j) =
   trunc _ _ (cong (push₂ a) α) (cong (push₂ a) β) i j

 pop₂Flush : List A → Unit ⊎ (Q₂ × A)
 pop₂Flush [] = inl tt
 pop₂Flush (x ∷ xs) = inr (Q₂⟨ [] , xs ⟩ , x)

 pop₂ : Q₂ → Unit ⊎ (Q₂ × A)
 pop₂ Q₂⟨ xs , [] ⟩ = pop₂Flush (rev xs)
 pop₂ Q₂⟨ xs , y ∷ ys ⟩ = inr (Q₂⟨ xs , ys ⟩ , y)
 pop₂ (tilt xs [] z i) = path i
   where
   path : pop₂Flush (rev (xs ++ [ z ])) ≡ inr (Q₂⟨ xs , [] ⟩ , z)
   path =
     cong pop₂Flush (rev-++ xs [ z ])
     ∙ cong (λ q → inr (q , z)) (sym (multitilt [] [] (rev xs)))
     ∙ cong (λ ys → inr (Q₂⟨ ys , [] ⟩ , z)) (rev-rev xs)
 pop₂ (tilt xs (y ∷ ys) z i) = inr (tilt xs ys z i , y)
 pop₂ (trunc q q' α β i j) =
   isOfHLevelSum 0
     (isProp→isSet isPropUnit)
     (isOfHLevelΣ 2 trunc λ _ → Aset)
     (pop₂ q) (pop₂ q') (cong pop₂ α) (cong pop₂ β)
    i j

 2List : Queue
 2List = (Q₂ , emp₂ , push₂ , pop₂)

 -- We construct an equivalence Q₁≃Q₂ and prove that this is a queue-iso
 quot : Q₁ → Q₂
 quot xs = Q₂⟨ xs , [] ⟩

 eval : Q₂ → Q₁
 eval Q₂⟨ xs , ys ⟩ = xs ++ rev ys
 eval (tilt xs ys z i) = path i
   where
   path : (xs ++ [ z ]) ++ rev ys ≡ xs ++ rev (ys ++ [ z ])
   path =
     ++-assoc xs [ z ] (rev ys)
     ∙ cong (_++_ xs) (sym (rev-++ ys [ z ]))
 eval (trunc q q' α β i j) = -- truncated case
   isOfHLevelList 0 Aset (eval q) (eval q') (cong eval α) (cong eval β) i j

 quot∘eval : ∀ q → quot (eval q) ≡ q
 quot∘eval Q₂⟨ xs , ys ⟩ = multitilt xs [] ys
 quot∘eval (tilt xs ys z i) = -- truncated case
   isOfHLevelPathP'
     {A = λ i → quot (eval (tilt xs ys z i)) ≡ tilt xs ys z i}
     0
     (λ _ → trunc _ _)
     (multitilt (xs ++ [ z ]) [] ys) (multitilt xs [] (ys ++ [ z ]))
     .fst i
 quot∘eval (trunc q q' α β i j) = -- truncated case
   isOfHLevelPathP'
     {A = λ i →
       PathP (λ j → quot (eval (trunc q q' α β i j)) ≡ trunc q q' α β i j)
         (quot∘eval q) (quot∘eval q')}
     0
     (λ _ → isOfHLevelPathP' 1 (λ _ → isOfHLevelSuc 2 trunc _ _) _ _)
     (cong quot∘eval α) (cong quot∘eval β)
     .fst i j

 eval∘quot : ∀ xs → eval (quot xs) ≡ xs
 eval∘quot = ++-unit-r

 -- We get our desired equivalence
 quotEquiv : Q₁ ≃ Q₂
 quotEquiv = isoToEquiv (iso quot eval quot∘eval eval∘quot)

 -- Now it only remains to prove that this is a queue-iso
 quot∘emp : quot emp₁ ≡ emp₂
 quot∘emp = refl

 quot∘push : ∀ x xs → quot (push₁ x xs) ≡ push₂ x (quot xs)
 quot∘push x xs = refl

 quot∘pop : ∀ xs → pop-map-forward quot (pop₁ xs) ≡ pop₂ (quot xs)
 quot∘pop [] = refl
 quot∘pop (x ∷ []) = refl
 quot∘pop (x ∷ x' ∷ xs) =
   pop-map-forward-∘ quot (push₁ x) (pop₁ (x' ∷ xs))
   ∙ sym (pop-map-forward-∘ (push₂ x) quot (pop₁ (x' ∷ xs)))
   ∙ cong (pop-map-forward (push₂ x)) (quot∘pop (x' ∷ xs))
   ∙ lemma x x' (rev xs)
   where
   lemma : ∀ x x' ys
     → pop-map-forward (push₂ x) (pop₂Flush (ys ++ [ x' ]))
       ≡ pop₂Flush ((ys ++ [ x' ]) ++ [ x ])
   lemma x x' [] i = inr (tilt [] [] x i , x')
   lemma x x' (y ∷ ys) i = inr (tilt [] (ys ++ [ x' ]) x i , y)

 quotEquiv-is-queue-iso : queue-iso 1List 2List quotEquiv
 quotEquiv-is-queue-iso = quot∘emp , quot∘push , quot∘pop

 -- And we get the desired Path
 Path-1List-2List : 1List ≡ 2List
 Path-1List-2List = SIP queue-structure queue-iso  Queue-is-SNS 1List 2List .fst
                   (quotEquiv , quotEquiv-is-queue-iso)

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
open import Oscar.Prelude
open import Oscar.Class.IsPrecategory
open import Oscar.Class.Surjection
open import Oscar.Class.Smap
open import Oscar.Class.Surjtranscommutativity
open import Oscar.Class.Surjextensionality
open import Oscar.Class.Transitivity

module Oscar.Class.IsPrefunctor where

module _
  {𝔬₁} {𝔒₁ : Ø 𝔬₁}
  {𝔯₁} (_∼₁_ : 𝔒₁ → 𝔒₁ → Ø 𝔯₁)
  {ℓ₁} (_∼̇₁_ : ∀ {x y} → x ∼₁ y → x ∼₁ y → Ø ℓ₁)
  (_↦₁_ : Transitivity.type _∼₁_)
  {𝔬₂} {𝔒₂ : Ø 𝔬₂}
  {𝔯₂} (_∼₂_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂)
  {ℓ₂} (_∼̇₂_ : ∀ {x y} → x ∼₂ y → x ∼₂ y → Ø ℓ₂)
  (_↦₂_ : Transitivity.type _∼₂_)
  {surjection : Surjection.type 𝔒₁ 𝔒₂}
  (smap : Smap.type _∼₁_ _∼₂_ surjection surjection)
  where
  record IsPrefunctor : Ø 𝔬₁ ∙̂ 𝔯₁ ∙̂ ℓ₁ ∙̂ 𝔬₂ ∙̂ 𝔯₂ ∙̂ ℓ₂ where
    constructor ∁
    field
      overlap ⦃ `IsPrecategory₁ ⦄ : IsPrecategory _∼₁_ _∼̇₁_ _↦₁_
      overlap ⦃ `IsPrecategory₂ ⦄ : IsPrecategory _∼₂_ _∼̇₂_ _↦₂_
      overlap ⦃ `𝓢urjtranscommutativity ⦄ : Surjtranscommutativity.class _∼₁_ _∼₂_ _∼̇₂_ smap _↦₁_ _↦₂_
      ⦃ `𝓢urjextensionality ⦄ : Surjextensionality.class _∼₁_ _∼̇₁_ _∼₂_ _∼̇₂_ surjection smap