text:
------------------------------------------------------------------------
-- Groups
------------------------------------------------------------------------

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

open import Equality

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

open Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude as P hiding (id; _∘_) renaming (_×_ to _⊗_)

import Bijection eq as B
open import Equivalence eq as Eq using (_≃_)
open import Function-universe eq as F hiding (id; _∘_)
open import Groupoid eq using (Groupoid)
open import H-level eq
open import H-level.Closure eq
open import Integer.Basics eq using (+_; -[1+_])
open import Univalence-axiom eq

private
  variable
    a g₁ g₂ : Level
    A       : Type a
    g x y   : A
    k       : Kind

------------------------------------------------------------------------
-- Groups

-- Groups.
--
-- Note that the carrier type is required to be a set (following the
-- HoTT book).

record Group g : Type (lsuc g) where
  infix  8 _⁻¹
  infixr 7 _∘_

  field
    Carrier        : Type g
    Carrier-is-set : Is-set Carrier
    _∘_            : Carrier → Carrier → Carrier
    id             : Carrier
    _⁻¹            : Carrier → Carrier
    left-identity  : ∀ x → (id ∘ x) ≡ x
    right-identity : ∀ x → (x ∘ id) ≡ x
    assoc          : ∀ x y z → (x ∘ (y ∘ z)) ≡ ((x ∘ y) ∘ z)
    left-inverse   : ∀ x → ((x ⁻¹) ∘ x) ≡ id
    right-inverse  : ∀ x → (x ∘ (x ⁻¹)) ≡ id

  -- Groups are groupoids.

  groupoid : Groupoid lzero g
  groupoid = record
    { Object         = ⊤
    ; _∼_            = λ _ _ → Carrier
    ; id             = id
    ; _∘_            = _∘_
    ; _⁻¹            = _⁻¹
    ; left-identity  = left-identity
    ; right-identity = right-identity
    ; assoc          = assoc
    ; left-inverse   = left-inverse
    ; right-inverse  = right-inverse
    }

  open Groupoid groupoid public
    hiding (Object; _∼_; id; _∘_; _⁻¹; left-identity; right-identity;
            assoc; left-inverse; right-inverse)

private
  variable
    G G₁ G₁′ G₂ G₂′ G₃ : Group g

-- The type of groups can be expressed using a nested Σ-type.

Group-as-Σ :
  Group g ≃
  ∃ λ (A : Set g) →
  let A = ⌞ A ⌟ in
  ∃ λ (_∘_ : A → A → A) →
  ∃ λ (id : A) →
  ∃ λ (_⁻¹ : A → A) →
    (∀ x → (id ∘ x) ≡ x) ⊗
    (∀ x → (x ∘ id) ≡ x) ⊗
    (∀ x y z → (x ∘ (y ∘ z)) ≡ ((x ∘ y) ∘ z)) ⊗
    (∀ x → ((x ⁻¹) ∘ x) ≡ id) ⊗
    (∀ x → (x ∘ (x ⁻¹)) ≡ id)
Group-as-Σ =
  Eq.↔→≃
    (λ G → let open Group G in
         (Carrier , Carrier-is-set)
       , _∘_
       , id
       , _⁻¹
       , left-identity
       , right-identity
       , assoc
       , left-inverse
       , right-inverse)
    _
    refl
    refl

------------------------------------------------------------------------
-- Group homomorphisms and isomorphisms

-- Group homomorphisms (generalised to several kinds of underlying
-- "functions").

record Homomorphic (k : Kind) (G₁ : Group g₁) (G₂ : Group g₂) :
                   Type (g₁ ⊔ g₂) where
  private
    module G₁ = Group G₁
    module G₂ = Group G₂

  field
    related : G₁.Carrier ↝[ k ] G₂.Carrier

  to : G₁.Carrier → G₂.Carrier
  to = to-implication related

  field
    homomorphic :
      ∀ x y → to (x G₁.∘ y) ≡ to x G₂.∘ to y

open Homomorphic public using (related; homomorphic)
open Homomorphic using (to)

-- The type of (generalised) group homomorphisms can be expressed
-- using a nested Σ-type.

Homomorphic-as-Σ :
  {G₁ : Group g₁} {G₂ : Group g₂} →
  Homomorphic k G₁ G₂ ≃
  let module G₁ = Group G₁
      module G₂ = Group G₂
  in
  ∃ λ (f : G₁.Carrier ↝[ k ] G₂.Carrier) →
    ∀ x y →
    to-implication f (x G₁.∘ y) ≡
    to-implication f x G₂.∘ to-implication f y
Homomorphic-as-Σ =
  Eq.↔→≃
    (λ G₁↝G₂ → G₁↝G₂ .related , G₁↝G₂ .homomorphic)
    _
    refl
    refl

-- A variant of Homomorphic.

infix 4 _↝[_]ᴳ_ _→ᴳ_ _≃ᴳ_

_↝[_]ᴳ_ : Group g₁ → Kind → Group g₂ → Type (g₁ ⊔ g₂)
_↝[_]ᴳ_ = flip Homomorphic

-- Group homomorphisms.

_→ᴳ_ : Group g₁ → Group g₂ → Type (g₁ ⊔ g₂)
_→ᴳ_ = _↝[ implication ]ᴳ_

-- Group isomorphisms.

_≃ᴳ_ : Group g₁ → Group g₂ → Type (g₁ ⊔ g₂)
_≃ᴳ_ = _↝[ equivalence ]ᴳ_

-- "Functions" of type G₁ ↝[ k ]ᴳ G₂ can be converted to group
-- homomorphisms.

↝ᴳ→→ᴳ : G₁ ↝[ k ]ᴳ G₂ → G₁ →ᴳ G₂
↝ᴳ→→ᴳ f .related     = to f
↝ᴳ→→ᴳ f .homomorphic = f .homomorphic

-- _↝[ k ]ᴳ_ is reflexive.

↝ᴳ-refl : G ↝[ k ]ᴳ G
↝ᴳ-refl                 .related         = F.id
↝ᴳ-refl {G = G} {k = k} .homomorphic x y =
  to-implication {k = k} F.id (x ∘ y)  ≡⟨ cong (_$ _) $ to-implication-id k ⟩

  x ∘ y                                ≡⟨ sym $ cong₂ (λ f g → f _ ∘ g _)
                                            (to-implication-id k)
                                            (to-implication-id k) ⟩∎
  to-implication {k = k} F.id x ∘
  to-implication {k = k} F.id y        ∎
  where
  open Group G

-- _↝[ k ]ᴳ_ is transitive.

↝ᴳ-trans : G₁ ↝[ k ]ᴳ G₂ → G₂ ↝[ k ]ᴳ G₃ → G₁ ↝[ k ]ᴳ G₃
↝ᴳ-trans {G₁ = G₁} {k = k} {G₂ = G₂} {G₃ = G₃}
  G₁↝G₂ G₂↝G₃ = λ where
    .related         → G₂↝G₃ .related F.∘ G₁↝G₂ .related
    .homomorphic x y →
      to-implication (G₂↝G₃ .related F.∘ G₁↝G₂ .related) (x G₁.∘ y)  ≡⟨ cong (_$ _) $ to-implication-∘ k ⟩

      to G₂↝G₃ (to G₁↝G₂ (x G₁.∘ y))                                 ≡⟨ cong (to G₂↝G₃) $ homomorphic G₁↝G₂ _ _ ⟩

      to G₂↝G₃ (to G₁↝G₂ x G₂.∘ to G₁↝G₂ y)                          ≡⟨ homomorphic G₂↝G₃ _ _ ⟩

      to G₂↝G₃ (to G₁↝G₂ x) G₃.∘ to G₂↝G₃ (to G₁↝G₂ y)               ≡⟨ sym $ cong₂ (λ f g → f _ G₃.∘ g _)
                                                                          (to-implication-∘ k)
                                                                          (to-implication-∘ k) ⟩∎
      to-implication (G₂↝G₃ .related F.∘ G₁↝G₂ .related) x G₃.∘
      to-implication (G₂↝G₃ .related F.∘ G₁↝G₂ .related) y           ∎
  where
  module G₁ = Group G₁
  module G₂ = Group G₂
  module G₃ = Group G₃

-- _≃ᴳ_ is symmetric.

≃ᴳ-sym : G₁ ≃ᴳ G₂ → G₂ ≃ᴳ G₁
≃ᴳ-sym {G₁ = G₁} {G₂ = G₂} G₁≃G₂ = λ where
    .related         → inverse (G₁≃G₂ .related)
    .homomorphic x y → _≃_.injective (G₁≃G₂ .related)
      (to G₁≃G₂ (_≃_.from (G₁≃G₂ .related) (x G₂.∘ y))                   ≡⟨ _≃_.right-inverse-of (G₁≃G₂ .related) _ ⟩

       x G₂.∘ y                                                          ≡⟨ sym $ cong₂ G₂._∘_
                                                                              (_≃_.right-inverse-of (G₁≃G₂ .related) _)
                                                                              (_≃_.right-inverse-of (G₁≃G₂ .related) _) ⟩
       to G₁≃G₂ (_≃_.from (G₁≃G₂ .related) x) G₂.∘
       to G₁≃G₂ (_≃_.from (G₁≃G₂ .related) y)                            ≡⟨ sym $ G₁≃G₂ .homomorphic _ _ ⟩∎

       to G₁≃G₂
         (_≃_.from (G₁≃G₂ .related) x G₁.∘ _≃_.from (G₁≃G₂ .related) y)  ∎)
  where
  module G₁ = Group G₁
  module G₂ = Group G₂

-- Group homomorphisms preserve identity elements.

→ᴳ-id :
  (G₁↝G₂ : G₁ ↝[ k ]ᴳ G₂) →
  to G₁↝G₂ (Group.id G₁) ≡ Group.id G₂
→ᴳ-id {G₁ = G₁} {G₂ = G₂} G₁↝G₂ =
  G₂.idempotent⇒≡id
    (to G₁↝G₂ G₁.id G₂.∘ to G₁↝G₂ G₁.id  ≡⟨ sym $ G₁↝G₂ .homomorphic _ _ ⟩
     to G₁↝G₂ (G₁.id G₁.∘ G₁.id)         ≡⟨ cong (to G₁↝G₂) $ G₁.left-identity _ ⟩∎
     to G₁↝G₂ G₁.id                      ∎)
  where
  module G₁ = Group G₁
  module G₂ = Group G₂

-- Group homomorphisms are homomorphic with respect to the inverse
-- operators.

→ᴳ-⁻¹ :
  ∀ (G₁↝G₂ : G₁ ↝[ k ]ᴳ G₂) x →
  to G₁↝G₂ (Group._⁻¹ G₁ x) ≡ Group._⁻¹ G₂ (to G₁↝G₂ x)
→ᴳ-⁻¹ {G₁ = G₁} {G₂ = G₂} G₁↝G₂ x = G₂.⁻¹∘≡id→≡
  (to G₁↝G₂ x G₂.⁻¹ G₂.⁻¹ G₂.∘ to G₁↝G₂ (x G₁.⁻¹)  ≡⟨ cong (G₂._∘ to G₁↝G₂ (x G₁.⁻¹)) $ G₂.involutive _ ⟩
   to G₁↝G₂ x G₂.∘ to G₁↝G₂ (x G₁.⁻¹)              ≡⟨ sym $ G₁↝G₂ .homomorphic _ _ ⟩
   to G₁↝G₂ (x G₁.∘ x G₁.⁻¹)                       ≡⟨ cong (to G₁↝G₂) (G₁.right-inverse _) ⟩
   to G₁↝G₂ G₁.id                                  ≡⟨ →ᴳ-id G₁↝G₂ ⟩∎
   G₂.id                                           ∎)
  where
  module G₁ = Group G₁
  module G₂ = Group G₂

-- Group homomorphisms are homomorphic with respect to exponentiation.

→ᴳ-^ :
  ∀ (G₁↝G₂ : G₁ ↝[ k ]ᴳ G₂) x i →
  to G₁↝G₂ (Group._^_ G₁ x i) ≡
  Group._^_ G₂ (to G₁↝G₂ x) i
→ᴳ-^ {G₁ = G₁} {G₂ = G₂} G₁↝G₂ x = lemma₂
  where
  module G₁ = Group G₁
  module G₂ = Group G₂

  lemma₁ : ∀ n → to G₁↝G₂ (y G₁.^+ n) ≡ to G₁↝G₂ y G₂.^+ n
  lemma₁ zero =
    to G₁↝G₂ G₁.id  ≡⟨ →ᴳ-id G₁↝G₂ ⟩∎
    G₂.id    ∎
  lemma₁ {y = y} (suc n) =
    to G₁↝G₂ (y G₁.∘ y G₁.^+ n)           ≡⟨ G₁↝G₂ .homomorphic _ _ ⟩
    to G₁↝G₂ y G₂.∘ to G₁↝G₂ (y G₁.^+ n)  ≡⟨ cong (_ G₂.∘_) $ lemma₁ n ⟩∎
    to G₁↝G₂ y G₂.∘ to G₁↝G₂ y G₂.^+ n    ∎

  lemma₂ : ∀ i → to G₁↝G₂ (x G₁.^ i) ≡ to G₁↝G₂ x G₂.^ i
  lemma₂ (+ n)    = lemma₁ n
  lemma₂ -[1+ n ] =
    to G₁↝G₂ ((x G₁.⁻¹) G₁.^+ suc n)  ≡⟨ lemma₁ (suc n) ⟩
    to G₁↝G₂ (x G₁.⁻¹) G₂.^+ suc n    ≡⟨ cong (G₂._^+ suc n) $ →ᴳ-⁻¹ G₁↝G₂ _ ⟩∎
    (to G₁↝G₂ x G₂.⁻¹) G₂.^+ suc n    ∎

-- Group equality can be expressed in terms of equality of pairs of
-- carrier types and binary operators (assuming extensionality).

≡≃,∘≡,∘ :
  {G₁ G₂ : Group g} →
  Extensionality g g →
  let module G₁ = Group G₁
      module G₂ = Group G₂
  in
  (G₁ ≡ G₂) ≃ ((G₁.Carrier , G₁._∘_) ≡ (G₂.Carrier , G₂._∘_))
≡≃,∘≡,∘ {g = g} {G₁ = G₁} {G₂ = G₂} ext =
  G₁ ≡ G₂                                                    ↝⟨ inverse $ Eq.≃-≡ Group≃ ⟩

  ((G₁.Carrier , G₁._∘_) , _) ≡ ((G₂.Carrier , G₂._∘_) , _)  ↔⟨ (inverse $
                                                                 ignore-propositional-component $
                                                                 The-rest-propositional _) ⟩□
  (G₁.Carrier , G₁._∘_) ≡ (G₂.Carrier , G₂._∘_)              □
  where
  module G₁ = Group G₁
  module G₂ = Group G₂

  Carrier-∘ = ∃ λ (C : Type g) → (C → C → C)

  The-rest : Carrier-∘ → Type g
  The-rest (C , _∘_) =
    ∃ λ ((id , _⁻¹) : C ⊗ (C → C)) →
      Is-set C ⊗
      (∀ x → (id ∘ x) ≡ x) ⊗
      (∀ x → (x ∘ id) ≡ x) ⊗
      (∀ x y z → (x ∘ (y ∘ z)) ≡ ((x ∘ y) ∘ z)) ⊗
      (∀ x → ((x ⁻¹) ∘ x) ≡ id) ⊗
      (∀ x → (x ∘ (x ⁻¹)) ≡ id)

  Group≃ : Group g ≃ Σ Carrier-∘ The-rest
  Group≃ = Eq.↔→≃
    (λ G → let open Group G in
         (Carrier , _∘_)
       , (id , _⁻¹)
       , Carrier-is-set , left-identity , right-identity , assoc
       , left-inverse , right-inverse)
    _
    refl
    refl

  The-rest-propositional : ∀ C → Is-proposition (The-rest C)
  The-rest-propositional C R₁ R₂ =
    Σ-≡,≡→≡
      (cong₂ _,_ id-unique inverse-unique)
      ((×-closure 1 (H-level-propositional ext 2) $
        ×-closure 1 (Π-closure ext 1 λ _ →
                     G₂′.Carrier-is-set) $
        ×-closure 1 (Π-closure ext 1 λ _ →
                     G₂′.Carrier-is-set) $
        ×-closure 1 (Π-closure ext 1 λ _ →
                     Π-closure ext 1 λ _ →
                     Π-closure ext 1 λ _ →
                     G₂′.Carrier-is-set) $
        ×-closure 1 (Π-closure ext 1 λ _ →
                     G₂′.Carrier-is-set) $
                    (Π-closure ext 1 λ _ →
                     G₂′.Carrier-is-set))
         _ _)
    where
    module G₁′ = Group (_≃_.from Group≃ (C , R₁))
    module G₂′ = Group (_≃_.from Group≃ (C , R₂))

    id-unique : G₁′.id ≡ G₂′.id
    id-unique = G₂′.idempotent⇒≡id (G₁′.left-identity G₁′.id)

    inverse-unique : G₁′._⁻¹ ≡ G₂′._⁻¹
    inverse-unique = apply-ext ext λ x → G₂′.⁻¹-unique-right
      (x G₁′.∘ x G₁′.⁻¹  ≡⟨ G₁′.right-inverse _ ⟩
       G₁′.id            ≡⟨ id-unique ⟩∎
       G₂′.id            ∎)

-- Group isomorphisms are equivalent to equalities (assuming
-- extensionality and univalence).

≃ᴳ≃≡ :
  {G₁ G₂ : Group g} →
  Extensionality g g →
  Univalence g →
  (G₁ ≃ᴳ G₂) ≃ (G₁ ≡ G₂)
≃ᴳ≃≡ {G₁ = G₁} {G₂ = G₂} ext univ =
  G₁ ≃ᴳ G₂                                                              ↝⟨ Homomorphic-as-Σ ⟩

  (∃ λ (eq : G₁.Carrier ≃ G₂.Carrier) →
     ∀ x y →
     _≃_.to eq (x G₁.∘ y) ≡ _≃_.to eq x G₂.∘ _≃_.to eq y)               ↝⟨ (∃-cong λ eq → Π-cong ext eq λ _ → Π-cong ext eq λ _ →
                                                                            ≡⇒≃ $ sym $ cong (_≡ _≃_.to eq _ G₂.∘ _≃_.to eq _) $ cong (_≃_.to eq) $
                                                                            cong₂ G₁._∘_
                                                                              (_≃_.left-inverse-of eq _)
                                                                              (_≃_.left-inverse-of eq _)) ⟩
  (∃ λ (eq : G₁.Carrier ≃ G₂.Carrier) →
     ∀ x y → _≃_.to eq (_≃_.from eq x G₁.∘ _≃_.from eq y) ≡ x G₂.∘ y)   ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ →
                                                                            Eq.extensionality-isomorphism ext) ⟩
  (∃ λ (eq : G₁.Carrier ≃ G₂.Carrier) →
     ∀ x →
     (λ y → _≃_.to eq (_≃_.from eq x G₁.∘ _≃_.from eq y)) ≡ (x G₂.∘_))  ↝⟨ (∃-cong λ _ →
                                                                            Eq.extensionality-isomorphism ext) ⟩
  (∃ λ (eq : G₁.Carrier ≃ G₂.Carrier) →
     (λ x y → _≃_.to eq (_≃_.from eq x G₁.∘ _≃_.from eq y)) ≡ G₂._∘_)   ↝⟨ (∃-cong λ eq → ≡⇒≃ $ cong (_≡ _) $ sym $ lemma eq) ⟩

  (∃ λ (eq : G₁.Carrier ≃ G₂.Carrier) →
     subst (λ A → A → A → A) (≃⇒≡ univ eq) G₁._∘_ ≡ G₂._∘_)             ↝⟨ (Σ-cong (inverse $ ≡≃≃ univ) λ _ → Eq.id) ⟩

  (∃ λ (eq : G₁.Carrier ≡ G₂.Carrier) →
     subst (λ A → A → A → A) eq G₁._∘_ ≡ G₂._∘_)                        ↔⟨ B.Σ-≡,≡↔≡ ⟩

  ((G₁.Carrier , G₁._∘_) ≡ (G₂.Carrier , G₂._∘_))                       ↝⟨ inverse $ ≡≃,∘≡,∘ ext ⟩□

  G₁ ≡ G₂                                                               □
  where
  module G₁ = Group G₁
  module G₂ = Group G₂

  lemma : ∀ _ → _
  lemma = λ eq → apply-ext ext λ x → apply-ext ext λ y →
    subst (λ A → A → A → A) (≃⇒≡ univ eq) G₁._∘_ x y      ≡⟨ cong (_$ y) subst-→ ⟩

    subst (λ A → A → A) (≃⇒≡ univ eq)
      (subst P.id (sym (≃⇒≡ univ eq)) x G₁.∘_) y          ≡⟨ subst-→ ⟩

    subst P.id (≃⇒≡ univ eq)
      (subst P.id (sym (≃⇒≡ univ eq)) x G₁.∘
       subst P.id (sym (≃⇒≡ univ eq)) y)                  ≡⟨ cong₂ (λ f g → f (g x G₁.∘ g y))
                                                               (trans (apply-ext ext λ _ → subst-id-in-terms-of-≡⇒↝ equivalence) $
                                                                cong _≃_.to $ _≃_.right-inverse-of (≡≃≃ univ) _)
                                                               (trans (apply-ext ext λ _ → subst-id-in-terms-of-inverse∘≡⇒↝ equivalence) $
                                                                cong _≃_.from $ _≃_.right-inverse-of (≡≃≃ univ) _) ⟩∎
    _≃_.to eq (_≃_.from eq x G₁.∘ _≃_.from eq y)          ∎

------------------------------------------------------------------------
-- Abelian groups

-- The property of being abelian.

Abelian : Group g → Type g
Abelian G =
  ∀ x y → x ∘ y ≡ y ∘ x
  where
  open Group G

-- If two groups are isomorphic, and one is abelian, then the other
-- one is abelian.

≃ᴳ→Abelian→Abelian : G₁ ≃ᴳ G₂ → Abelian G₁ → Abelian G₂
≃ᴳ→Abelian→Abelian {G₁ = G₁} {G₂ = G₂} G₁≃G₂ ∘-comm x y =
  _≃_.injective (G₂≃G₁ .related)
    (to G₂≃G₁ (x G₂.∘ y)         ≡⟨ G₂≃G₁ .homomorphic _ _ ⟩
     to G₂≃G₁ x G₁.∘ to G₂≃G₁ y  ≡⟨ ∘-comm _ _ ⟩
     to G₂≃G₁ y G₁.∘ to G₂≃G₁ x  ≡⟨ sym $ G₂≃G₁ .homomorphic _ _ ⟩∎
     to G₂≃G₁ (y G₂.∘ x)         ∎)
  where
  module G₁ = Group G₁
  module G₂ = Group G₂

  G₂≃G₁ = ≃ᴳ-sym G₁≃G₂

------------------------------------------------------------------------
-- A group construction

-- The direct product of two groups.

infixr 2 _×_

_×_ : Group g₁ → Group g₂ → Group (g₁ ⊔ g₂)
G₁ × G₂ = λ where
    .Carrier          → G₁.Carrier ⊗ G₂.Carrier
    .Carrier-is-set   → ×-closure 2 G₁.Carrier-is-set G₂.Carrier-is-set
    ._∘_              → Σ-zip G₁._∘_ G₂._∘_
    .id               → G₁.id , G₂.id
    ._⁻¹              → Σ-map G₁._⁻¹ G₂._⁻¹
    .left-identity _  → cong₂ _,_
                          (G₁.left-identity _) (G₂.left-identity _)
    .right-identity _ → cong₂ _,_
                          (G₁.right-identity _) (G₂.right-identity _)
    .assoc _ _ _      → cong₂ _,_ (G₁.assoc _ _ _) (G₂.assoc _ _ _)
    .left-inverse _   → cong₂ _,_
                          (G₁.left-inverse _) (G₂.left-inverse _)
    .right-inverse _  → cong₂ _,_
                          (G₁.right-inverse _) (G₂.right-inverse _)
  where
  open Group

  module G₁ = Group G₁
  module G₂ = Group G₂

-- The direct product operator preserves group homomorphisms.

↝-× :
  G₁ ↝[ k ]ᴳ G₂ → G₁′ ↝[ k ]ᴳ G₂′ →
  (G₁ × G₁′) ↝[ k ]ᴳ (G₂ × G₂′)
↝-× {G₁ = G₁} {k = k} {G₂ = G₂} {G₁′ = G₁′} {G₂′ = G₂′}
  G₁↝G₂ G₁′↝G₂′ = λ where
  .related →
    G₁↝G₂ .related ×-cong G₁′↝G₂′ .related
  .homomorphic x@(x₁ , x₂) y@(y₁ , y₂) →
    to-implication (G₁↝G₂ .related ×-cong G₁′↝G₂′ .related)
      (Σ-zip (Group._∘_ G₁) (Group._∘_ G₁′) x y)                   ≡⟨ cong (_$ _) $ to-implication-×-cong k ⟩

    Σ-map (to G₁↝G₂) (to G₁′↝G₂′)
      (Σ-zip (Group._∘_ G₁) (Group._∘_ G₁′) x y)                   ≡⟨⟩

    to G₁↝G₂   (Group._∘_ G₁  x₁ y₁) ,
    to G₁′↝G₂′ (Group._∘_ G₁′ x₂ y₂)                               ≡⟨ cong₂ _,_
                                                                        (G₁↝G₂   .homomorphic _ _)
                                                                        (G₁′↝G₂′ .homomorphic _ _) ⟩
    Group._∘_ G₂  (to G₁↝G₂   x₁) (to G₁↝G₂   y₁) ,
    Group._∘_ G₂′ (to G₁′↝G₂′ x₂) (to G₁′↝G₂′ y₂)                  ≡⟨⟩

    Group._∘_ (G₂ × G₂′)
      (to G₁↝G₂ x₁ , to G₁′↝G₂′ x₂)
      (to G₁↝G₂ y₁ , to G₁′↝G₂′ y₂)                                ≡⟨ sym $ cong₂ (λ f g → Group._∘_ (G₂ × G₂′) (f _) (g _))
                                                                        (to-implication-×-cong k)
                                                                        (to-implication-×-cong k) ⟩∎
    Group._∘_ (G₂ × G₂′)
      (to-implication (G₁↝G₂ .related ×-cong G₁′↝G₂′ .related) x)
      (to-implication (G₁↝G₂ .related ×-cong G₁′↝G₂′ .related) y)  ∎

-- Exponentiation for the direct product of G₁ and G₂ can be expressed
-- in terms of exponentiation for G₁ and exponentiation for G₂.

^-× :
  ∀ (G₁ : Group g₁) (G₂ : Group g₂) {x y} i →
  Group._^_ (G₁ × G₂) (x , y) i ≡
  (Group._^_ G₁ x i , Group._^_ G₂ y i)
^-× G₁ G₂ = helper
  where
  module G₁  = Group G₁
  module G₂  = Group G₂
  module G₁₂ = Group (G₁ × G₂)

  +-helper : ∀ n → (x , y) G₁₂.^+ n ≡ (x G₁.^+ n , y G₂.^+ n)
  +-helper                 zero    = refl _
  +-helper {x = x} {y = y} (suc n) =
    (x , y) G₁₂.∘ (x , y) G₁₂.^+ n         ≡⟨ cong (_ G₁₂.∘_) $ +-helper n ⟩
    (x , y) G₁₂.∘ (x G₁.^+ n , y G₂.^+ n)  ≡⟨⟩
    (x G₁.∘ x G₁.^+ n , y G₂.∘ y G₂.^+ n)  ∎

  helper : ∀ i → (x , y) G₁₂.^ i ≡ (x G₁.^ i , y G₂.^ i)
  helper (+ n)    = +-helper n
  helper -[1+ n ] = +-helper (suc n)

------------------------------------------------------------------------
-- The centre of a group

-- Centre ext G is the centre of the group G, sometimes denoted Z(G).

Centre :
  Extensionality g g →
  Group g → Group g
Centre ext G = λ where
    .Carrier        → ∃ λ (x : Carrier) → ∀ y → x ∘ y ≡ y ∘ x
    .Carrier-is-set → Σ-closure 2 Carrier-is-set λ _ →
                      Π-closure ext 2 λ _ →
                      mono₁ 2 Carrier-is-set
    ._∘_            → Σ-zip _∘_ λ {x y} hyp₁ hyp₂ z →
                        (x ∘ y) ∘ z  ≡⟨ sym $ assoc _ _ _ ⟩
                        x ∘ (y ∘ z)  ≡⟨ cong (x ∘_) $ hyp₂ z ⟩
                        x ∘ (z ∘ y)  ≡⟨ assoc _ _ _ ⟩
                        (x ∘ z) ∘ y  ≡⟨ cong (_∘ y) $ hyp₁ z ⟩
                        (z ∘ x) ∘ y  ≡⟨ sym $ assoc _ _ _ ⟩∎
                        z ∘ (x ∘ y)  ∎
    .id             → id
                    , λ x →
                        id ∘ x  ≡⟨ left-identity _ ⟩
                        x       ≡⟨ sym $ right-identity _ ⟩∎
                        x ∘ id  ∎
    ._⁻¹            → Σ-map _⁻¹ λ {x} hyp y →
                        x ⁻¹ ∘ y        ≡⟨ cong (x ⁻¹ ∘_) $ sym $ involutive _ ⟩
                        x ⁻¹ ∘ y ⁻¹ ⁻¹  ≡⟨ sym ∘⁻¹ ⟩
                        (y ⁻¹ ∘ x) ⁻¹   ≡⟨ cong _⁻¹ $ sym $ hyp (y ⁻¹) ⟩
                        (x ∘ y ⁻¹) ⁻¹   ≡⟨ ∘⁻¹ ⟩
                        y ⁻¹ ⁻¹ ∘ x ⁻¹  ≡⟨ cong (_∘ x ⁻¹) $ involutive _ ⟩∎
                        y ∘ x ⁻¹        ∎
    .left-identity  → λ _ →
                      Σ-≡,≡→≡ (left-identity _)
                        ((Π-closure ext 1 λ _ → Carrier-is-set) _ _)
    .right-identity → λ _ →
                      Σ-≡,≡→≡ (right-identity _)
                        ((Π-closure ext 1 λ _ → Carrier-is-set) _ _)
    .assoc          → λ _ _ _ →
                      Σ-≡,≡→≡ (assoc _ _ _)
                        ((Π-closure ext 1 λ _ → Carrier-is-set) _ _)
    .left-inverse   → λ _ →
                      Σ-≡,≡→≡ (left-inverse _)
                        ((Π-closure ext 1 λ _ → Carrier-is-set) _ _)
    .right-inverse  → λ _ →
                      Σ-≡,≡→≡ (right-inverse _)
                        ((Π-closure ext 1 λ _ → Carrier-is-set) _ _)
  where
  open Group G

-- The centre of an abelian group is isomorphic to the group.

Abelian→Centre≃ :
  (ext : Extensionality g g) (G : Group g) →
  Abelian G → Centre ext G ≃ᴳ G
Abelian→Centre≃ ext G abelian = ≃ᴳ-sym λ where
    .Homomorphic.related         → inverse equiv
    .Homomorphic.homomorphic _ _ →
      cong (_ ,_) ((Π-closure ext 1 λ _ → Carrier-is-set) _ _)
  where
  open Group G

  equiv =
    (∃ λ (x : Carrier) → ∀ y → x ∘ y ≡ y ∘ x)  ↔⟨ (drop-⊤-right λ _ →
                                                   _⇔_.to contractible⇔↔⊤ $
                                                   Π-closure ext 0 λ _ →
                                                   propositional⇒inhabited⇒contractible
                                                     Carrier-is-set
                                                     (abelian _ _)) ⟩□
    Carrier                                    □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module examplesPaperJFP.CatNonTerm where

open import examplesPaperJFP.BasicIO hiding (main)
open import examplesPaperJFP.Console hiding (main)
open import examplesPaperJFP.NativeIOSafe
module _ where
  {-# NON_TERMINATING #-}
  cat  :  IO ConsoleInterface Unit
  cat  =  exec getLine                         λ{ nothing    → return unit ;
                                                (just line) →
           exec (putStrLn line)                 λ _ →
           cat                                }

ext: agda

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
open import Data.Nat
open import Data.Bool
open import Data.Product
open import Function
open import Data.List hiding (lookup)
open import Data.List.All
open import Data.List.Membership.Propositional
open import Data.Maybe.Categorical
open import Category.Monad
open import Agda.Primitive
open import Size
open import Codata.Thunk
open import Codata.Delay
open import Codata.Delay.Categorical

module Typed.STLC.Delay where

data Ty : Set where
  numt boolt : Ty
  _⟶_ : Ty → Ty → Ty

data Expr : List Ty → Ty → Set where
  add : ∀ {Γ} →
    Expr Γ numt → Expr Γ numt →
    Expr Γ numt
  num : ∀ {Γ} →
    ℕ →
    Expr Γ numt
  true′ false′ : ∀ {Γ} →
    Expr Γ boolt
  if′_then_else : ∀ {Γ} →
    ∀ {t} → Expr Γ boolt → Expr Γ t → Expr Γ t →
    Expr Γ t
  ƛ_ : ∀ {Γ t₁ t₂} →
    Expr (t₁ ∷ Γ) t₂ →
    Expr Γ (t₁ ⟶ t₂)
  _∙_ : ∀ {Γ t₁ t₂} →
    Expr Γ (t₁ ⟶ t₂) → Expr Γ t₁ →
    Expr Γ t₂
  var : ∀ {Γ t} →
    t ∈ Γ →
    Expr Γ t

mutual
  data Val : Ty → Set where
    numv : ℕ → Val numt
    boolv : Bool → Val boolt
    ⟨ƛ_,_⟩ : ∀ {Γ t₁ t₂} → Expr (t₁ ∷ Γ) t₂ → Env Γ → Val (t₁ ⟶ t₂)

  Env : List Ty → Set
  Env Γ = All Val Γ

ReaderT : ∀ {a} {M : Set a → Set a} (R : Set a) → RawMonad M → RawMonad (λ A → R → M A)
ReaderT _ M = record { return = λ a _ → return a ;
                       _>>=_ = λ f k r → f r >>= λ x → k x r }
  where open RawMonad M

module _ {Γ : List Ty} {i} where
  open RawMonad {lzero} (ReaderT (Env Γ) (Sequential.monad {i})) public

M : List Ty → Size → Set → Set
M Γ i A = Env Γ → Delay A i

getEnv : ∀ {Γ i} → M Γ i (Env Γ)
getEnv E = now E

withEnv : ∀ {Γ Γ' i A} → Env Γ → M Γ i A → M Γ' i A
withEnv E m _ = m E

get : ∀ {Γ t i} → t ∈ Γ → M Γ i (Val t)
get x E = now (lookup E x)

mutual
  eval : ∀ {Γ t} → Expr Γ t → ∀ {i} → M Γ i (Val t)
  eval (add e₁ e₂) = do
    numv n₁ ← eval e₁
    numv n₂ ← eval e₁
    return (numv (n₁ + n₂))
  eval (num n) = do
    return (numv n)
  eval true′ = do
    return (boolv true)
  eval false′ = do
    return (boolv false)
  eval (if′ c then t else e) = do
    (boolv b) ← eval c
    if b then eval t else eval e
  eval (ƛ e) = do
    E ← getEnv
    return ⟨ƛ e , E ⟩
  eval (f ∙ a) = do
    ⟨ƛ e , E ⟩ ← eval f
    v ← eval a
    withEnv (v ∷ E) (▹eval e)
  eval (var x) = do
    get x

  ▹eval : ∀ {Γ i t} → Expr Γ t → M Γ i (Val t)
  ▹eval e E = later λ where .force → eval e E


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

open import Prelude hiding (_×_)

module Categories.HSets {ℓ : Level} where

open import Categories
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Data.Sigma.Properties
open import Categories.Product
open import Categories.Exponential

hSetPreCategory : PreCategory (ℓsuc ℓ) ℓ
hSetPreCategory .PreCategory.Ob = hSet _
hSetPreCategory .PreCategory.Hom (X , _) (Y , _) = X → Y
hSetPreCategory .PreCategory.Id = id
hSetPreCategory .PreCategory.Comp f g = f ∘ g
hSetPreCategory .PreCategory.assoc-Comp _ _ _ = refl
hSetPreCategory .PreCategory.Comp-Id _ = refl
hSetPreCategory .PreCategory.Id-Comp _ = refl
hSetPreCategory .PreCategory.Hom-Set {X} {Y} = hLevelPi 2 λ _ → Y .snd

open PreCategory hSetPreCategory

_⟨×⟩_ : isSet A → isSet B → isSet (A Prelude.× B)
xs ⟨×⟩ ys = isOfHLevelΣ 2 xs (const ys)

module _ {X Y : Ob} where
  iso-iso : (X ≅ Y) ⇔ (fst X ⇔ fst Y)
  iso-iso .fun (f , g , f∘g , g∘f) = iso f g (λ x i → g∘f i x) (λ x i → f∘g i x)
  iso-iso .inv (iso f g g∘f f∘g) = f , g  , (λ i x → f∘g x i) , (λ i x → g∘f x i)
  iso-iso .rightInv _ = refl
  iso-iso .leftInv  _ = refl

  univ⇔ : (X ≡ Y) ⇔ (X ≅ Y)
  univ⇔ = equivToIso (≃ΣProp≡ (λ _ → isPropIsSet)) ⟨ trans-⇔ ⟩
          equivToIso univalence ⟨ trans-⇔ ⟩
          sym-⇔ (iso⇔equiv (snd X)) ⟨ trans-⇔ ⟩
          sym-⇔ iso-iso

hSetCategory : Category (ℓsuc ℓ) ℓ
hSetCategory .Category.preCategory = hSetPreCategory
hSetCategory .Category.univalent = isoToEquiv univ⇔

hSetProd : HasProducts hSetCategory
hSetProd .HasProducts.product X Y .Product.obj = (X .fst Prelude.× Y .fst) , X .snd ⟨×⟩ Y .snd
hSetProd .HasProducts.product X Y .Product.proj₁ = fst
hSetProd .HasProducts.product X Y .Product.proj₂ = snd
hSetProd .HasProducts.product X Y .Product.ump f g .fst z = f z , g z
hSetProd .HasProducts.product X Y .Product.ump f g .snd .fst .fst = refl
hSetProd .HasProducts.product X Y .Product.ump f g .snd .fst .snd = refl
hSetProd .HasProducts.product X Y .Product.ump f g .snd .snd (f≡ , g≡) i x = f≡ (~ i) x , g≡ (~ i) x

hSetExp : HasExponentials hSetCategory hSetProd
hSetExp  X Y .Exponential.obj = (X .fst → Y .fst) , hLevelPi 2 λ _ → Y .snd
hSetExp  X Y .Exponential.eval (f , x) = f x
hSetExp  X Y .Exponential.uniq X₁ f .fst = curry f
hSetExp  X Y .Exponential.uniq X₁ f .snd .fst = refl
hSetExp  X Y .Exponential.uniq X₁ f .snd .snd {y} x = cong curry (sym x)

open import Categories.Pullback

hSetHasPullbacks : HasPullbacks hSetCategory
hSetHasPullbacks {X = X} {Y = Y} {Z = Z} f g .Pullback.P = ∃[ ab ] (f (fst ab) ≡ g (snd ab)) , isOfHLevelΣ 2 (X .snd ⟨×⟩ Y .snd) λ xy → isProp→isSet (Z .snd (f (xy .fst)) (g (xy .snd)))
hSetHasPullbacks f g .Pullback.p₁ ((x , _) , _) = x
hSetHasPullbacks f g .Pullback.p₂ ((_ , y) , _) = y
hSetHasPullbacks f g .Pullback.commute = funExt snd
hSetHasPullbacks f g .Pullback.ump {A = A} h₁ h₂ p .fst x = (h₁ x , h₂ x) , λ i → p i x
hSetHasPullbacks f g .Pullback.ump {A = A} h₁ h₂ p .snd .fst .fst = refl
hSetHasPullbacks f g .Pullback.ump {A = A} h₁ h₂ p .snd .fst .snd = refl
hSetHasPullbacks {Z = Z} f g .Pullback.ump {A = A} h₁ h₂ p .snd .snd {i} (p₁e , p₂e) = funExt (λ x → ΣProp≡ (λ _ → Z .snd _ _) λ j → p₁e (~ j) x , p₂e (~ j) x)

hSetTerminal : Terminal
hSetTerminal .fst = Lift _ ⊤ , isProp→isSet λ _ _ → refl
hSetTerminal .snd .fst x .lower = tt
hSetTerminal .snd .snd y = funExt λ _ → refl

hSetInitial : Initial
hSetInitial .fst = Lift _ ⊥ , λ ()
hSetInitial .snd .fst ()
hSetInitial .snd .snd y i ()

open import HITs.PropositionalTruncation
open import Categories.Coequalizer

∃!′ : (A : Type a) → (A → Type b) → Type (a ℓ⊔ b)
∃!′ A P = ∥ Σ A P ∥ Prelude.× AtMostOne P

lemma23 : ∀ {p} {P : A → hProp p} → ∃!′ A (fst ∘ P) → Σ A (fst ∘ P)
lemma23 {P = P} (x , y) = rec (λ xs ys → ΣProp≡ (snd ∘ P) (y (xs .fst) (ys .fst) (xs .snd) (ys .snd))) id x

module _ {A : Type a} {P : A → Type b} (R : ∀ x → P x → hProp c) where
  uniqueChoice : (Π[ x ⦂ A ] (∃!′ (P x) (λ u → R x u .fst))) →
                 Σ[ f ⦂ Π[ x ⦂ A ] P x ] Π[ x ⦂ A ] (R x (f x) .fst)
  uniqueChoice H = fst ∘ mid , snd ∘ mid
    where
    mid : Π[ x ⦂ A ] Σ[ u ⦂ P x ] (R x u .fst)
    mid x = lemma23 {P = R x} (H x)

open import HITs.PropositionalTruncation.Sugar

module CoeqProofs {X Y : Ob} (f : X ⟶ Y) where
  KernelPair : Pullback hSetCategory {X = X} {Z = Y} {Y = X} f f
  KernelPair = hSetHasPullbacks f f

  Im : Ob
  Im = ∃[ b ] ∥ fiber f b ∥ , isOfHLevelΣ 2 (Y .snd) λ _ → isProp→isSet squash

  im : X ⟶ Im
  im x = f x , ∣ x , refl ∣

  open Pullback KernelPair

  lem : ∀ {H : Ob} (h : X ⟶ H) → h ∘ p₁ ≡ h ∘ p₂ → Σ[ f ⦂ (Im ⟶ H) ] Π[ x ⦂ Im .fst ] (∀ y → im y ≡ x → h y ≡ f x)
  lem {H = H} h eq = uniqueChoice R prf
    where
    R : Im .fst → H .fst → hProp _
    R w x .fst = ∀ y → im y ≡ w → h y ≡ x
    R w x .snd = hLevelPi 1 λ _ → hLevelPi 1 λ _ → H .snd _ _

    prf : Π[ x ⦂ Im .fst ] ∃!′ (H .fst) (λ u → ∀ y → im y ≡ x → h y ≡ u)
    prf (xy , p) .fst = (λ { (z , r) → h z , λ y imy≡xyp → cong (_$ ((y , z) , cong fst imy≡xyp ; sym r)) eq }) ∥$∥ p
    prf (xy , p) .snd x₁ x₂ Px₁ Px₂ = rec (H .snd x₁ x₂) (λ { (z , zs) → sym (Px₁ z (ΣProp≡ (λ _ → squash) zs)) ; Px₂ z (ΣProp≡ (λ _ → squash) zs) } ) p

  lem₂ : ∀ (H : Ob) (h : X ⟶ H) (i : Im ⟶ H) (x : Im .fst) (hi : h ≡ i ∘ im) (eq : h ∘ p₁ ≡ h ∘ p₂) → i x ≡ lem {H = H} h eq .fst x
  lem₂ H h i x hi eq = rec (H .snd _ _) (λ { (y , ys) → (cong i (ΣProp≡ (λ _ → squash) (sym ys)) ; sym (cong (_$ y) hi)) ; lem {H = H} h eq .snd x y (ΣProp≡ (λ _ → squash) ys) }) (x .snd)

  hSetCoeq : Coequalizer hSetCategory {X = P} {Y = X} p₁ p₂
  hSetCoeq .Coequalizer.obj = Im
  hSetCoeq .Coequalizer.arr = im
  hSetCoeq .Coequalizer.equality = funExt λ x → ΣProp≡ (λ _ → squash) λ i → commute i x
  hSetCoeq .Coequalizer.coequalize {H = H} {h = h} eq = lem {H = H} h eq .fst
  hSetCoeq .Coequalizer.universal {H = H} {h = h} {eq = eq} = funExt λ x → lem {H = H} h eq .snd (im x) x refl
  hSetCoeq .Coequalizer.unique {H = H} {h = h} {i = i} {eq = eq} prf = funExt λ x → lem₂ H h i x prf eq
open CoeqProofs using (hSetCoeq) public

module PullbackSurjProofs {X Y : Ob} (f : X ⟶ Y) (fSurj : Surjective f) where
  KernelPair : Pullback hSetCategory {X = X} {Z = Y} {Y = X} f f
  KernelPair = hSetHasPullbacks f f

  open Pullback KernelPair

  p₁surj : Surjective p₁
  p₁surj y = ∣ ((y , y) , refl) , refl ∣

  p₂surj : Surjective p₂
  p₂surj y = ∣ ((y , y) , refl) , refl ∣

open import Relation.Binary
open import Cubical.HITs.SetQuotients

module _ {A : Type a} {R : A → A → Type b} {C : Type c}
         (isSetC : isSet C)
         (f : A → C)
         (coh : ∀ x y → R x y → f x ≡ f y)
         where

  recQuot : A / R → C
  recQuot [ a ] = f a
  recQuot (eq/ a b r i) = coh a b r i
  recQuot (squash/ xs ys x y i j) = isSetC (recQuot xs) (recQuot ys) (cong recQuot x) (cong recQuot y) i j

open import Path.Reasoning

module ExtactProofs {X : Ob} {R : X .fst → X .fst → hProp ℓ}
  (symR : Symmetric (λ x y → R x y .fst))
  (transR : Transitive (λ x y → R x y .fst))
  (reflR : Reflexive (λ x y → R x y .fst))
  where
  ℛ : X .fst → X .fst → Type ℓ
  ℛ x y = R x y .fst

  Src : Ob
  Src .fst = ∃[ x,y ] (uncurry ℛ x,y)
  Src .snd = isOfHLevelΣ 2 (X .snd ⟨×⟩ X .snd) λ _ → isProp→isSet (R _ _ .snd)

  pr₁ pr₂ : Src ⟶ X
  pr₁ = fst ∘ fst
  pr₂ = snd ∘ fst

  ROb : Ob
  ROb = X .fst / ℛ , squash/

  CR : Coequalizer hSetCategory {X = Src} {Y = X} pr₁ pr₂
  CR .Coequalizer.obj = ROb
  CR .Coequalizer.arr = [_]
  CR .Coequalizer.equality = funExt λ { ((x , y) , x~y) → eq/ x y x~y}
  CR .Coequalizer.coequalize {H = H} {h = h} e = recQuot (H .snd) h λ x y x~y → cong (_$ ((x , y) , x~y)) e
  CR .Coequalizer.universal {H = H} {h = h} {eq = e} = refl
  CR .Coequalizer.unique {H = H} {h = h} {i = i} {eq = e} p = funExt (elimSetQuotientsProp (λ _ → H .snd _ _) λ x j → p (~ j) x)

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
{-# OPTIONS --type-in-type #-}
module Record where

infixr 2 _,_
record Σ (A : Set)(B : A → Set) : Set where
  constructor _,_
  field fst : A
        snd : B fst

open Σ

data ⊤ : Set where
  tt : ⊤

∃ : {A : Set}(B : A → Set) → Set
∃ B = Σ _ B

infix 10 _≡_

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

trans : ∀ {A B C}{a : A}{b : B}{c : C} → a ≡ b → b ≡ c → a ≡ c
trans refl p = p

sym : ∀ {A B}{a : A}{b : B} → a ≡ b → b ≡ a
sym refl = refl

resp : ∀ {A}{B : A → Set}{a a' : A} →
       (f : (a : A) → B a) → a ≡ a' → f a ≡ f a'
resp f refl = refl

Cat : Set
Cat =
  ∃ λ (Obj : Set) →
  ∃ λ (Hom : Obj → Obj → Set) →
  ∃ λ (id : ∀ X → Hom X X) →
  ∃ λ (_○_ : ∀ {X Y Z} → Hom Y Z → Hom X Y → Hom X Z) →
  ∃ λ (idl : ∀ {X Y}{f : Hom X Y} → id Y ○ f ≡ f) →
  ∃ λ (idr : ∀ {X Y}{f : Hom X Y} → f ○ id X ≡ f) →
  ∃ λ (assoc : ∀ {W X Y Z}{f : Hom W X}{g : Hom X Y}{h : Hom Y Z} →
                (h ○ g) ○ f ≡ h ○ (g ○ f)) →
  ⊤

Obj : (C : Cat) → Set
Obj C = fst C

Hom : (C : Cat) → Obj C → Obj C → Set
Hom C = fst (snd C)

id : (C : Cat) → ∀ X → Hom C X X
id C = fst (snd (snd C))

comp : (C : Cat) → ∀ {X Y Z} → Hom C Y Z → Hom C X Y → Hom C X Z
comp C = fst (snd (snd (snd C)))

idl : (C : Cat) → ∀ {X Y}{f : Hom C X Y} → comp C (id C Y) f ≡ f
idl C = fst (snd (snd (snd (snd C))))

idr : (C : Cat) → ∀ {X Y}{f : Hom C X Y} → comp C f (id C X) ≡ f
idr C = fst (snd (snd (snd (snd (snd C)))))

assoc : (C : Cat) → ∀ {W X Y Z}{f : Hom C W X}{g : Hom C X Y}{h : Hom C Y Z} →
        comp C (comp C h g) f ≡ comp C h (comp C g f)
assoc C = fst (snd (snd (snd (snd (snd (snd C))))))

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Basics where

data Zero : Set where
record One : Set where constructor <>
data Two : Set where tt ff : Two

data Nat : Set where
  ze : Nat
  su : Nat -> Nat

data _+_ (S T : Set) : Set where
  inl : S -> S + T
  inr : T -> S + T

record Sg (S : Set)(T : S -> Set) : Set where
  constructor _,_
  field
    fst : S
    snd : T fst
open Sg public
_*_ : Set -> Set -> Set
S * T = Sg S \ _ -> T
infixr 4 _,_ _*_

data _==_ {X : Set}(x : X) : X -> Set where
  refl : x == x


text:
-- Homotopy type theory

-- https://github.com/agda/cubical

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

module TypeTheory.HoTT.Base where

-- agda-stdlib
open import Level renaming (zero to lzero; suc to lsuc)
open import Data.Product
open import Relation.Binary.PropositionalEquality

private
  variable
    a b : Level

fiber : {A : Set a} {B : Set b} (f : A → B) (y : B) → Set (a ⊔ b)
fiber f y = ∃ λ x → f x ≡ y

isContr : Set a → Set a
isContr A = Σ A λ x → ∀ y → x ≡ y

isProp : Set a → Set a
isProp A = (x y : A) → x ≡ y

isSet : Set a → Set a
isSet A = (x y : A) → isProp (x ≡ y)


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

module Dodo.Binary.Equality where

-- Stdlib imports
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Level using (Level; _⊔_)
open import Function using (_∘_)
open import Relation.Unary using (Pred)
open import Relation.Binary using (Rel; REL)
open import Relation.Binary using (Symmetric)
-- Local imports
open import Dodo.Unary.Equality

infix 4 _⊆₂'_ _⊆₂_ _⇔₂_ _⊇₂_

-- | Binary relation subset helper. Generally, use `_⊆₂_` (below).
--
--
-- # Design decision: Explicit variables
--
-- `x` and `y` are passed /explicitly/. If they were implicit, Agda tries (and often fails) to
-- instantiate them at inappropriate applications.
_⊆₂'_ : {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b}
  → (P : REL A B ℓ₁)
  → (R : REL A B ℓ₂)
  → Set _
_⊆₂'_ {A = A} {B = B} P R = ∀ (x : A) (y : B) → P x y → R x y

-- | Binary relation subset
--
-- Note that this does /not/ describe structural equality between inhabitants, only
-- "(directed) co-inhabitation".
-- `P ⊆₂ Q` denotes: If `P x y` is inhabited, then `Q x y` is inhabited.
--
-- Whatever these inhabitants are, is irrelevant w.r.t. the subset constraint.
--
--
-- # Design decision: Include P and R in the type
--
-- Somehow, Agda cannot infer P and R from `P ⇒ R`, and requires them explicitly passed.
-- For proof convenience, wrap the proof in this structure, which explicitly conveys P and R
-- to the type-checker.
data _⊆₂_ {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b} (P : REL A B ℓ₁) (R : REL A B ℓ₂) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
  ⊆: : P ⊆₂' R → P ⊆₂ R

-- | Binary relation equality
--
-- Note that this does /not/ describe structural equality between inhabitants, only
-- "co-inhabitation".
-- `P ⇔₂ Q` denotes: `P x y` is inhabited iff `Q x y` is inhabited.
--
-- Whatever these inhabitants are, is irrelevant w.r.t. the equality constraint.
--
--
-- # Design decision: Include P and R in the type
--
-- Somehow, Agda cannot infer P and R from `P ⇔ R`, and requires them explicitly passed.
-- For proof convenience, wrap the proof in this structure, which explicitly conveys P and R
-- to the type-checker.
data _⇔₂_ {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b} (P : REL A B ℓ₁) (R : REL A B ℓ₂) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
  ⇔: : P ⊆₂' R → R ⊆₂' P → P ⇔₂ R

-- | Binary relation superset
_⊇₂_ : {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b} (P : REL A B ℓ₁) (R : REL A B ℓ₂) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
P ⊇₂ R = R ⊆₂ P

-- # Helpers

-- | Unwraps the `⊆:` constructor
un-⊆₂ : ∀ {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b} {P : REL A B ℓ₁} {R : REL A B ℓ₂}
  → P ⊆₂ R
    -------
  → P ⊆₂' R
un-⊆₂ (⊆: P⊆R) = P⊆R

-- | Unlifts a function over `⊆₂` to its unwrapped variant over `⊆₂'`.
unlift-⊆₂ : ∀ {a b c d ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : REL C D ℓ₃} {S : REL C D ℓ₄}
  → ( P ⊆₂ Q → R ⊆₂ S )
    ---------------------
  → ( P ⊆₂' Q → R ⊆₂' S )
unlift-⊆₂ f P⊆Q = un-⊆₂ (f (⊆: P⊆Q))

-- | Lifts a function over `⊆₂'` to its wrapped variant over `⊆₂`.
lift-⊆₂ : ∀ {a b c d ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : REL C D ℓ₃} {S : REL C D ℓ₄}
  → ( P ⊆₂' Q → R ⊆₂' S )
    ---------------------
  → ( P ⊆₂ Q → R ⊆₂ S )
lift-⊆₂ f (⊆: P⊆Q) = ⊆: (f P⊆Q)

-- | Introduces an equality `⇔₂` from both bi-directional components.
⇔₂-intro : {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b}
  → {P : REL A B ℓ₁} {R : REL A B ℓ₂}
  → P ⊆₂ R
  → R ⊆₂ P
    ------
  → P ⇔₂ R
⇔₂-intro (⊆: P⊆R) (⊆: R⊆P) = ⇔: P⊆R R⊆P

-- | Construct an equality `⇔₂` from a mapping over both bi-directional components.
⇔₂-compose : ∀ {a b c d ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : REL C D ℓ₃} {S : REL C D ℓ₄}
  → ( P ⊆₂ Q → R ⊆₂ S )
  → ( Q ⊆₂ P → S ⊆₂ R )
  → P ⇔₂ Q
    -------------------
  → R ⇔₂ S
⇔₂-compose ⊆-proof ⊇-proof (⇔: P⊆Q R⊆S) = ⇔₂-intro (⊆-proof (⊆: P⊆Q)) (⊇-proof (⊆: R⊆S))

-- | Construct a /binary/ equality `⇔₂` from a mapping over both bi-directional components of a /unary/ relation.
⇔₂-compose-⇔₁ : ∀ {a b c ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} {A : Set a} {B : Set b} {C : Set c}
    {P : Pred A ℓ₁} {Q : Pred A ℓ₂} {R : REL B C ℓ₃} {S : REL B C ℓ₄}
  → ( P ⊆₁ Q → R ⊆₂ S )
  → ( Q ⊆₁ P → S ⊆₂ R )
  → P ⇔₁ Q
    -------------------
  → R ⇔₂ S
⇔₂-compose-⇔₁ ⊆-proof ⊇-proof (⇔: P⊆Q R⊆S) = ⇔₂-intro (⊆-proof (⊆: P⊆Q)) (⊇-proof (⊆: R⊆S))

-- | Construct a /unary/ equalty `⇔₁` from a mapping over both bi-directional components of a /binary/ relation.
⇔₁-compose-⇔₂ : ∀ {a b c ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} {A : Set a} {B : Set b} {C : Set c}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : Pred C ℓ₃} {S : Pred C ℓ₄}
  → ( P ⊆₂ Q → R ⊆₁ S )
  → ( Q ⊆₂ P → S ⊆₁ R )
  → P ⇔₂ Q
    -------------------
  → R ⇔₁ S
⇔₁-compose-⇔₂ ⊆-proof ⊇-proof (⇔: P⊆Q R⊆S) = ⇔₁-intro (⊆-proof (⊆: P⊆Q)) (⊇-proof (⊆: R⊆S))

-- # Properties

-- ## Properties: ⊆₂

module _ {a b ℓ : Level} {A : Set a} {B : Set b} {R : REL A B ℓ} where

  ⊆₂-refl : R ⊆₂ R
  ⊆₂-refl = ⊆: (λ _ _ Rxy → Rxy)

module _ {a b ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b} {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : REL A B ℓ₃} where

  ⊆₂-trans : P ⊆₂ Q → Q ⊆₂ R → P ⊆₂ R
  ⊆₂-trans (⊆: P⊆Q) (⊆: Q⊆R) = ⊆: (λ x y Pxy → Q⊆R x y (P⊆Q x y Pxy))

-- ## Properties: ⇔₂

module _ {a b ℓ : Level} {A : Set a} {B : Set b} {R : REL A B ℓ} where

  ⇔₂-refl : R ⇔₂ R
  ⇔₂-refl = ⇔₂-intro ⊆₂-refl ⊆₂-refl

module _ {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b} {Q : REL A B ℓ₁} {R : REL A B ℓ₂} where

  -- | Symmetry of the `_⇔₂_` operation.
  --
  --
  -- # Design decision: No Symmetric
  --
  -- Do /not/ use `Symmetric _⇔₂_` as its type. It messes up the universe levels.
  ⇔₂-sym : Q ⇔₂ R → R ⇔₂ Q
  ⇔₂-sym (⇔: Q⊆R R⊆Q) = ⇔: R⊆Q Q⊆R

module _ {a b ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : REL A B ℓ₃} where

  ⇔₂-trans : P ⇔₂ Q → Q ⇔₂ R → P ⇔₂ R
  ⇔₂-trans (⇔: P⊆Q Q⊆P) (⇔: Q⊆R R⊆Q) =
    ⇔₂-intro (⊆₂-trans (⊆: P⊆Q) (⊆: Q⊆R)) (⊆₂-trans (⊆: R⊆Q) (⊆: Q⊆P))

-- # Operations

-- ## Operations: ⇔₂ and ⊆₂ conversion

⇔₂-to-⊆₂ : {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b} {P : REL A B ℓ₁} {Q : REL A B ℓ₂}
  → P ⇔₂ Q
    ------
  → P ⊆₂ Q
⇔₂-to-⊆₂ (⇔: P⊆Q _) = ⊆: P⊆Q

⇔₂-to-⊇₂ : {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b} {P : REL A B ℓ₁} {Q : REL A B ℓ₂}
  → P ⇔₂ Q
    ------
  → Q ⊆₂ P
⇔₂-to-⊇₂ (⇔: _ Q⊆P) = ⊆: Q⊆P

-- ## Operations: ⊆₂

⊆₂-apply : {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂}
  → P ⊆₂ Q
  → {x : A} {y : B}
  → P x y
    ---------------
  → Q x y
⊆₂-apply (⊆: P⊆Q) {x} {y} = P⊆Q x y

-- | Substitute an equal relation (under `⇔₂`) for the left-hand side of a subset definition.
⊆₂-substˡ : ∀ {a b ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : REL A B ℓ₃}
  → P ⇔₂ Q
  → P ⊆₂ R
    ------
  → Q ⊆₂ R
⊆₂-substˡ (⇔: _ Q⊆P) P⊆R = ⊆₂-trans (⊆: Q⊆P) P⊆R

-- | Substitute an equal relation (under `⇔₂`) for the right-hand side of a subset definition.
⊆₂-substʳ : ∀ {a b ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : REL A B ℓ₃}
  → Q ⇔₂ R
  → P ⊆₂ Q
    ------
  → P ⊆₂ R
⊆₂-substʳ (⇔: Q⊆R _) P⊆Q = ⊆₂-trans P⊆Q (⊆: Q⊆R)

-- | Weaken intentional equality of relations to their subset `⊆₂` definition.
≡-to-⊆₂ : {a b ℓ : Level} {A : Set a} {B : Set b}
    {P Q : REL A B ℓ}
  → P ≡ Q
    ------
  → P ⊆₂ Q
≡-to-⊆₂ refl = ⊆: (λ _ _ Pxy → Pxy)

-- | Weaken intentional equality of relations to their superset definition (inverted `⊆₂`).
≡-to-⊇₂ : {a b ℓ : Level} {A : Set a} {B : Set b}
    {P Q : REL A B ℓ}
  → P ≡ Q
    ------
  → Q ⊆₂ P
≡-to-⊇₂ refl = ⊆: (λ _ _ Qxy → Qxy)

-- | Substitute both elements of the relation's instantiation.
subst-rel : {a b ℓ : Level} → {A : Set a} {B : Set b}
  → (R : REL A B ℓ)
  → {x₁ x₂ : A}
  → x₁ ≡ x₂
  → {y₁ y₂ : B}
  → y₁ ≡ y₂
  → R x₁ y₁
    -----------------------
  → R x₂ y₂
subst-rel _ refl refl Rxy = Rxy

-- ## Operations: ⇔₂

⇔₂-apply-⊆₂ : {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂}
  → P ⇔₂ Q
  → {x : A} {y : B}
  → P x y
    ---------------
  → Q x y
⇔₂-apply-⊆₂ = ⊆₂-apply ∘ ⇔₂-to-⊆₂

⇔₂-apply-⊇₂ : {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂}
  → P ⇔₂ Q
  → {x : A} {y : B}
  → Q x y
    ---------------
  → P x y
⇔₂-apply-⊇₂ = ⊆₂-apply ∘ ⇔₂-to-⊇₂

≡-to-⇔₂ : {a b ℓ : Level} {A : Set a} {B : Set b}
    {P Q : REL A B ℓ}
  → P ≡ Q
    ------
  → P ⇔₂ Q
≡-to-⇔₂ refl = ⇔₂-intro ⊆₂-refl ⊆₂-refl

-- # Reasoning

-- ## Reasoning: ⊆₂

-- | A collection of functions for writing subset proofs over binary relations.
--
--
-- # Example
--
-- ```
-- proof P Q R S =
--   begin⊆₂
--     (P ⨾ Q) ⨾ (R ⨾ S)
--   ⊆₂⟨ ⇔₂-to-⊇₂ ⨾-assoc ⟩
--     ((P ⨾ Q) ⨾ R) ⨾ S
--   ⊆₂⟨ ⨾-substˡ-⊆₂ (⇔₂-to-⊆₂ ⨾-assoc) ⟩
--     P ⨾ (Q ⨾ R) ⨾ S
--   ⊆₂∎
-- ```
module ⊆₂-Reasoning {a b ℓ₁ : Level} {A : Set a} {B : Set b} where

  infix  3 _⊆₂∎
  infixr 2 step-⊆₂
  infix  1 begin⊆₂_

  begin⊆₂_ : {ℓ₂ : Level} {P : REL A B ℓ₁} {Q : REL A B ℓ₂}
    → P ⊆₂ Q
    → P ⊆₂ Q
  begin⊆₂_ P⊆Q = P⊆Q

  step-⊆₂ : ∀ {ℓ₂ ℓ₃ : Level}
    → (P : REL A B ℓ₁)
    → {Q : REL A B ℓ₂}
    → {R : REL A B ℓ₃}
    → Q ⊆₂ R
    → P ⊆₂ Q
    → P ⊆₂ R
  step-⊆₂ P Q⊆R P⊆Q = ⊆₂-trans P⊆Q Q⊆R

  _⊆₂∎ : ∀ (P : REL A B ℓ₁) → P ⊆₂ P
  _⊆₂∎ P = ⊆: (λ _ _ z → z)

  syntax step-⊆₂ P Q⊆R P⊆Q = P ⊆₂⟨ P⊆Q ⟩ Q⊆R

-- ## Reasoning: ⇔₂

-- | A collection of functions for writing equality proofs over binary relations.
--
--
-- # Example
--
-- ```
-- proof P Q R S =
--   begin⇔₂
--     (P ⨾ Q) ⨾ (R ⨾ S)
--   ⇔₂⟨ ⇔₂-sym ⨾-assoc ⟩
--     ((P ⨾ Q) ⨾ R) ⨾ S
--   ⇔₂⟨ ⨾-substˡ ⨾-assoc ⟩
--     P ⨾ (Q ⨾ R) ⨾ S
--   ⇔₂∎
-- ```
module ⇔₂-Reasoning {a b ℓ₁ : Level} {A : Set a} {B : Set b} where

  infix  3 _⇔₂∎
  infixr 2 _⇔₂⟨⟩_ step-⇔₂
  infix  1 begin⇔₂_

  begin⇔₂_ : {ℓ₂ : Level} {P : REL A B ℓ₁} {Q : REL A B ℓ₂}
    → P ⇔₂ Q
    → P ⇔₂ Q
  begin⇔₂_ P⇔Q = P⇔Q

  _⇔₂⟨⟩_ : {ℓ₂ : Level}
      (P : REL A B ℓ₁)
    → {Q : REL A B ℓ₂}
    → P ⇔₂ Q
    → P ⇔₂ Q
  _ ⇔₂⟨⟩ x≡y = x≡y

  step-⇔₂ : ∀ {ℓ₂ ℓ₃ : Level}
    → (P : REL A B ℓ₁)
    → {Q : REL A B ℓ₂}
    → {R : REL A B ℓ₃}
    → Q ⇔₂ R
    → P ⇔₂ Q
    → P ⇔₂ R
  step-⇔₂ _ Q⇔R P⇔Q = ⇔₂-trans P⇔Q Q⇔R

  _⇔₂∎ : ∀ (P : REL A B ℓ₁) → P ⇔₂ P
  _⇔₂∎ _ = ⇔₂-refl

  syntax step-⇔₂ P Q⇔R P⇔Q = P ⇔₂⟨ P⇔Q ⟩ Q⇔R

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Implementation.Action where

open import Light.Library.Action using (Library ; Dependencies)
open import Light.Level using (++_ ; 0ℓ)
open import Light.Library.Data.Unit using (Unit)
open import Light.Library.Data.Natural using (ℕ)
open import Light.Variable.Sets
open import Light.Variable.Levels
import Light.Package
import Light.Implementation.Data.Natural
import Light.Implementation.Data.Unit

instance dependencies : Dependencies
dependencies = record {}

instance library : Library dependencies
library = record { Implementation }
      where
      module Implementation where
            postulate Main : Set
            private
                  postulate
                        pure′ : 𝕒 → Main
                        bind′ : Main → (𝕒 → Main) → Main
                        follow : Main → Main → Main

            {-# COMPILE JS pure′ = () => () => () => a => () => a #-}
            {-# COMPILE JS bind′ = () => () => () => m => f => f(m()) #-}
            {-# COMPILE JS follow = () => () => m => m2 => () => (m(), m2()) #-}

            {-# NO_UNIVERSE_CHECK #-}
            data Action (𝕒 : Set ℓ) : Set ℓ where
                  pure : 𝕒 → Action 𝕒
                  _>>=_ : Action 𝕓 → (𝕓 → Action 𝕒) → Action 𝕒
                  _>>_ : Action 𝕓 → Action 𝕒 → Action 𝕒
                  lift : Main → Action 𝕒

            run : Action 𝕒 → Main
            run (pure a) = pure′ a
            run (a >>= f) = bind′ (run a) (λ a → run (f a))
            run (a >> b) = follow (run a) (run b)
            run (lift m) = m

            private
                  postulate log′ alert′ : 𝕒 → Main
                  postulate prompt′ : Main

            log : 𝕒 → Action Unit
            log a = lift (log′ a)

            prompt = lift prompt′

            alert : 𝕒 → Action Unit
            alert a = lift (alert′ a)

            {-# COMPILE JS log′ = () => () => a => () => console.log(a) #-}
            {-# COMPILE JS prompt′ = () => () => BigInt(prompt()) #-}
            {-# COMPILE JS alert′ = () => () => () => a => alert(a) #-}

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
module Impure.LFRef.Properties.Soundness where

open import Data.Nat
open import Data.Sum
open import Data.Product as Pr
open import Data.List as List hiding (monad)
open import Data.Fin using (fromℕ≤; Fin)
open import Data.Vec hiding (_∷ʳ_; _>>=_)
open import Data.Star hiding (_>>=_)
open import Function
open import Extensions.List as L

open import Relation.Binary.PropositionalEquality as P
open import Relation.Binary.Core using (REL; Reflexive)
open import Relation.Binary.List.Pointwise as PRel hiding (refl)

open import Impure.LFRef.Syntax
open import Impure.LFRef.Welltyped
open import Impure.LFRef.Eval
open import Impure.LFRef.Properties.Decidable

progress : ∀ {𝕊 Σ A} {e : Exp 0} {μ} →
           𝕊 , Σ ⊢ μ →
           𝕊 , Σ , [] ⊢ₑ e ∶ A →
           --------------------------------------
           (ExpVal e) ⊎ (∃₂ λ e' μ' → (𝕊 ⊢ e , μ ≻ e' , μ'))

progress p (tm (con k ts _)) = inj₁ (tm con)
progress p (tm unit) = inj₁ (tm unit)
progress p (tm (var ()))
progress p (tm (loc x)) = inj₁ (tm loc)

progress p (fn ·★[ q ] ts) = inj₂ (, (, funapp-β fn (tele-fit-length ts)))

progress p (ref e) with progress p e
progress p (ref {_} {tm _} (tm _)) | inj₁ (tm v) = inj₂ (, (, ref-val v))
progress p (ref {_} {_ ·★ _} e) | inj₁ ()
progress p (ref {_} {ref x} e) | inj₁ ()
progress p (ref {_} { ! x } e) | inj₁ ()
progress p (ref {_} {x ≔ x₁} e) | inj₁ ()
progress p (ref e) | inj₂ (e' , μ' , step) = inj₂ (, (, ref-clos step))

progress p (!_ {x = x} e) with progress p e
progress p (!_ {_} {tm .(loc _)} (tm (loc x))) | inj₁ (tm _) =
  inj₂ (, (, !-val (P.subst (_<_ _) (pointwise-length p) ([]=-length x))))
progress p (!_ {_} {tm (var ())} e) | _
progress p (!_ {_} {_ ·★ _} e) | inj₁ ()
progress p (!_ {_} {ref x} e) | inj₁ ()
progress p (!_ {_} { ! x } e) | inj₁ ()
progress p (!_ {_} {x ≔ x₁} e) | inj₁ ()
progress p (! e) | inj₂ (e' , μ' , step) = inj₂ (, (, !-clos step))

progress p (l ≔ e) with progress p l | progress p e
progress p (tm () ≔ e) | inj₁ (tm unit) | (inj₁ (tm x₁))
progress p (tm () ≔ e) | inj₁ (tm con) | (inj₁ (tm x₁))
progress p (tm (loc x) ≔ e) | inj₁ (tm loc) | (inj₁ (tm v)) =
  inj₂ (, (, ≔-val (P.subst (_<_ _) (pointwise-length p) ([]=-length x)) v))
progress p (l ≔ e) | inj₂ (_ , _ , step) | _ = inj₂ (, (, ≔-clos₁ step))
progress p (l ≔ e) | inj₁ v | (inj₂ (_ , _ , step)) = inj₂ (, (, ≔-clos₂ v step))

progress-seq : ∀ {𝕊 Σ A} {e : SeqExp 0} {μ} →
                𝕊 , Σ ⊢ μ →
                𝕊 , Σ , [] ⊢ₛ e ∶ A →
                --------------------------------------
                SeqExpVal e ⊎ ∃₂ λ e' μ' → (𝕊 ⊢ e , μ ≻ₛ e' , μ')

progress-seq p (ret e) with progress p e
... | inj₁ (tm v) = inj₁ (ret-tm v)
... | inj₂ (e' , μ' , step) = inj₂ (, , ret-clos step)
progress-seq p (lett x e) with progress p x
progress-seq p (lett x e) | inj₁ (tm v) = inj₂ (, (, lett-β))
progress-seq p (lett x e) | inj₂ (x' , μ' , step) = inj₂ (, (, lett-clos step))

postulate

  lem₂ : ∀ {n 𝕊 Σ e a b t} {Γ : Ctx n} →
           𝕊 , Σ , (a :+: Γ) ⊢ₑ e ∶ weaken₁-tp b →
           𝕊 , Σ , Γ ⊢ t ∶ a →
           𝕊 , Σ , Γ ⊢ₑ (e exp/ (sub t)) ∶ b

  lem₃ : ∀ {n 𝕊 Σ e a b t} {Γ : Ctx n} →
           𝕊 , Σ , (a :+: Γ) ⊢ₛ e ∶ weaken₁-tp b →
           𝕊 , Σ , Γ ⊢ t ∶ a →
           𝕊 , Σ , Γ ⊢ₛ (e seq/ (sub t)) ∶ b

  lem₁ : ∀ {n 𝕊 Σ φ ts} {Γ : Ctx n} →
          𝕊 ⊢ φ fnOk →
          (p : 𝕊 , Σ , Γ ⊢ ts ∶ⁿ weaken+-tele n (Fun.args φ)) →
          (q : length ts ≡ (Fun.m φ)) →
          𝕊 , Σ , Γ ⊢ₑ (!call (Fun.body φ) ts q) ∶ ((Fun.returntype φ) fun[ ts / q ])

-- loading from a welltyped store results in a welltyped term
!load-ok : ∀ {Σ Σ' A μ i 𝕊} →
            -- store-welltypedness type (strengthened for induction)
            Rel (λ A x → 𝕊 , Σ , [] ⊢ (proj₁ x) ∶ A) Σ' μ →
            Σ' L.[ i ]= A → (l : i < length μ) →
            𝕊 , Σ , [] ⊢ (!load μ l) ∶ A
!load-ok [] ()
!load-ok (x∼y ∷ p) here (s≤s z≤n) = x∼y
!load-ok (x∼y ∷ p) (there q) (s≤s l) = !load-ok p q l

mutual
  ⊒-preserves-tm : ∀ {n Γ Σ Σ' A 𝕊} {t : Term n} → Σ' ⊒ Σ → 𝕊 , Σ , Γ ⊢ t ∶ A → 𝕊 , Σ' , Γ ⊢ t ∶ A
  ⊒-preserves-tm ext unit = unit
  ⊒-preserves-tm ext (var x) = var x
  ⊒-preserves-tm ext (con x p q) = con x (⊒-preserves-tele ext p) q
  ⊒-preserves-tm ext (loc x) = loc (xs⊒ys[i] x ext)

  ⊒-preserves-tele : ∀ {n m Γ Σ Σ' 𝕊} {ts : List (Term n)} {T : Tele n m} → Σ' ⊒ Σ →
                    𝕊 , Σ , Γ ⊢ ts ∶ⁿ T →
                    𝕊 , Σ' , Γ ⊢ ts ∶ⁿ T
  ⊒-preserves-tele ext ε = ε
  ⊒-preserves-tele ext (x ⟶ p) = ⊒-preserves-tm ext x ⟶ (⊒-preserves-tele ext p)

-- welltypedness is preseved under store extensions
⊒-preserves : ∀ {n Γ Σ Σ' A 𝕊} {e : Exp n} → Σ' ⊒ Σ → 𝕊 , Σ , Γ ⊢ₑ e ∶ A → 𝕊 , Σ' , Γ ⊢ₑ e ∶ A
⊒-preserves ext (tm x) = tm (⊒-preserves-tm ext x)
⊒-preserves ext (x ·★[ refl ] p) with ⊒-preserves-tele ext p
... | p' = x ·★[ refl ] p'

⊒-preserves ext (ref p) = ref (⊒-preserves ext p)
⊒-preserves ext (! p) = ! (⊒-preserves ext p)
⊒-preserves ext (p ≔ q) = ⊒-preserves ext p ≔ ⊒-preserves ext q

⊒-preserves-seq : ∀ {n Γ Σ Σ' A 𝕊} {e : SeqExp n} → Σ' ⊒ Σ → 𝕊 , Σ , Γ ⊢ₛ e ∶ A → 𝕊 , Σ' , Γ ⊢ₛ e ∶ A
⊒-preserves-seq ext (ret e) = ret (⊒-preserves ext e)
⊒-preserves-seq ext (lett e c) = lett (⊒-preserves ext e) (⊒-preserves-seq ext c)

-- helper for lifting preserving reductions into their closure
clos-cong : ∀ {Σ μ 𝕊 A B} {e : Exp 0} (c : Exp 0 → Exp 0) →
                (f : ∀ {Σ'} (ext : Σ' ⊒ Σ) → 𝕊 , Σ' , [] ⊢ₑ e ∶ A → 𝕊 , Σ' , [] ⊢ₑ c e ∶ B) →
                (∃ λ Σ' → 𝕊 , Σ' , [] ⊢ₑ e ∶ A × Σ' ⊒ Σ × 𝕊 , Σ' ⊢ μ) →
                ∃ λ Σ' → 𝕊 , Σ' , [] ⊢ₑ c e ∶ B × Σ' ⊒ Σ × 𝕊 , Σ' ⊢ μ
clos-cong _ f (Σ , wte , ext , μ-wt) = Σ , f ext wte , ext , μ-wt

≻-preserves : ∀ {𝕊 Σ A} {e : Exp 0} {e' μ' μ} →
              𝕊 , [] ⊢ok →
              𝕊 , Σ , [] ⊢ₑ e ∶ A →
              𝕊 , Σ ⊢ μ →
              𝕊 ⊢ e , μ ≻ e' , μ' →
              ----------------------------------------------------
              ∃ λ Σ' → 𝕊 , Σ' , [] ⊢ₑ e' ∶ A × Σ' ⊒ Σ × 𝕊 , Σ' ⊢ μ'

-- variables
≻-preserves ok (tm x) q ()

-- function application
≻-preserves {Σ = Σ} ok (fn ·★[ refl ] ts) q (funapp-β x refl) with
  []=-functional _ _  fn x | all-lookup fn (_,_⊢ok.funs-ok ok)
... | refl | fn-ok = Σ , (lem₁ fn-ok ts refl) , ⊑-refl , q

-- new references
≻-preserves {Σ = Σ} ok (ref {A = A} (tm x)) q (ref-val v) = let ext = (∷ʳ-⊒ A Σ) in
  Σ ∷ʳ A ,
  (tm (loc (P.subst (λ i → _ L.[ i ]= _) (pointwise-length q) (∷ʳ[length] Σ A)))) ,
  ext ,
  pointwise-∷ʳ (PRel.map (⊒-preserves-tm ext) q) (⊒-preserves-tm ext x)
≻-preserves ok (ref p) q (ref-clos step) =
  clos-cong
    ref (const ref)
    (≻-preserves ok p q step)

-- dereferencing
≻-preserves {Σ = Σ₁} ok (! tm (loc x)) q (!-val p)
  = Σ₁ , tm (!load-ok q x p) , ⊑-refl , q
≻-preserves ok (! p) q (!-clos step) =
  clos-cong
    !_ (const !_)
    (≻-preserves ok p q step)

-- assignment
≻-preserves {Σ = Σ₁} ok (_≔_ (tm (loc x)) (tm y)) q (≔-val p v) =
  Σ₁ , tm unit , ⊑-refl , pointwise-[]≔ q x p y
≻-preserves ok (p ≔ p₁) q (≔-clos₁ step) =
  clos-cong
    (λ p' → p' ≔ _) (λ ext p' → p' ≔ ⊒-preserves ext p₁)
    (≻-preserves ok p q step)
≻-preserves ok (p ≔ p₁) q (≔-clos₂ v step) =
  clos-cong
    (λ p' → _ ≔ p') (λ ext p' → ⊒-preserves ext p ≔ p')
    (≻-preserves ok p₁ q step)

-- let binding
≻ₛ-preserves : ∀ {𝕊 Σ A} {e : SeqExp 0} {e' μ' μ} →
              𝕊 , [] ⊢ok →
              𝕊 , Σ , [] ⊢ₛ e ∶ A →
              𝕊 , Σ ⊢ μ →
              𝕊 ⊢ e , μ ≻ₛ e' , μ' →
              -------------------------------------------------------
              ∃ λ Σ' → 𝕊 , Σ' , [] ⊢ₛ e' ∶ A × Σ' ⊒ Σ × 𝕊 , Σ' ⊢ μ'
≻ₛ-preserves {Σ = Σ} ok (lett (tm x) p) q lett-β = Σ , lem₃ p x , ⊑-refl , q
≻ₛ-preserves ok (lett p p₁) q (lett-clos step) with ≻-preserves ok p q step
... | Σ₂ , wte' , Σ₂⊒Σ₁ , q' = Σ₂ , lett wte' ((⊒-preserves-seq Σ₂⊒Σ₁ p₁)) , Σ₂⊒Σ₁ , q'
≻ₛ-preserves ok (ret e) q (ret-clos step) with ≻-preserves ok e q step
... | Σ₂ , wte' , Σ₂⊒Σ₁ , q' = Σ₂ , ret wte' , Σ₂⊒Σ₁ , q'

module SafeEval where

  open import Category.Monad.Partiality
  open import Category.Monad
  open import Coinduction
  open import Level as Lev

  open RawMonad {f = Lev.zero} monad

  -- typesafe evaluation in the partiality/delay-monad;
  -- or "soundness" modulo non-trivial divergence
  eval : ∀ {𝕊 Σ a μ} {e : SeqExp 0} →
        𝕊 , [] ⊢ok → -- given an ok signature context,
        𝕊 , Σ , [] ⊢ₛ e ∶ a → -- a welltyped closed expression,
        𝕊 , Σ ⊢ μ → -- and a welltyped store
       ---------------------------------------------------------------------------------------
        -- eval will either diverge or provide evidence of a term v, store μ' and storetype Σ'
        (∃ λ v → ∃ λ μ' → ∃ λ Σ' →
          -- such that v is a value,
          (SeqExpVal v) ×
          -- ...there is a sequence of small steps from e to v
          (𝕊 ⊢ e , μ ≻⋆ v , μ') ×
          -- ...v has the same type as e
          (𝕊 , Σ' , [] ⊢ₛ v ∶ a) ×
          -- ...μ' is typed by Σ'
          (𝕊 , Σ' ⊢ μ') ×
          -- ...and finally, Σ' is an extension of Σ
          (Σ' ⊒ Σ)) ⊥

  eval 𝕊-ok wte μ-ok with progress-seq μ-ok wte
  eval 𝕊-ok wte μ-ok | inj₁ v = now (_ , _ , _ , v , ε , wte , μ-ok , ⊑-refl)
  eval 𝕊-ok wte μ-ok | inj₂ (e' , μ' , step) with ≻ₛ-preserves 𝕊-ok wte μ-ok step
  ... | (Σ' , wte' , ext₁ , μ'-ok) with later (♯ (eval 𝕊-ok wte' μ'-ok))
  ... | (now (v' , μ'' , Σ'' , val , steps , wte'' , μ''-ok , ext₂)) =
    now (v' , (μ'' , (Σ'' , val , ((steps ▻ step) , (wte'' , μ''-ok , ⊑-trans ext₁ ext₂)))))
  ... | (later x) = later (♯ (♭ x >>=
    λ{ (v' , μ'' , Σ'' , val , steps , wte'' , μ''-ok , ext₂) →
      now (v' , μ'' , Σ'' , val , steps ▻ step , wte'' , μ''-ok , ⊑-trans ext₁ ext₂)
    }))


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

module HITs.PropositionalTruncation.Properties where

open import HITs.PropositionalTruncation
open import Prelude
open import Data.Empty.Properties using (isProp⊥)

refute-trunc : ¬ A → ¬ ∥ A ∥
refute-trunc = rec isProp⊥

recompute : Dec A → ∥ A ∥ → A
recompute (yes p)  _  = p
recompute (no ¬p)  p  = ⊥-elim (rec isProp⊥ ¬p p)

open import HITs.PropositionalTruncation.Sugar

bij-iso : A ↔ B → ∥ A ∥ ⇔ ∥ B ∥
bij-iso A↔B .fun = _∥$∥_ (A↔B .fun)
bij-iso A↔B .inv = _∥$∥_ (A↔B .inv)
bij-iso A↔B .rightInv x = squash _ x
bij-iso A↔B .leftInv  x = squash _ x

bij-eq : A ↔ B → ∥ A ∥ ≡ ∥ B ∥
bij-eq = isoToPath ∘ bij-iso

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
open import Relation.Binary using (Decidable; Setoid; DecSetoid)
open import Level

module CP.Session3 {a} {b} (ChanDecSetoid : DecSetoid zero a) (TypeDecSetoid : DecSetoid zero b) where

module TS = DecSetoid TypeDecSetoid

Type : Set
Type = DecSetoid.Carrier TypeDecSetoid

open DecSetoid ChanDecSetoid

Chan : Set
Chan = Carrier

module _ where
  -- type of
  infix 6 _∶_
  data TypeOf : Set a where
    _∶_ : (x : Chan) → (A : Type) → TypeOf

  chanOf : TypeOf → Chan
  chanOf (x ∶ _) = x

  import Relation.Binary.Construct.On as On

  decSetoid : DecSetoid _ _
  decSetoid = On.decSetoid ChanDecSetoid chanOf

open import Data.List.Relation.Binary.Subset.DecSetoid decSetoid
open import Data.List

Session : Set a
Session = List TypeOf

open import Relation.Nullary
open import Relation.Nullary.Decidable

open import Data.Product
open import Data.Maybe

seperate : (Γ : Session) → (x : Chan) → Maybe (∃[ Δ ] ∃[ A ] (Γ ≋ x ∶ A ∷ Δ))
seperate []          x = nothing
seperate (y ∶ A ∷ Γ) x with y ≟ x
... | yes P = just (Γ , A , ∷-cong P ≋-refl)
... | no ¬P with seperate Γ x
... | just (Δ , B , eq) = just (y ∶ A ∷ Δ , B , reasoning)
  where
    open EqReasoning
    reasoning : y ∶ A ∷ Γ ≋ x ∶ B ∷ y ∶ A ∷ Δ
    reasoning =
      begin
        y ∶ A ∷ Γ
      ≈⟨ ∷-cong refl eq ⟩
        y ∶ A ∷ x ∶ B ∷ Δ
      ≈⟨ ≋-swap ⟩
        x ∶ B ∷ y ∶ A ∷ Δ
      ∎
... | nothing = nothing

-- insertion
infixl 5 _#_
_#_ : Session → TypeOf → Session
Γ # (x ∶ A) with seperate Γ x
... | nothing = x ∶ A ∷ Γ
... | just (Δ , _ , _) = x ∶ A ∷ Δ

insert-idempotent : ∀ Γ x A → Γ # x ∶ A # x ∶ A ≋ Γ # x ∶ A
insert-idempotent Γ x A with seperate Γ x
insert-idempotent Γ x A | nothing with seperate (x ∶ A ∷ Γ) x
... | nothing = {!   !}
... | just x₁ = {!   !}
insert-idempotent Γ x A | just x₁ = {!   !}

max_stars_repo_name: banacorn/bidirectional

max_issues_repo_name: banacorn/bidirectional

max_forks_repo_name: banacorn/bidirectional


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

module Data.Binary.Isomorphism where

open import Data.Binary.Definition
open import Data.Binary.Conversion
open import Data.Binary.Increment
open import Prelude
import Data.Nat as ℕ

inc-suc : ∀ x → ⟦ inc x ⇓⟧ ≡ suc ⟦ x ⇓⟧
inc-suc 0ᵇ     i = 1
inc-suc (1ᵇ x) i = 2 ℕ.+ ⟦ x ⇓⟧ ℕ.* 2
inc-suc (2ᵇ x) i = suc (inc-suc x i ℕ.* 2)

inc-2*-1ᵇ : ∀ n → inc ⟦ n ℕ.* 2 ⇑⟧ ≡ 1ᵇ ⟦ n ⇑⟧
inc-2*-1ᵇ zero    i = 1ᵇ 0ᵇ
inc-2*-1ᵇ (suc n) i = inc (inc (inc-2*-1ᵇ n i))

𝔹-rightInv : ∀ x → ⟦ ⟦ x ⇑⟧ ⇓⟧ ≡ x
𝔹-rightInv zero    = refl
𝔹-rightInv (suc x) = inc-suc ⟦ x ⇑⟧ ; cong suc (𝔹-rightInv x)

𝔹-leftInv : ∀ x → ⟦ ⟦ x ⇓⟧ ⇑⟧ ≡ x
𝔹-leftInv 0ᵇ = refl
𝔹-leftInv (1ᵇ x) =           inc-2*-1ᵇ ⟦ x ⇓⟧  ; cong 1ᵇ_ (𝔹-leftInv x)
𝔹-leftInv (2ᵇ x) = cong inc (inc-2*-1ᵇ ⟦ x ⇓⟧) ; cong 2ᵇ_ (𝔹-leftInv x)

𝔹⇔ℕ : 𝔹 ⇔ ℕ
𝔹⇔ℕ .fun = ⟦_⇓⟧
𝔹⇔ℕ .inv = ⟦_⇑⟧
𝔹⇔ℕ .rightInv = 𝔹-rightInv
𝔹⇔ℕ .leftInv  = 𝔹-leftInv


text:
module Numeral.Natural.Prime.Proofs where

import Lvl
open import Data
open import Data.Boolean.Stmt
open import Data.Either as Either using ()
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Lang.Instance
open import Logic
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Logic.Predicate
open import Numeral.Natural
open import Numeral.Natural.Relation.Divisibility
open import Numeral.Natural.Relation.Divisibility.Proofs
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Prime
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Function.Domain
open import Structure.Operator.Properties
open import Structure.Relator.Properties
open import Type

[0]-nonprime : ¬ Prime(0)
[0]-nonprime ()

[1]-nonprime : ¬ Prime(1)
[1]-nonprime ()

[0]-noncomposite : ¬ Composite(0)
[0]-noncomposite ()

[1]-noncomposite : ¬ Composite(1)
[1]-noncomposite ()

[2]-prime : Prime(2)
[2]-prime = intro p where
  p : PrimeProof
  p {0} _ = [∨]-introₗ [≡]-intro
  p {1} _ = [∨]-introᵣ [≡]-intro

[3]-prime : Prime(3)
[3]-prime = intro p where
  p : PrimeProof
  p {0} _ = [∨]-introₗ [≡]-intro
  p {1} (Div𝐒 ())
  p {2} _ = [∨]-introᵣ [≡]-intro

[4]-composite : Composite(4)
[4]-composite = intro 0 0

[5]-prime : Prime(5)
[5]-prime = intro p where
  p : PrimeProof
  p {0} _ = [∨]-introₗ [≡]-intro
  p {1} (Div𝐒 (Div𝐒 ()))
  p {2} (Div𝐒 ())
  p {3} (Div𝐒 ())
  p {4} _ = [∨]-introᵣ [≡]-intro

[6]-composite : Composite(6)
[6]-composite = Composite-intro 2 3

[7]-prime : Prime(7)
[7]-prime = intro p where
  p : PrimeProof
  p {0} _ = [∨]-introₗ [≡]-intro
  p {1} (Div𝐒 (Div𝐒 (Div𝐒 ())))
  p {2} (Div𝐒 (Div𝐒 ()))
  p {3} (Div𝐒 ())
  p {4} (Div𝐒 ())
  p {5} (Div𝐒 ())
  p {6} d = [∨]-introᵣ [≡]-intro

[8]-composite : Composite(8)
[8]-composite = Composite-intro 2 4

[9]-composite : Composite(9)
[9]-composite = Composite-intro 3 3

[10]-composite : Composite(10)
[10]-composite = Composite-intro 2 5

[11]-prime : Prime(11)
[11]-prime = intro p where
  p : PrimeProof
  p {0} _ = [∨]-introₗ [≡]-intro
  p {1} (Div𝐒 (Div𝐒 (Div𝐒 (Div𝐒 (Div𝐒 ())))))
  p {2} (Div𝐒 (Div𝐒 (Div𝐒 ())))
  p {3} (Div𝐒 (Div𝐒 ()))
  p {4} (Div𝐒 (Div𝐒 ()))
  p {5} (Div𝐒 ())
  p {6} (Div𝐒 ())
  p {7} (Div𝐒 ())
  p {8} (Div𝐒 ())
  p {9} (Div𝐒 ())
  p {10} d = [∨]-introᵣ [≡]-intro

prime-only-divisors : ∀{n} → Prime(n) → (∀{x} → (x ∣ n) → ((x ≡ 1) ∨ (x ≡ n)))
prime-only-divisors {𝐒 (𝐒 n)} (intro prime) {𝟎}   = [⊥]-elim ∘ [0]-divides-not
prime-only-divisors {𝐒 (𝐒 n)} (intro prime) {𝐒 x} = Either.map ([≡]-with(𝐒)) ([≡]-with(𝐒)) ∘ prime

prime-when-only-divisors : ∀{n} → (n ≥ 2) → (∀{x} → (x ∣ n) → ((x ≡ 1) ∨ (x ≡ n))) → Prime(n)
prime-when-only-divisors {𝐒(𝐒 n)} (succ _) proof = intro p where
  p : PrimeProof
  p {𝟎}   _ = [∨]-introₗ [≡]-intro
  p {𝐒 x}   = Either.map (injective(𝐒)) (injective(𝐒)) ∘ proof

prime-prime-divisor : ∀{a b} → Prime(a) → Prime(b) → (a ∣ b) → (a ≡ b)
prime-prime-divisor pa pb div with prime-only-divisors pb div
... | [∨]-introₗ [≡]-intro with () ← [1]-nonprime pa
... | [∨]-introᵣ ab = ab

module _ where
  open import Sets.PredicateSet renaming (_≡_ to _≡ₛ_)

  private variable a b n p : ℕ

  -- All prime numbers are prime factors of 0.
  [0]-primeFactors : PrimeFactor(0) ⊇ Prime
  [0]-primeFactors prime = intro where
    instance _ = prime
    instance _ = Div𝟎

  -- There are no prime factors of 1.
  [1]-primeFactors : PrimeFactor(1) ⊆ ∅ {Lvl.𝟎}
  [1]-primeFactors {𝐒 𝟎} (intro ⦃ () ⦄)
  [1]-primeFactors {𝐒 (𝐒 x)} (intro ⦃ factor = factor ⦄) with succ() ← divides-upper-limit factor

  -- The only prime factors of a prime number is itself.
  prime-primeFactors : ⦃ _ : Prime(p) ⦄ → (PrimeFactor(p) ≡ₛ (• p))
  prime-primeFactors {p}{x} = [↔]-intro (\{[≡]-intro → intro}) (\{intro → symmetry(_≡_) (prime-prime-divisor infer infer infer)})

  -- When a number is a prime factor of itself, it is a prime number.
  -- A very obvious fact (it follows by definition).
  reflexive-primeFactor-is-prime : (n ∈ PrimeFactor(n)) → Prime(n)
  reflexive-primeFactor-is-prime intro = infer

  divisor-primeFactors : ∀{a b} → (a ∣ b) → (PrimeFactor(a) ⊆ PrimeFactor(b))
  divisor-primeFactors div (intro ⦃ p ⦄ ⦃ xa ⦄) = intro ⦃ p ⦄ ⦃ transitivity(_∣_) xa div ⦄

composite-existence : ∀{n} → Composite(n) ↔ ∃{Obj = ℕ ⨯ ℕ}(\(a , b) → (a + 2) ⋅ (b + 2) ≡ n)
composite-existence = [↔]-intro (\{([∃]-intro (a , b) ⦃ [≡]-intro ⦄) → intro a b}) \{(intro a b) → [∃]-intro (a , b) ⦃ [≡]-intro ⦄}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

--{-# OPTIONS -v rewriting:100 #-}

postulate
  _↦_ : ∀ {i} {A : Set i} → A → A → Set i
{-# BUILTIN REWRITE _↦_ #-}

data _==_ {i} {A : Set i} (a : A) : A → Set i where
  idp : a == a

ap : ∀ i j (A : Set i) (B : Set j) (f : A → B) (x y : A)
  → (x == y → f x == f y)
ap _ _ _ _ f _ ._ idp = idp

postulate
  ap∘-rewr : ∀ {i j k} {A : Set i} {B : Set j} {C : Set k} (g : B → C) (f : A → B)
    {x y : A} (p : x == y) →
    ap j k B C g (f x) (f y) (ap i j A B f x y p) ↦ ap i k A C (λ x → g (f x)) x y p
{-# REWRITE ap∘-rewr #-}

-- This one works, rewriting the RHS to the LHS using the previous rewrite rule as expected
{-ap∘ : ∀ {i j k} {A : Set i} {B : Set j} {C : Set k} (g : B → C) (f : A → B)
  {x y : A} (p : x == y) →
  ap (λ x → g (f x)) p == ap g (ap f p)
ap∘ g f p = idp
-}

postulate P : ∀ i (A : Set i) (x y : A) (p : x == y) → Set

-- This one doesn’t work, although it should just have to rewrite [P (ap g (ap f p))] to [P (ap (λ x → g (f x)) p)]
test : ∀ {i j k} {A : Set i} {B : Set j} {C : Set k} (g : B → C) (f : A → B)
  {x y : A} (p : x == y)
  → P k C (g (f x)) (g (f y)) (ap i k A C (λ x → g (f x)) x y p) → P k C (g (f x)) (g (f y)) (ap j k B C g (f x) (f y) (ap i j A B f x y p))
test g f p s = s

{-
.i != .j of type .Agda.Primitive.Level
when checking that the expression s has type P (ap g (ap f p))
-}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
------------------------------------------------------------------------------
-- Testing the translation of definitions
------------------------------------------------------------------------------

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

module Definition01a where

postulate
  D   : Set
  _≡_ : D → D → Set
  d   : D

-- We test the translation of the definition of a nullary function.
e : D
e = d
{-# ATP definition e #-}

postulate foo : e ≡ d
{-# ATP prove foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Structures.Action where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure
open import Cubical.Functions.FunExtEquiv

open import Cubical.Data.Sigma

open import Cubical.Algebra.Group
open import Cubical.Structures.LeftAction

open import Cubical.DStructures.Base
open import Cubical.DStructures.Meta.Properties

open import Cubical.DStructures.Structures.Constant
open import Cubical.DStructures.Structures.Type
open import Cubical.DStructures.Structures.Group

private
  module _ {ℓ ℓ' : Level} where
    Las : ((G , H) : Group {ℓ} × Group {ℓ'}) → Type (ℓ-max ℓ ℓ')
    Las (G , H) = LeftActionStructure ⟨ G ⟩ ⟨ H ⟩

module _ (ℓ ℓ' : Level) where
  G²Las = Σ[ GH ∈ G² ℓ ℓ' ] Las GH
  GGLas = Σ[ G ∈ Group {ℓ} ] Σ[ H ∈ Group {ℓ'} ] Las (G , H)
  Action = Σ[ ((G , H) , _α_) ∈ G²Las ] (IsGroupAction G H _α_)
  G²LasAct = Σ[ (G , H) ∈ G² ℓ ℓ' ] Σ[ α ∈ Las (G , H) ] IsGroupAction G H α
  GGLasAct = Σ[ G ∈ Group {ℓ} ] Σ[ H ∈ Group {ℓ'} ] Σ[ α ∈ Las (G , H) ] IsGroupAction G H α

  IsoAction : Iso Action GGLasAct
  IsoAction = compIso Σ-assoc-Iso Σ-assoc-Iso

  -- two groups with an action structure, i.e. a map ⟨ G ⟩ → ⟨ H ⟩ → ⟨ H ⟩
  𝒮ᴰ-G²\Las : URGStrᴰ (𝒮-group ℓ ×𝒮 𝒮-group ℓ')
                      (λ GH → Las GH)
                      (ℓ-max ℓ ℓ')
  𝒮ᴰ-G²\Las =
    make-𝒮ᴰ (λ {(G , H)} _α_ (eG , eH) _β_
                   → (g : ⟨ G ⟩) (h : ⟨ H ⟩)
                     → GroupEquiv.eq eH .fst (g α h) ≡ (GroupEquiv.eq eG .fst g) β (GroupEquiv.eq eH .fst h))
                (λ _ _ _ → refl)
                λ (G , H) _α_ → isContrRespectEquiv
                                                       -- (Σ[ _β_ ∈ Las (G , H) ] (_α_ ≡ _β_)
                                                       (Σ-cong-equiv-snd (λ _β_ → invEquiv funExt₂Equiv))
                                                       (isContrSingl _α_)

  𝒮-G²Las : URGStr G²Las (ℓ-max ℓ ℓ')
  𝒮-G²Las = ∫⟨ 𝒮-group ℓ ×𝒮 𝒮-group ℓ' ⟩ 𝒮ᴰ-G²\Las

  open ActionΣTheory

  𝒮ᴰ-G²Las\Action : URGStrᴰ 𝒮-G²Las
                     (λ ((G , H) , _α_) → IsGroupAction G H _α_)
                     ℓ-zero
  𝒮ᴰ-G²Las\Action = Subtype→Sub-𝒮ᴰ (λ ((G , H) , _α_) → IsGroupAction G H _α_ , isPropIsGroupAction G H _α_)
                             𝒮-G²Las

  𝒮-G²LasAction : URGStr Action (ℓ-max ℓ ℓ')
  𝒮-G²LasAction = ∫⟨ 𝒮-G²Las ⟩ 𝒮ᴰ-G²Las\Action

  𝒮-Action = 𝒮-G²LasAction

  𝒮ᴰ-G\GLasAction : URGStrᴰ (𝒮-group ℓ)
                            (λ G → Σ[ H ∈ Group {ℓ'} ] Σ[ α ∈ Las (G , H) ] IsGroupAction G H α)
                            (ℓ-max ℓ ℓ')
  𝒮ᴰ-G\GLasAction =
    splitTotal-𝒮ᴰ (𝒮-group ℓ)
                  (𝒮ᴰ-const (𝒮-group ℓ) (𝒮-group ℓ'))
                  (splitTotal-𝒮ᴰ (𝒮-group ℓ ×𝒮 𝒮-group ℓ')
                                 𝒮ᴰ-G²\Las
                                 𝒮ᴰ-G²Las\Action)

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


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

open import Level

-- This is really a degenerate version of Categories.Category.Instance.Zero
-- Here EmptySet is not given an explicit name, it is an alias for Lift o ⊥
module Categories.Category.Instance.EmptySet where

open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Binary.PropositionalEquality using (refl)

open import Categories.Category.Instance.Sets
import Categories.Object.Initial as Init

module _ {o : Level} where
  open Init (Sets o)

  EmptySet-⊥ : Initial
  EmptySet-⊥ = record { ⊥ = Lift o ⊥ ; ! = λ { {A} (lift x) → ⊥-elim x } ; !-unique = λ { f {()} } }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
-- Andreas, 2016-02-11. Irrelevant constructors are not (yet?) supported

data D : Set where
  .c : D

-- Should fail, e.g., with parse error.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- Pretty-printing (documents and document combinators)
------------------------------------------------------------------------

{-# OPTIONS --guardedness #-}

module Pretty where

open import Data.Bool
open import Data.Char
open import Data.List hiding ([_])
open import Data.List.NonEmpty using (List⁺; _∷_; _∷⁺_)
open import Data.List.Properties
open import Data.Maybe hiding (_>>=_)
open import Data.Nat
open import Data.Product
open import Data.Unit
open import Function
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Tactic.MonoidSolver

open import Grammar.Infinite as G
  hiding (_<$>_; _<$_; _⊛_; _<⊛_; _⊛>_; token; tok; if-true; sat;
          tok-sat; symbol; list; list⁺)

------------------------------------------------------------------------
-- Pretty-printers

mutual

  -- Pretty-printer documents, indexed by grammars and corresponding
  -- values.
  --
  -- For convenience I have chosen to parametrise Doc by "extended"
  -- grammars rather than basic ones.

  infixr 20 _◇_

  data Doc : ∀ {A} → Grammar A → A → Set₁ where

    -- Concatenation.

    _◇_   : ∀ {c₁ c₂ A B x y}
              {g₁ : ∞Grammar c₁ A} {g₂ : A → ∞Grammar c₂ B} →
            Doc (♭? g₁) x → Doc (♭? (g₂ x)) y → Doc (g₁ >>= g₂) y

    -- A string. Note that I do /not/ enforce Wadler's convention
    -- that the string does not contain newline characters.

    text  : ∀ {s} → Doc (string s) s

    -- One or more whitespace characters.

    line  : Doc (tt G.<$ whitespace +) tt

    -- Grouping construct.

    group : ∀ {A x} {g : Grammar A} → Doc g x → Doc g x

    -- Increases the nesting level. (Whatever this means. Renderers
    -- are free to ignore group and nest, see ugly-renderer below.)

    nest  : ∀ {A x} {g : Grammar A} → ℕ → Doc g x → Doc g x

    -- Embedding operator: Documents for one grammar/result also
    -- work for other grammars/results, given that the semantics
    -- are, in a certain sense, compatible.

    emb   : ∀ {A B x y} {g₁ : Grammar A} {g₂ : Grammar B} →
            (∀ {s} → x ∈ g₁ · s → y ∈ g₂ · s) →
            Doc g₁ x → Doc g₂ y

    -- Fill operator.

    fill  : ∀ {A xs} {g : Grammar A} →
            Docs g xs → Doc (g sep-by whitespace +) xs

  -- Sequences of documents, all based on the same grammar.

  infixr 5 _∷_

  data Docs {A} (g : Grammar A) : List⁺ A → Set₁ where
    [_] : ∀ {x} → Doc g x → Docs g (x ∷ [])
    _∷_ : ∀ {x xs} → Doc g x → Docs g xs → Docs g (x ∷⁺ xs)

-- Pretty-printers. A pretty-printer is a function that for every
-- value constructs a matching document.

Pretty-printer : {A : Set} → Grammar A → Set₁
Pretty-printer g = ∀ x → Doc g x

Pretty-printer-for : {A : Set} → Grammar-for A → Set₁
Pretty-printer-for g = ∀ x → Doc (g x) (x , refl)

------------------------------------------------------------------------
-- Derived document combinators

-- A "smart" variant of emb. Can be used to avoid long chains of emb
-- constructors.

embed : ∀ {A B} {g₁ : Grammar A} {g₂ : Grammar B} {x y} →
        (∀ {s} → x ∈ g₁ · s → y ∈ g₂ · s) → Doc g₁ x → Doc g₂ y
embed f (emb g d) = emb (f ∘ g) d
embed f d         = emb f d

-- A document for the empty string.

nil : ∀ {A} {x : A} → Doc (return x) x
nil = embed lemma text
  where
  lemma : ∀ {x s} → [] ∈ string [] · s → x ∈ return x · s
  lemma return-sem = return-sem

-- A document for the given character.

token : ∀ {t} → Doc G.token t
token {t} = embed lemma text
  where
  lemma′ : ∀ {x s} → x ∈ string (t ∷ []) · s → x ≡ t ∷ [] →
           t ∈ G.token · s
  lemma′ (⊛-sem (<$>-sem tok-sem) return-sem) refl = token-sem

  lemma : ∀ {s} → t ∷ [] ∈ string (t ∷ []) · s → t ∈ G.token · s
  lemma t∈ = lemma′ t∈ refl

-- A document for the given character.

tok : ∀ {t} → Doc (G.tok t) t
tok {t} = embed lemma token
  where
  lemma : ∀ {s} → t ∈ G.token · s → t ∈ G.tok t · s
  lemma token-sem = tok-sem

-- Some mapping combinators.

infix 21 <$>_ <$_

<$>_ : ∀ {c A B} {f : A → B} {x} {g : ∞Grammar c A} →
       Doc (♭? g) x → Doc (f G.<$> g) (f x)
<$> d = embed <$>-sem d

<$_ : ∀ {c A B} {x : A} {y} {g : ∞Grammar c B} →
      Doc (♭? g) y → Doc (x G.<$ g) x
<$ d = embed <$-sem d

-- Some sequencing combinators.

infixl 20 _⊛_ _<⊛_ _⊛>_ _<⊛-tt_ _tt-⊛>_

_⊛_ : ∀ {c₁ c₂ A B f x}
        {g₁ : ∞Grammar c₁ (A → B)} {g₂ : ∞Grammar c₂ A} →
      Doc (♭? g₁) f → Doc (♭? g₂) x → Doc (g₁ G.⊛ g₂) (f x)
_⊛_ {g₁ = g₁} {g₂} d₁ d₂ = embed lemma (d₁ ◇ <$> d₂)
  where
  lemma : ∀ {x s} →
          x ∈ (g₁ >>= λ f → f G.<$> g₂) · s → x ∈ g₁ G.⊛ g₂ · s
  lemma (>>=-sem f∈ (<$>-sem x∈)) = ⊛-sem f∈ x∈

_<⊛_ : ∀ {c₁ c₂ A B x y} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B} →
       Doc (♭? g₁) x → Doc (♭? g₂) y → Doc (g₁ G.<⊛ g₂) x
_<⊛_ {g₁ = g₁} {g₂} d₁ d₂ = embed lemma (d₁ ◇ <$ d₂)
  where
  lemma : ∀ {x s} →
          x ∈ (g₁ >>= λ x → x G.<$ g₂) · s → x ∈ g₁ G.<⊛ g₂ · s
  lemma (>>=-sem x∈ (<$-sem y∈)) = <⊛-sem x∈ y∈

_⊛>_ : ∀ {c₁ c₂ A B x y} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B} →
       Doc (♭? g₁) x → Doc (♭? g₂) y → Doc (g₁ G.⊛> g₂) y
_⊛>_ {g₁ = g₁} {g₂} d₁ d₂ = embed lemma (d₁ ◇ d₂)
  where
  lemma : ∀ {y s} →
          y ∈ (g₁ >>= λ _ → g₂) · s → y ∈ g₁ G.⊛> g₂ · s
  lemma (>>=-sem x∈ y∈) = ⊛>-sem x∈ y∈

_<⊛-tt_ : ∀ {c₁ c₂ A B x} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B} →
          Doc (♭? g₁) x → Doc (tt G.<$ g₂) tt → Doc (g₁ G.<⊛ g₂) x
_<⊛-tt_ {g₁ = g₁} {g₂} d₁ d₂ = embed lemma (d₁ <⊛ d₂)
  where
  lemma : ∀ {x s} → x ∈ g₁ G.<⊛ (tt G.<$ g₂) · s → x ∈ g₁ G.<⊛ g₂ · s
  lemma (<⊛-sem x∈ (<$-sem y∈)) = <⊛-sem x∈ y∈

_tt-⊛>_ : ∀ {c₁ c₂ A B x} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B} →
          Doc (tt G.<$ g₁) tt → Doc (♭? g₂) x → Doc (g₁ G.⊛> g₂) x
_tt-⊛>_ {g₁ = g₁} {g₂} d₁ d₂ = embed lemma (d₁ ⊛> d₂)
  where
  lemma : ∀ {x s} → x ∈ (tt G.<$ g₁) G.⊛> g₂ · s → x ∈ g₁ G.⊛> g₂ · s
  lemma (⊛>-sem (<$-sem x∈) y∈) = ⊛>-sem x∈ y∈

-- Document combinators for choices.

left : ∀ {c₁ c₂ A x} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ A} →
       Doc (♭? g₁) x → Doc (g₁ ∣ g₂) x
left d = embed left-sem d

right : ∀ {c₁ c₂ A x} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ A} →
        Doc (♭? g₂) x → Doc (g₁ ∣ g₂) x
right d = embed right-sem d

-- Some Kleene star and plus combinators.

nil-⋆ : ∀ {c A} {g : ∞Grammar c A} → Doc (g ⋆) []
nil-⋆ {A = A} {g} = embed lemma nil
  where
  lemma : ∀ {s} → [] ∈ return {A = List A} [] · s → [] ∈ g ⋆ · s
  lemma return-sem = ⋆-[]-sem

cons-⋆+ : ∀ {c A} {g : ∞Grammar c A} {x xs} →
          Doc (♭? g) x → Doc (g ⋆) xs → Doc (g +) (x ∷ xs)
cons-⋆+ d₁ d₂ = <$> d₁ ⊛ d₂

cons-⋆ : ∀ {c A} {g : ∞Grammar c A} {x xs} →
         Doc (♭? g) x → Doc (g ⋆) xs → Doc (g ⋆) (x ∷ xs)
cons-⋆ d₁ d₂ = embed ⋆-+-sem (cons-⋆+ d₁ d₂)

-- A document for the empty string.

if-true : ∀ b → Pretty-printer (G.if-true b)
if-true true  _  = nil
if-true false ()

-- Documents for the given character.

sat : (p : Char → Bool) → Pretty-printer (G.sat p)
sat p (t , proof) = token ◇ <$> if-true (p t) proof

tok-sat : {p : Char → Bool} → Pretty-printer-for (G.tok-sat p)
tok-sat _ = <$ tok

-- A single space character.

space : Doc (whitespace ⋆) (' ' ∷ [])
space = embed lemma tok
  where
  lemma : ∀ {s} →
          ' ' ∈ G.tok ' ' · s →
          (' ' ∷ []) ∈ whitespace ⋆ · s
  lemma tok-sem = ⋆-+-sem single-space-sem

-- A variant of line (with _⋆ instead of _+ in the grammar).

line⋆ : Doc (tt G.<$ whitespace ⋆) tt
line⋆ = embed lemma line
  where
  lemma : ∀ {s} →
          tt ∈ tt G.<$ whitespace + · s →
          tt ∈ tt G.<$ whitespace ⋆ · s
  lemma (<$-sem w+) = <$-sem (⋆-+-sem w+)

-- Combinators that add a final "line" to the document, nested i
-- steps. (The grammars have to satisfy certain predicates.)

final-line′ : ∀ {A} {g : Grammar A} {x} →
              Trailing-whitespace g → Doc g x → (i : ℕ) → Doc g x
final-line′ trailing d i = embed trailing (d <⊛-tt nest i line⋆)

final-line : ∀ {A} {g : Grammar A} {x} (n : ℕ)
             {trailing : T (is-just (trailing-whitespace n g))} →
             Doc g x → (i : ℕ) → Doc g x
final-line n {trailing} =
  final-line′ (to-witness-T (trailing-whitespace n _) trailing)

-- Trailing-whitespace never holds for grammars of the form g ⋆, but
-- if the list to be pretty-printed has at least one element, then
-- final-line may still work.

final-line-+⋆ : ∀ {c A} {g : ∞Grammar c A} {x xs} (n : ℕ)
                {trailing : T (is-just (trailing-whitespace n (g +)))} →
                Doc (g +) (x ∷ xs) → (i : ℕ) → Doc (g ⋆) (x ∷ xs)
final-line-+⋆ n {trailing} d i =
  embed ⋆-+-sem (final-line n {trailing} d i)

-- A document for the given symbol (and no following whitespace).

symbol : ∀ {s} → Doc (G.symbol s) s
symbol = text <⊛ nil-⋆

-- A document for the given symbol plus a "line".

symbol-line : ∀ {s} → Doc (G.symbol s) s
symbol-line = final-line 1 symbol 0

-- A document for the given symbol plus a space character.

symbol-space : ∀ {s} → Doc (G.symbol s) s
symbol-space = text <⊛ space

-- A combinator for bracketed output, based on one in Wadler's "A
-- prettier printer".

bracket : ∀ {c A x s₁ s₂} {g : ∞Grammar c A} (n : ℕ) →
          {trailing : T (is-just (trailing-whitespace n (♭? g)))} →
          Doc (♭? g) x → Doc (G.symbol s₁ G.⊛> g G.<⊛ G.symbol s₂) x
bracket n {trailing} d =
  group (nest 2 symbol-line
           ⊛>
         final-line n {trailing = trailing} (nest 2 d) 0
           <⊛
         symbol)

mutual

  -- Conversion of pretty-printers for elements into pretty-printers
  -- for lists.

  map⋆ : ∀ {c A} {g : ∞Grammar c A} →
         Pretty-printer (♭? g) → Pretty-printer (g ⋆)
  map⋆ p []       = nil-⋆
  map⋆ p (x ∷ xs) = embed ⋆-+-sem (map+ p (x ∷ xs))

  map+ : ∀ {c A} {g : ∞Grammar c A} →
         Pretty-printer (♭? g) → Pretty-printer (g +)
  map+ p (x ∷ xs) = cons-⋆+ (p x) (map⋆ p xs)

mutual

  -- Conversion of pretty-printers for specific elements into
  -- pretty-printers for specific lists.

  list : ∀ {A} {elem : Grammar-for A} →
         Pretty-printer-for elem →
         Pretty-printer-for (G.list elem)
  list e []       = nil
  list e (x ∷ xs) = <$> (list⁺ e (x ∷ xs))

  list⁺ : ∀ {A} {elem : Grammar-for A} →
          Pretty-printer-for elem →
          Pretty-printer-for (G.list⁺ elem)
  list⁺ e (x ∷ xs) = <$> (e x) ⊛ list e xs

-- A variant of fill. (The grammar has to satisfy a certain
-- predicate.)

fill+ : ∀ {c A} {g : ∞Grammar c A} (n : ℕ)
        {trailing : T (is-just (trailing-whitespace n (♭? g)))} →
        ∀ {xs} → Docs (♭? g) xs → Doc (g +) xs
fill+ {g = g} n {trailing} ds = embed lemma (fill ds)
  where
  trailing! = to-witness-T (trailing-whitespace n (♭? g)) trailing

  lemma′ : ∀ {x xs s₁ s₂} →
           x ∈ ♭? g · s₁ → xs ∈ ♭? g prec-by whitespace + · s₂ →
           x ∷ xs ∈ g + · s₁ ++ s₂
  lemma′           x∈ ⋆-[]-sem = +-sem x∈ ⋆-[]-sem
  lemma′ {s₁ = s₁} x∈ (⋆-+-sem (⊛-sem (<$>-sem (⊛>-sem w+ x′∈)) xs∈)) =
    cast lemma″
         (+-∷-sem (trailing! (<⊛-sem x∈ (⋆-+-sem w+))) (lemma′ x′∈ xs∈))
    where
    lemma″ :
      ∀ {s₂ s₃ s₄} → (s₁ ++ s₂) ++ s₃ ++ s₄ ≡ s₁ ++ (s₂ ++ s₃) ++ s₄
    lemma″ = solve (++-monoid Char)

  lemma : ∀ {s xs} → xs ∈ ♭? g sep-by whitespace + · s → xs ∈ g + · s
  lemma (⊛-sem (<$>-sem x∈) xs∈) = lemma′ x∈ xs∈

-- Variants of map+/map⋆ that use fill. (The grammars have to satisfy
-- a certain predicate.)

map+-fill : ∀ {c A} {g : ∞Grammar c A} (n : ℕ)
            {trailing : T (is-just (trailing-whitespace n (♭? g)))} →
            Pretty-printer (♭? g) →
            Pretty-printer (g +)
map+-fill {g = g} n {trailing} p (x ∷ xs) =
  fill+ n {trailing = trailing} (to-docs x xs)
  where
  to-docs : ∀ x xs → Docs (♭? g) (x ∷ xs)
  to-docs x []        = [ p x ]
  to-docs x (x′ ∷ xs) = p x ∷ to-docs x′ xs

map⋆-fill : ∀ {c A} {g : ∞Grammar c A} (n : ℕ)
            {trailing : T (is-just (trailing-whitespace n (♭? g)))} →
            Pretty-printer (♭? g) →
            Pretty-printer (g ⋆)
map⋆-fill n            p []       = nil-⋆
map⋆-fill n {trailing} p (x ∷ xs) =
  embed ⋆-+-sem (map+-fill n {trailing = trailing} p (x ∷ xs))

max_stars_repo_name: nad/pretty

max_issues_repo_name: nad/pretty

max_forks_repo_name: nad/pretty


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

module Categories.Category.Concrete.Properties where

open import Data.Unit.Polymorphic
open import Function.Equality using (Π; _⟨$⟩_; const; _∘_)
open import Level
open import Relation.Binary using (Setoid)
import Relation.Binary.Reasoning.Setoid as SR

open import Categories.Adjoint using (_⊣_; Adjoint)
open import Categories.Category.Core using (Category)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Category.Concrete
open import Categories.Functor.Core using (Functor)
open import Categories.Functor.Representable using (Representable)
open import Categories.Functor.Properties using (Faithful)
import Categories.Morphism.Reasoning as MR
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)

open Concrete

⊣⇒Representable : {o ℓ e : Level} (C : Category o ℓ e) (conc : Concrete C ℓ e) → (F : Functor (Setoids ℓ e) C) →
  F ⊣ concretize conc  → RepresentablyConcrete C
⊣⇒Representable {_} {ℓ} {e} C conc F L = record
  { conc = conc
  ; representable = record
    { A = F.₀ OneS
    ; Iso = record
      { F⇒G = ntHelper record
        { η = λ X → record
          { _⟨$⟩_ = λ x → L.counit.η X C.∘ F.₁ (const x)
          ; cong = λ i≈j → C.∘-resp-≈ʳ (F.F-resp-≈ λ _ → i≈j)
          }
        ; commute = λ {X} {Y} f {x} {y} x≈y →
            let open C.HomReasoning in begin
            L.counit.η Y C.∘ F.₁ (const (U.₁ f ⟨$⟩ x))          ≈⟨ refl⟩∘⟨ F.F-resp-≈ (λ _ → Π.cong (U.₁ f) x≈y) ⟩
            L.counit.η Y C.∘ F.₁ (U.F₁ f ∘ const y)            ≈⟨ pushʳ F.homomorphism ⟩
            ((L.counit.η Y C.∘ F.₁ (U.₁ f)) C.∘ F.₁ (const y)) ≈⟨ pushˡ (commute L.counit f) ⟩
            f C.∘ L.counit.η X C.∘ F.₁ (const y)               ≈˘⟨ C.identityʳ ⟩
            (f C.∘ L.counit.η X C.∘ F.₁ (const y)) C.∘ C.id    ∎
        }
      ; F⇐G = ntHelper record
        { η = λ c → record
          { _⟨$⟩_ = λ 1⇒c → U.₁ 1⇒c ⟨$⟩ η1
          ; cong = λ i≈j → U.F-resp-≈ i≈j (Setoid.refl (U.₀ (F.₀ OneS)))
          }
        ; commute = λ {X} {Y} f {x} {y} x≈y →
             let module CH = C.HomReasoning in
             let open SR (U.₀ Y) in
             begin
             U.₁ ((f C.∘ x) C.∘ C.id) ⟨$⟩ η1 ≈⟨ U.F-resp-≈ (C.identityʳ CH.○ (CH.refl⟩∘⟨ x≈y)) Srefl ⟩
             U.₁ (f C.∘ y) ⟨$⟩ η1            ≈⟨ U.homomorphism Srefl ⟩
             U.₁ f ⟨$⟩ (U.₁ y ⟨$⟩ η1)         ∎
        }
      ; iso = λ X → record
        { isoˡ = λ {x} {y} x≈y → Setoid.trans (U.₀ X) (L.LRadjunct≈id {OneS} {X} {const x} tt) x≈y
        ; isoʳ = λ {1⇒x} {1⇒y} x≈y →
          let open C.HomReasoning in begin
          L.counit.η X C.∘ F.₁ (const (U.₁ 1⇒x ⟨$⟩ η1))   ≈⟨ (refl⟩∘⟨ F.F-resp-≈ λ _ → U.F-resp-≈ x≈y Srefl) ⟩
          L.counit.η X C.∘ F.₁ (U.₁ 1⇒y ∘ L.unit.η OneS)  ≈⟨ L.RLadjunct≈id {OneS} {X} {1⇒y}  ⟩
          1⇒y ∎
        }
      }
    }
  }
  where
  module C = Category C
  module U = Functor (concretize conc)
  module F = Functor F
  module L = Adjoint L
  open NaturalTransformation
  open MR C
  -- Is this somewhere else?  Should it be?
  OneS : Setoid ℓ e
  OneS = record { Carrier = ⊤ {ℓ} ; _≈_ = λ _ _ → ⊤ {e}}
  η1 : Setoid.Carrier (U.₀ (F.₀ OneS))
  η1 = L.unit.η OneS ⟨$⟩ tt
  Srefl = Setoid.refl (U.₀ (F.₀ OneS))

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories