text:
module IO.File where

open import Base
open import IO

{-# IMPORT System.IO #-}

FilePath = String

data IOMode : Set where
  readMode      : IOMode
  writeMode     : IOMode
  appendMode    : IOMode
  readWriteMode : IOMode

{-# COMPILED_DATA IOMode ReadMode WriteMode AppendMode ReadWriteMode #-}

canRead : IOMode -> Bool
canRead readMode      = true
canRead writeMode     = false
canRead appendMode    = false
canRead readWriteMode = true

canWrite : IOMode -> Bool
canWrite readMode      = false
canWrite writeMode     = true
canWrite appendMode    = true
canWrite readWriteMode = true

CanRead : IOMode -> Set
CanRead m = IsTrue (canRead m)

CanWrite : IOMode -> Set
CanWrite m = IsTrue (canWrite m)

postulate
  Handle : Set

private
 postulate
  hs-openFile : FilePath -> IOMode -> IO Handle
  hs-hClose   : Handle -> IO Unit

  hs-hGetChar : Handle -> IO Char
  hs-hGetLine : Handle -> IO String
  hs-hGetContents : Handle -> IO String

  hs-hPutStr  : Handle -> String -> IO Unit

{-# COMPILED hs-openFile     openFile #-}
{-# COMPILED hs-hClose       hClose #-}
{-# COMPILED hs-hGetChar     hGetChar #-}
{-# COMPILED hs-hGetLine     hGetLine #-}
{-# COMPILED hs-hGetContents hGetContents #-}
{-# COMPILED hs-hPutStr      hPutStr #-}

Handles = List (Handle × IOMode)

abstract
 -- The FileIO monad. Records the list of open handles before and after
 -- a computation. The open handles after the computation may depend on
 -- the computed value.
 data FileIO (A : Set)(hs₁ : Handles)(hs₂ : A -> Handles) : Set where
   fileIO : IO A -> FileIO A hs₁ hs₂

private
 abstract
  unFileIO : forall {A hs f} -> FileIO A hs f -> IO A
  unFileIO (fileIO io) = io

FileIO₋ : Set -> Handles -> Handles -> Set
FileIO₋ A hs₁ hs₂ = FileIO A hs₁ (\_ -> hs₂)

abstract
  openFile : {hs : Handles} -> FilePath -> (m : IOMode) ->
             FileIO Handle hs (\h -> (h , m) :: hs)
  openFile file mode = fileIO (hs-openFile file mode)

infix 30 _∈_
data _∈_ {A : Set}(x : A) : List A -> Set where
  hd : forall {xs} -> x ∈ x :: xs
  tl : forall {y xs} -> x ∈ xs -> x ∈ y :: xs

delete : {A : Set}{x : A}(xs : List A) -> x ∈ xs -> List A
delete [] ()
delete (x :: xs)  hd    = xs
delete (x :: xs) (tl p) = x :: delete xs p

abstract
  hClose : {hs : Handles}{m : IOMode}(h : Handle)(p : (h , m) ∈ hs) ->
           FileIO₋ Unit hs (delete hs p)
  hClose h _ = fileIO (hs-hClose h)

  hGetLine : {hs : Handles}{m : IOMode}{isRead : CanRead m}(h : Handle)
             (p : (h , m) ∈ hs) -> FileIO₋ String hs hs
  hGetLine h _ = fileIO (hs-hGetLine h)

  hGetContents : {hs : Handles}{m : IOMode}{isRead : CanRead m}(h : Handle)
             (p : (h , m) ∈ hs) -> FileIO₋ String hs (delete hs p)
  hGetContents h _ = fileIO (hs-hGetContents h)

abstract
  -- You can only run file computations that don't leave any open
  -- handles.
  runFileIO : {A : Set} -> FileIO₋ A [] [] -> IO A
  runFileIO (fileIO m) = m

abstract
  _>>=_ : forall {A B hs f g} ->
          FileIO A hs f -> ((x : A) -> FileIO B (f x) g) -> FileIO B hs g
  fileIO m >>= k = fileIO (bindIO m \x -> unFileIO (k x))

  return : forall {A hs} -> A -> FileIO₋ A hs hs
  return x = fileIO (returnIO x)


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

module Data.ByteString.Primitive.Int where

open import Agda.Builtin.Nat using (Nat)

{-# FOREIGN GHC import qualified Data.Int #-}
postulate
  Int : Set
  Int64 : Set
  IntToℕ : Int → Nat
  ℕToInt : Nat → Int
  int64Toℕ : Int64 → Nat
  ℕToInt64 : Nat → Int64
{-# COMPILE GHC Int = type (Prelude.Int) #-}
{-# COMPILE GHC Int64 = type (Data.Int.Int64) #-}
{-# COMPILE GHC IntToℕ = (Prelude.fromIntegral) #-}
{-# COMPILE GHC ℕToInt = (Prelude.fromIntegral) #-}
{-# COMPILE GHC int64Toℕ = (Prelude.fromIntegral) #-}
{-# COMPILE GHC ℕToInt64 = (Prelude.fromIntegral) #-}

ext: agda

max_stars_repo_name: semenov-vladyslav/bytes-agda

max_issues_repo_name: semenov-vladyslav/bytes-agda

max_forks_repo_name: semenov-vladyslav/bytes-agda


text:
-- Andreas, 2016-09-13, issue #2177, reported by Andres
--
-- Check me with -v check.ranges:100

postulate A : Set

-- Was an internal error when loading Agda.Primitive
-- (because of range outside the current file).

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import lib.Basics
open import lib.Equivalence2
open import lib.Function2
open import lib.NType2
open import lib.types.Group
open import lib.types.Pi
open import lib.types.Subtype
open import lib.types.Truncation
open import lib.groups.Homomorphism
open import lib.groups.SubgroupProp

module lib.groups.Isomorphism where

GroupStructureIso : ∀ {i j} {GEl : Type i} {HEl : Type j}
  (GS : GroupStructure GEl) (HS : GroupStructure HEl) → Type (lmax i j)
GroupStructureIso GS HS = Σ (GroupStructureHom GS HS) (λ φ → is-equiv (GroupStructureHom.f φ))

infix 30 _≃ᴳˢ_ -- [ˢ] for structures
_≃ᴳˢ_ = GroupStructureIso

GroupIso : ∀ {i j} (G : Group i) (H : Group j) → Type (lmax i j)
GroupIso G H = Σ (G →ᴳ H) (λ φ → is-equiv (GroupHom.f φ))

infix 30 _≃ᴳ_
_≃ᴳ_ = GroupIso

≃ᴳˢ-to-≃ᴳ : ∀ {i j} {G : Group i} {H : Group j}
  → (Group.group-struct G ≃ᴳˢ Group.group-struct H) → (G ≃ᴳ H)
≃ᴳˢ-to-≃ᴳ (φ , φ-is-equiv) = →ᴳˢ-to-→ᴳ φ , φ-is-equiv

≃-to-≃ᴳ : ∀ {i j} {G : Group i} {H : Group j} (e : Group.El G ≃ Group.El H)
  → preserves-comp (Group.comp G) (Group.comp H) (–> e) → G ≃ᴳ H
≃-to-≃ᴳ (f , f-is-equiv) pres-comp = group-hom f pres-comp , f-is-equiv

≃-to-≃ᴳˢ : ∀ {i j} {GEl : Type i} {HEl : Type j}
  {GS : GroupStructure GEl} {HS : GroupStructure HEl} (e : GEl ≃ HEl)
  → preserves-comp (GroupStructure.comp GS) (GroupStructure.comp HS) (–> e)
  → GS ≃ᴳˢ HS
≃-to-≃ᴳˢ (f , f-is-equiv) pres-comp = group-structure-hom f pres-comp , f-is-equiv

private
  inverse-preserves-comp : ∀ {i j} {A : Type i} {B : Type j}
    (A-comp : A → A → A) (B-comp : B → B → B) {f : A → B} (f-ie : is-equiv f)
    → preserves-comp A-comp B-comp f
    → preserves-comp B-comp A-comp (is-equiv.g f-ie)
  inverse-preserves-comp Ac Bc ie pc b₁ b₂ = let open is-equiv ie in
    ap2 (λ w₁ w₂ → g (Bc w₁ w₂)) (! (f-g b₁)) (! (f-g b₂))
    ∙ ! (ap g (pc (g b₁) (g b₂)))
    ∙ g-f (Ac (g b₁) (g b₂))

module GroupStructureIso {i j} {GEl : Type i} {HEl : Type j}
  {GS : GroupStructure GEl} {HS : GroupStructure HEl}
  (iso : GroupStructureIso GS HS) where

  f-shom : GS →ᴳˢ HS
  f-shom = fst iso

  open GroupStructureHom {GS = GS} {HS = HS} f-shom public

  f-is-equiv : is-equiv f
  f-is-equiv = snd iso

  open is-equiv f-is-equiv public

  f-equiv : GEl ≃ HEl
  f-equiv = f , f-is-equiv

  g-shom : HS →ᴳˢ GS
  g-shom = group-structure-hom g (inverse-preserves-comp (GroupStructure.comp GS) (GroupStructure.comp HS) f-is-equiv pres-comp)

  g-is-equiv : is-equiv g
  g-is-equiv = is-equiv-inverse f-is-equiv

  g-equiv : HEl ≃ GEl
  g-equiv = g , g-is-equiv

module GroupIso {i j} {G : Group i} {H : Group j} (iso : GroupIso G H) where

  f-hom : G →ᴳ H
  f-hom = fst iso

  open GroupHom {G = G} {H = H} f-hom public

  f-is-equiv : is-equiv f
  f-is-equiv = snd iso

  open is-equiv f-is-equiv public

  f-equiv : Group.El G ≃ Group.El H
  f-equiv = f , f-is-equiv

  g-hom : H →ᴳ G
  g-hom = group-hom g (inverse-preserves-comp (Group.comp G) (Group.comp H) f-is-equiv pres-comp)

  g-is-equiv : is-equiv g
  g-is-equiv = is-equiv-inverse f-is-equiv

  g-equiv : Group.El H ≃ Group.El G
  g-equiv = g , g-is-equiv

idiso : ∀ {i} (G : Group i) → (G ≃ᴳ G)
idiso G = idhom G , idf-is-equiv _

idsiso : ∀ {i} {GEl : Type i} (GS : GroupStructure GEl) → (GS ≃ᴳˢ GS)
idsiso GS = idshom GS , idf-is-equiv _

{- equality of isomomorphisms -}
abstract
  group-hom=-to-iso= : ∀ {i j} {G : Group i} {H : Group j} {φ ψ : G ≃ᴳ H}
    → GroupIso.f-hom φ == GroupIso.f-hom ψ → φ == ψ
  group-hom=-to-iso= = Subtype=-out (is-equiv-prop ∘sub GroupHom.f)

  group-iso= : ∀ {i j} {G : Group i} {H : Group j} {φ ψ : G ≃ᴳ H}
    → GroupIso.f φ == GroupIso.f ψ → φ == ψ
  group-iso= {H = H} p = group-hom=-to-iso= $ group-hom= p

{- compositions -}

infixr 80 _∘eᴳˢ_ _∘eᴳ_

_∘eᴳˢ_ : ∀ {i j k} {GEl : Type i} {HEl : Type j} {KEl : Type k}
  {GS : GroupStructure GEl} {HS : GroupStructure HEl} {KS : GroupStructure KEl}
  → HS ≃ᴳˢ KS → GS ≃ᴳˢ HS → GS ≃ᴳˢ KS
(φ₂ , ie₂) ∘eᴳˢ (φ₁ , ie₁) = (φ₂ ∘ᴳˢ φ₁ , ie₂ ∘ise ie₁)

_∘eᴳ_ : ∀ {i j k} {G : Group i} {H : Group j} {K : Group k}
  → H ≃ᴳ K → G ≃ᴳ H → G ≃ᴳ K
(φ₂ , ie₂) ∘eᴳ (φ₁ , ie₁) = (φ₂ ∘ᴳ φ₁ , ie₂ ∘ise ie₁)

infixr 10 _≃ᴳˢ⟨_⟩_ _≃ᴳ⟨_⟩_
infix  15 _≃ᴳˢ∎ _≃ᴳ∎

_≃ᴳˢ⟨_⟩_ : ∀ {i j k} {GEl : Type i} {HEl : Type j} {KEl : Type k}
  (GS : GroupStructure GEl) {HS : GroupStructure HEl} {KS : GroupStructure KEl}
  → GS ≃ᴳˢ HS → HS ≃ᴳˢ KS → GS ≃ᴳˢ KS
GS ≃ᴳˢ⟨ e₁ ⟩ e₂ = e₂ ∘eᴳˢ e₁

_≃ᴳ⟨_⟩_ : ∀ {i j k} (G : Group i) {H : Group j} {K : Group k}
  → G ≃ᴳ H → H ≃ᴳ K → G ≃ᴳ K
G ≃ᴳ⟨ e₁ ⟩ e₂ = e₂ ∘eᴳ e₁

_≃ᴳˢ∎ : ∀ {i} {GEl : Type i} (GS : GroupStructure GEl) → (GS ≃ᴳˢ GS)
_≃ᴳˢ∎ = idsiso

_≃ᴳ∎ : ∀ {i} (G : Group i) → (G ≃ᴳ G)
_≃ᴳ∎ = idiso

infixl 120 _⁻¹ᴳˢ _⁻¹ᴳ

_⁻¹ᴳˢ : ∀ {i j} {GEl : Type i} {HEl : Type j} {GS : GroupStructure GEl} {HS : GroupStructure HEl}
  → GS ≃ᴳˢ HS → HS ≃ᴳˢ GS
_⁻¹ᴳˢ {GS = GS} {HS} (φ , ie) = GroupStructureIso.g-shom (φ , ie) , is-equiv-inverse ie

_⁻¹ᴳ : ∀ {i j} {G : Group i} {H : Group j} → G ≃ᴳ H → H ≃ᴳ G
_⁻¹ᴳ {G = G} {H = H} (φ , ie) = GroupIso.g-hom (φ , ie) , is-equiv-inverse ie

{- mimicking notations for equivalences -}

–>ᴳ : ∀ {i j} {G : Group i} {H : Group j} → (G ≃ᴳ H) → (G →ᴳ H)
–>ᴳ = GroupIso.f-hom

<–ᴳ : ∀ {i j} {G : Group i} {H : Group j} → (G ≃ᴳ H) → (H →ᴳ G)
<–ᴳ = GroupIso.g-hom

{- univalence -}

module _ {i} {G H : Group i} (iso : GroupIso G H) where
  private
    module G = Group G
    module H = Group H
    open module φ = GroupIso {G = G} {H = H} iso
  El= = ua f-equiv

  private
    ap3-lemma : ∀ {i j k l} {C : Type i} {D : C → Type j} {E : C → Type k}
      {F : Type l} {c₁ c₂ : C} {d₁ : D c₁} {d₂ : D c₂} {e₁ : E c₁} {e₂ : E c₂}
      (f : (c : C) → D c → E c → F) (p : c₁ == c₂)
      → (d₁ == d₂ [ D ↓ p ]) → (e₁ == e₂ [ E ↓ p ])
      → (f c₁ d₁ e₁ == f c₂ d₂ e₂)
    ap3-lemma f idp idp idp = idp

    ap3-lemma-El : ∀ {i} {G H : Group i}
      (p : Group.El G == Group.El H)
      (q : Group.El-level G == Group.El-level H [ _ ↓ p ])
      (r : Group.group-struct G == Group.group-struct H [ _ ↓ p ])
      → ap Group.El (ap3-lemma (λ a b c → group a {{b}} c) p q r) == p
    ap3-lemma-El idp idp idp = idp

  {- a homomorphism which is an equivalence gives a path between groups -}
  abstract
    uaᴳ : G == H
    uaᴳ =
      ap3-lemma (λ a b c → group a {{b}} c)
        El=
        prop-has-all-paths-↓
        (↓-group-structure= El= ident= inv= comp=)
      where
      ident= : G.ident == H.ident [ (λ C → C) ↓ El= ]
      ident= = ↓-idf-ua-in _ pres-ident

      inv= : G.inv == H.inv [ (λ C → C → C) ↓ El= ]
      inv= =
        ↓-→-from-transp $ λ= λ a →
          transport (λ C → C) El= (G.inv a)
            =⟨ to-transp (↓-idf-ua-in _ idp) ⟩
          f (G.inv a)
            =⟨ pres-inv a ⟩
          H.inv (f a)
            =⟨ ap H.inv (! (to-transp (↓-idf-ua-in _ idp))) ⟩
          H.inv (transport (λ C → C) El= a) =∎

      comp=' : (a : G.El)
        → G.comp a == H.comp (f a) [ (λ C → C → C) ↓ El= ]
      comp=' a =
        ↓-→-from-transp $ λ= λ b →
          transport (λ C → C) El= (G.comp a b)
            =⟨ to-transp (↓-idf-ua-in _ idp) ⟩
          f (G.comp a b)
            =⟨ pres-comp a b ⟩
          H.comp (f a) (f b)
            =⟨ ! (to-transp (↓-idf-ua-in _ idp))
               |in-ctx (λ w → H.comp (f a) w) ⟩
          H.comp (f a) (transport (λ C → C) El= b) =∎

      comp= : G.comp == H.comp [ (λ C → C → C → C) ↓ El= ]
      comp= =
        ↓-→-from-transp $ λ= λ a →
          transport (λ C → C → C) El= (G.comp a)
            =⟨ to-transp (comp=' a) ⟩
          H.comp (f a)
            =⟨ ! (to-transp (↓-idf-ua-in _ idp)) |in-ctx (λ w → H.comp w) ⟩
          H.comp (transport (λ C → C) El= a) =∎

    -- XXX This stretches the naming convention a little bit.
    El=-β : ap Group.El uaᴳ == El=
    El=-β = ap3-lemma-El El= _ _

{- homomorphism from equality of groups -}

abstract
  transp-El-pres-comp : ∀ {i j} {A : Type i} (B : A → Group j) {a₁ a₂ : A} (p : a₁ == a₂)
    → preserves-comp (Group.comp (B a₁)) (Group.comp (B a₂)) (transport (Group.El ∘ B) p)
  transp-El-pres-comp B idp g₁ g₂ = idp

  transp!-El-pres-comp : ∀ {i j} {A : Type i} (B : A → Group j) {a₁ a₂ : A} (p : a₁ == a₂)
    → preserves-comp (Group.comp (B a₂)) (Group.comp (B a₁)) (transport! (Group.El ∘ B) p)
  transp!-El-pres-comp B idp h₁ h₂ = idp

transportᴳ : ∀ {i j} {A : Type i} (B : A → Group j) {a₁ a₂ : A} (p : a₁ == a₂)
  → (B a₁ →ᴳ B a₂)
transportᴳ B p = record {f = transport (Group.El ∘ B) p; pres-comp = transp-El-pres-comp B p}

transport!ᴳ : ∀ {i j} {A : Type i} (B : A → Group j) {a₁ a₂ : A} (p : a₁ == a₂)
  → (B a₂ →ᴳ B a₁)
transport!ᴳ B p = record {f = transport! (Group.El ∘ B) p; pres-comp = transp!-El-pres-comp B p}

abstract
  transpᴳ-is-iso : ∀ {i j} {A : Type i} (B : A → Group j) {a₁ a₂ : A} (p : a₁ == a₂)
    → is-equiv (GroupHom.f (transportᴳ B p))
  transpᴳ-is-iso B idp = idf-is-equiv _

  transp!ᴳ-is-iso : ∀ {i j} {A : Type i} (B : A → Group j) {a₁ a₂ : A} (p : a₁ == a₂)
    → is-equiv (GroupHom.f (transport!ᴳ B p))
  transp!ᴳ-is-iso B idp = idf-is-equiv _

transportᴳ-iso : ∀ {i j} {A : Type i} (B : A → Group j) {a₁ a₂ : A} (p : a₁ == a₂)
  → B a₁ ≃ᴳ B a₂
transportᴳ-iso B p = transportᴳ B p , transpᴳ-is-iso B p

transport!ᴳ-iso : ∀ {i j} {A : Type i} (B : A → Group j) {a₁ a₂ : A} (p : a₁ == a₂)
  → B a₂ ≃ᴳ B a₁
transport!ᴳ-iso B p = transport!ᴳ B p , transp!ᴳ-is-iso B p

coeᴳ : ∀ {i} {G H : Group i} → G == H → (G →ᴳ H)
coeᴳ = transportᴳ (idf _)

coe!ᴳ : ∀ {i} {G H : Group i} → G == H → (H →ᴳ G)
coe!ᴳ = transport!ᴳ (idf _)

coeᴳ-iso : ∀ {i} {G H : Group i} → G == H → G ≃ᴳ H
coeᴳ-iso = transportᴳ-iso (idf _)

coe!ᴳ-iso : ∀ {i} {G H : Group i} → G == H → H ≃ᴳ G
coe!ᴳ-iso = transport!ᴳ-iso (idf _)

abstract
  coeᴳ-β : ∀ {i} {G H : Group i} (iso : G ≃ᴳ H)
    → coeᴳ (uaᴳ iso) == GroupIso.f-hom iso
  coeᴳ-β iso = group-hom= $
      ap coe (El=-β iso)
    ∙ λ= (coe-β (GroupIso.f-equiv iso))

-- triviality

iso-preserves-trivial : ∀ {i j} {G : Group i} {H : Group j}
  → G ≃ᴳ H → is-trivialᴳ G → is-trivialᴳ H
iso-preserves-trivial iso G-is-trivial h =
    ! (GroupIso.f-g iso h)
  ∙ ap (GroupIso.f iso) (G-is-trivial _)
  ∙ GroupIso.pres-ident iso

iso-preserves'-trivial : ∀ {i j} {G : Group i} {H : Group j}
  → G ≃ᴳ H → is-trivialᴳ H → is-trivialᴳ G
iso-preserves'-trivial iso H-is-trivial g =
    ! (GroupIso.g-f iso g)
  ∙ ap (GroupIso.g iso) (H-is-trivial _)
  ∙ GroupHom.pres-ident (GroupIso.g-hom iso)

-- a surjective and injective homomorphism is an isomorphism
module _ {i j} {G : Group i} {H : Group j} (φ : G →ᴳ H)
  (surj : is-surjᴳ φ) (inj : is-injᴳ φ) where
  private
    module G = Group G
    module H = Group H
    module φ = GroupHom φ

    abstract
      instance
        image-prop : (h : H.El) → is-prop (hfiber φ.f h)
        image-prop h = all-paths-is-prop λ {(g₁ , p₁) (g₂ , p₂) →
          pair= (inj g₁ g₂ (p₁ ∙ ! p₂)) prop-has-all-paths-↓}

  surjᴳ-and-injᴳ-is-equiv : is-equiv φ.f
  surjᴳ-and-injᴳ-is-equiv = contr-map-is-equiv
    (λ h → let (g₁ , p₁) = Trunc-rec (idf _) (surj h) in
      has-level-in ((g₁ , p₁) , (λ {(g₂ , p₂) →
        pair= (inj g₁ g₂ (p₁ ∙ ! p₂))
                prop-has-all-paths-↓})))

  surjᴳ-and-injᴳ-iso : G ≃ᴳ H
  surjᴳ-and-injᴳ-iso = φ , surjᴳ-and-injᴳ-is-equiv

-- isomorphisms preserve abelianess.
module _ {i} {G H : Group i} (iso : G ≃ᴳ H) (G-abelian : is-abelian G) where
  private
    module G = Group G
    module H = Group H
    open GroupIso iso

  abstract
    iso-preserves-abelian : is-abelian H
    iso-preserves-abelian h₁ h₂ =
      H.comp h₁ h₂
        =⟨ ap2 H.comp (! $ f-g h₁) (! $ f-g h₂) ⟩
      H.comp (f (g h₁)) (f (g h₂))
        =⟨ ! $ pres-comp (g h₁) (g h₂) ⟩
      f (G.comp (g h₁) (g h₂))
        =⟨ G-abelian (g h₁) (g h₂) |in-ctx f ⟩
      f (G.comp (g h₂) (g h₁))
        =⟨ pres-comp (g h₂) (g h₁) ⟩
      H.comp (f (g h₂)) (f (g h₁))
        =⟨ ap2 H.comp (f-g h₂) (f-g h₁) ⟩
      H.comp h₂ h₁
        =∎

pre∘ᴳ-iso : ∀ {i j k} {G : Group i} {H : Group j} (K : AbGroup k)
  → (G ≃ᴳ H) → (hom-group H K ≃ᴳ hom-group G K)
pre∘ᴳ-iso K iso = ≃-to-≃ᴳ (equiv to from to-from from-to) to-pres-comp where
  to = GroupHom.f (pre∘ᴳ-hom K (–>ᴳ iso))
  to-pres-comp = GroupHom.pres-comp (pre∘ᴳ-hom K (–>ᴳ iso))
  from = GroupHom.f (pre∘ᴳ-hom K (<–ᴳ iso))
  abstract
    to-from : ∀ φ → to (from φ) == φ
    to-from φ = group-hom= $ λ= λ g → ap (GroupHom.f φ) (GroupIso.g-f iso g)

    from-to : ∀ φ → from (to φ) == φ
    from-to φ = group-hom= $ λ= λ h → ap (GroupHom.f φ) (GroupIso.f-g iso h)

post∘ᴳ-iso : ∀ {i j k} (G : Group i) (H : AbGroup j) (K : AbGroup k)
  → (AbGroup.grp H ≃ᴳ AbGroup.grp K) → (hom-group G H ≃ᴳ hom-group G K)
post∘ᴳ-iso G H K iso = ≃-to-≃ᴳ (equiv to from to-from from-to) to-pres-comp where
  to = GroupHom.f (post∘ᴳ-hom G H K (–>ᴳ iso))
  to-pres-comp = GroupHom.pres-comp (post∘ᴳ-hom G H K(–>ᴳ iso))
  from = GroupHom.f (post∘ᴳ-hom G K H (<–ᴳ iso))
  abstract
    to-from : ∀ φ → to (from φ) == φ
    to-from φ = group-hom= $ λ= λ g → GroupIso.f-g iso (GroupHom.f φ g)

    from-to : ∀ φ → from (to φ) == φ
    from-to φ = group-hom= $ λ= λ h → GroupIso.g-f iso (GroupHom.f φ h)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import HoTT
open import cohomology.Exactness
open import cohomology.FunctionOver

{- Splitting Lemma - Right Split
   Assume an exact sequence:

             φ   ψ
       0 → G → H → K

   where H is abelian. If ψ has a right inverse χ, then H == G × K. Over
   this path φ becomes the natural injection and ψ the natural projection.

   The only non-private terms are [iso], [φ-over-iso], and [ψ-over-iso].
-}

module cohomology.SplitExactRight {i} {L G H K : Group i}
  (H-abelian : is-abelian H) (φ : G →ᴳ H) (ψ : H →ᴳ K) where

private
  module G = Group G
  module H = Group H
  module K = Group K
  module φ = GroupHom φ
  module ψ = GroupHom ψ

module SplitExactRight
  (ex : is-exact-seq (L ⟨ cst-hom ⟩→ G ⟨ φ ⟩→ H ⟨ ψ ⟩→ K ⊣|))
  (χ : K →ᴳ H) (χ-rinv : (k : K.El) → ψ.f (GroupHom.f χ k) == k)
  where

  private
    module χ = GroupHom χ

    {- H == Ker ψ × Im χ -}

    ker-part : H →ᴳ Ker ψ
    ker-part = ker-hom ψ
      (comp-hom H-abelian (idhom H) (inv-hom H H-abelian ∘ᴳ (χ ∘ᴳ ψ)))
      (λ h →
        ψ.f (H.comp h (H.inv (χ.f (ψ.f h))))
          =⟨ ψ.pres-comp h (H.inv (χ.f (ψ.f h))) ⟩
        K.comp (ψ.f h) (ψ.f (H.inv (χ.f (ψ.f h))))
          =⟨ ! (χ.pres-inv (ψ.f h))
             |in-ctx (λ w → K.comp (ψ.f h) (ψ.f w)) ⟩
        K.comp (ψ.f h) (ψ.f (χ.f (K.inv (ψ.f h))))
          =⟨ χ-rinv (K.inv (ψ.f h)) |in-ctx (λ w → K.comp (ψ.f h) w) ⟩
        K.comp (ψ.f h) (K.inv (ψ.f h))
          =⟨ K.invr (ψ.f h) ⟩
        K.ident ∎)

    ker-part-kerψ : (h : H.El) (p : ψ.f h == K.ident)
      → GroupHom.f ker-part h == (h , p)
    ker-part-kerψ h p = pair=
      (H.comp h (H.inv (χ.f (ψ.f h)))
         =⟨ p |in-ctx (λ w → H.comp h (H.inv (χ.f w))) ⟩
       H.comp h (H.inv (χ.f K.ident))
         =⟨ χ.pres-ident |in-ctx (λ w → H.comp h (H.inv w)) ⟩
       H.comp h (H.inv H.ident)
         =⟨ group-inv-ident H |in-ctx H.comp h ⟩
       H.comp h H.ident
         =⟨ H.unitr h ⟩
       h ∎)
      (prop-has-all-paths-↓ (K.El-level _ _))

    ker-part-imχ : (h : H.El) → Trunc -1 (Σ K.El (λ k → χ.f k == h))
      → GroupHom.f ker-part h == Group.ident (Ker ψ)
    ker-part-imχ h = Trunc-rec (Group.El-level (Ker ψ) _ _) $
      (λ {(k , p) → pair=
        (H.comp h (H.inv (χ.f (ψ.f h)))
           =⟨ ! p |in-ctx (λ w → H.comp w (H.inv (χ.f (ψ.f w)))) ⟩
         H.comp (χ.f k) (H.inv (χ.f (ψ.f (χ.f k))))
           =⟨ χ-rinv k |in-ctx (λ w → H.comp (χ.f k) (H.inv (χ.f w))) ⟩
         H.comp (χ.f k) (H.inv (χ.f k))
           =⟨ H.invr (χ.f k) ⟩
         H.ident ∎)
        (prop-has-all-paths-↓ (K.El-level _ _))})

    im-part : H →ᴳ Im χ
    im-part = im-in-hom χ ∘ᴳ ψ

    im-part-kerψ : (h : H.El) → ψ.f h == K.ident
      → GroupHom.f im-part h == Group.ident (Im χ)
    im-part-kerψ h p = pair=
      (ap χ.f p ∙ χ.pres-ident)
      (prop-has-all-paths-↓ Trunc-level)

    im-part-imχ : (h : H.El) (s : Trunc -1 (Σ K.El (λ k → χ.f k == h)))
      → GroupHom.f im-part h == (h , s)
    im-part-imχ h s = pair=
      (Trunc-rec (Group.El-level H _ _)
        (λ {(k , p) →
          χ.f (ψ.f h)        =⟨ ! p |in-ctx (χ.f ∘ ψ.f) ⟩
          χ.f (ψ.f (χ.f k))  =⟨ χ-rinv k |in-ctx χ.f ⟩
          χ.f k              =⟨ p ⟩
          h ∎})
        s)
      (prop-has-all-paths-↓ Trunc-level)

    decomp : H →ᴳ Ker ψ ×ᴳ Im χ
    decomp = ×ᴳ-hom-in ker-part im-part

    decomp-is-equiv : is-equiv (GroupHom.f decomp)
    decomp-is-equiv = is-eq _ dinv decomp-dinv dinv-decomp
      where
      dinv : Group.El (Ker ψ ×ᴳ Im χ) → H.El
      dinv ((h₁ , _) , (h₂ , _)) = H.comp h₁ h₂

      decomp-dinv : ∀ s → GroupHom.f decomp (dinv s) == s
      decomp-dinv ((h₁ , kr) , (h₂ , im)) = pair×=
        (GroupHom.f ker-part (H.comp h₁ h₂)
           =⟨ GroupHom.pres-comp ker-part h₁ h₂ ⟩
         Group.comp (Ker ψ) (GroupHom.f ker-part h₁) (GroupHom.f ker-part h₂)
           =⟨ ker-part-kerψ h₁ kr
              |in-ctx (λ w → Group.comp (Ker ψ) w (GroupHom.f ker-part h₂)) ⟩
         Group.comp (Ker ψ) (h₁ , kr) (GroupHom.f ker-part h₂)
           =⟨ ker-part-imχ h₂ im
              |in-ctx (λ w → Group.comp (Ker ψ) (h₁ , kr) w) ⟩
         Group.comp (Ker ψ) (h₁ , kr) (Group.ident (Ker ψ))
           =⟨ Group.unitr (Ker ψ) (h₁ , kr) ⟩
         (h₁ , kr) ∎)
        (GroupHom.f im-part (H.comp h₁ h₂)
           =⟨ GroupHom.pres-comp im-part h₁ h₂ ⟩
         Group.comp (Im χ) (GroupHom.f im-part h₁) (GroupHom.f im-part h₂)
           =⟨ im-part-kerψ h₁ kr
              |in-ctx (λ w → Group.comp (Im χ) w (GroupHom.f im-part h₂)) ⟩
         Group.comp (Im χ) (Group.ident (Im χ)) (GroupHom.f im-part h₂)
           =⟨ im-part-imχ h₂ im
              |in-ctx (λ w → Group.comp (Im χ) (Group.ident (Im χ)) w) ⟩
         Group.comp (Im χ) (Group.ident (Im χ)) (h₂ , im)
           =⟨ Group.unitl (Im χ) (h₂ , im) ⟩
         (h₂ , im) ∎)

      dinv-decomp : ∀ h → dinv (GroupHom.f decomp h) == h
      dinv-decomp h =
        H.comp (H.comp h (H.inv (χ.f (ψ.f h)))) (χ.f (ψ.f h))
          =⟨ H.assoc h (H.inv (χ.f (ψ.f h))) (χ.f (ψ.f h)) ⟩
        H.comp h (H.comp (H.inv (χ.f (ψ.f h))) (χ.f (ψ.f h)))
          =⟨ H.invl (χ.f (ψ.f h)) |in-ctx H.comp h ⟩
        H.comp h H.ident
          =⟨ H.unitr h ⟩
        h ∎

    decomp-equiv : H.El ≃ Group.El (Ker ψ ×ᴳ Im χ)
    decomp-equiv = (_ , decomp-is-equiv)

    decomp-iso : H == Ker ψ ×ᴳ Im χ
    decomp-iso = group-ua (decomp , decomp-is-equiv)

    {- G == Ker ψ -}

    ker-in-φ : G →ᴳ Ker ψ
    ker-in-φ = ker-hom ψ φ (λ g → itok (exact-get ex 1) (φ.f g) [ g , idp ])

    ker-in-φ-is-equiv : is-equiv (GroupHom.f ker-in-φ)
    ker-in-φ-is-equiv = surj-inj-is-equiv ker-in-φ inj surj
      where
      inj = zero-kernel-injective ker-in-φ
        (λ g p → Trunc-rec (G.El-level _ _)
          (λ {(_ , q) → ! q}) (ktoi (exact-get ex 0) g (ap fst p)))

      surj = λ {(h , p) → Trunc-fmap
        (λ {(g , q) → (g , pair= q (prop-has-all-paths-↓ (K.El-level _ _)))})
        (ktoi (exact-get ex 1) h p)}

    G-iso-Kerψ : G == Ker ψ
    G-iso-Kerψ = group-ua (ker-in-φ , ker-in-φ-is-equiv)

    {- K == Im χ -}

    im-in-χ-is-equiv : is-equiv (GroupHom.f (im-in-hom χ))
    im-in-χ-is-equiv = surj-inj-is-equiv (im-in-hom χ) inj (im-in-surj χ)
      where
      inj = zero-kernel-injective (im-in-hom χ)
        (λ k p → ! (χ-rinv k) ∙ ap ψ.f (ap fst p) ∙ ψ.pres-ident)

    K-iso-Imχ : K == Im χ
    K-iso-Imχ = group-ua (im-in-hom χ , im-in-χ-is-equiv)

  {- H == G ×ᴳ K -}

  iso : H == G ×ᴳ K
  iso = decomp-iso ∙ ap2 _×ᴳ_ (! G-iso-Kerψ) (! K-iso-Imχ)

  private

    decomp-φ = ×ᴳ-hom-in ker-in-φ (cst-hom {G = G} {H = Im χ})
    ψ-dinv = ψ ∘ᴳ ×ᴳ-sum-hom H-abelian (ker-inj ψ) (im-inj χ)

    φ-over-decomp : φ == decomp-φ [ (λ J → G →ᴳ J) ↓ decomp-iso ]
    φ-over-decomp = codomain-over-iso $ codomain-over-equiv φ.f _ ▹ lemma
      where
      lemma : GroupHom.f decomp ∘ φ.f == GroupHom.f decomp-φ
      lemma = λ= (λ g → pair×=
        (ker-part-kerψ (φ.f g) (itok (exact-get ex 1) (φ.f g) [ g , idp ]))
        (im-part-kerψ (φ.f g) (itok (exact-get ex 1) (φ.f g) [ g , idp ])))

    ψ-over-decomp : ψ == ψ-dinv [ (λ J → J →ᴳ K) ↓ decomp-iso ]
    ψ-over-decomp = domain-over-iso $ domain!-over-equiv ψ.f _

    id-over-G-iso : idhom _ == ker-in-φ [ (λ J → G →ᴳ J) ↓ G-iso-Kerψ ]
    id-over-G-iso = codomain-over-iso $ codomain-over-equiv (idf _) _

    φ-over-G-iso : φ == ker-inj ψ [ (λ J → J →ᴳ H) ↓ G-iso-Kerψ ]
    φ-over-G-iso =
      domain-over-iso $ domain-over-equiv (GroupHom.f (ker-inj ψ)) _

    ψ|imχ-over-K-iso : idhom K == ψ ∘ᴳ im-inj χ
      [ (λ J → J →ᴳ K) ↓ K-iso-Imχ ]
    ψ|imχ-over-K-iso = domain-over-iso $ domain!-over-equiv (idf _) _ ▹ lemma
      where
      lemma : <– (_ , im-in-χ-is-equiv) == ψ.f ∘ GroupHom.f (im-inj χ)
      lemma = λ= (λ {(h , s) →
        Trunc-elim {P = λ s' → <– (_ , im-in-χ-is-equiv) (h , s') == ψ.f h}
          (λ _ → K.El-level _ _) (λ {(k , p) → ! (χ-rinv k) ∙ ap ψ.f p}) s})

    φ-over-G-K-isos : decomp-φ == ×ᴳ-inl
      [ (λ J → G →ᴳ J) ↓ ap2 _×ᴳ_ (! G-iso-Kerψ) (! K-iso-Imχ) ]
    φ-over-G-K-isos = ↓-ap2-in _ _×ᴳ_ $ transport
      (λ q → decomp-φ == ×ᴳ-inl [ (λ {(J₁ , J₂) → G →ᴳ J₁ ×ᴳ J₂}) ↓ q ])
      (! (pair×=-split-l (! G-iso-Kerψ) (! K-iso-Imχ)))
      (l ∙ᵈ r)
      where
      l : decomp-φ == ×ᴳ-hom-in (idhom G) (cst-hom {G = G} {H = Im χ})
        [ (λ {(J₁ , J₂) → G →ᴳ J₁ ×ᴳ J₂})
          ↓ ap (λ J → J , Im χ) (! G-iso-Kerψ) ]
      l = ↓-ap-in _ (λ J → J , Im χ)
            (ap↓ (λ θ → ×ᴳ-hom-in θ (cst-hom {G = G} {H = Im χ}))
              (!ᵈ id-over-G-iso))

      r : ×ᴳ-hom-in (idhom G) (cst-hom {H = Im χ}) == ×ᴳ-inl
        [ (λ {(J₁ , J₂) → G →ᴳ J₁ ×ᴳ J₂})
          ↓ ap (λ J → G , J) (! K-iso-Imχ) ]
      r = ↓-ap-in _ (λ J → G , J)
            (apd (λ J → ×ᴳ-hom-in (idhom G)
              (cst-hom {G = G} {H = J})) (! K-iso-Imχ))

    ψ-over-G-K-isos : ψ-dinv == ×ᴳ-snd {G = G}
      [ (λ J → J →ᴳ K) ↓ ap2 _×ᴳ_ (! G-iso-Kerψ) (! K-iso-Imχ) ]
    ψ-over-G-K-isos = ↓-ap2-in _ _×ᴳ_ $ transport
      (λ q → ψ-dinv == (×ᴳ-snd {G = G})
        [ (λ {(J₁ , J₂) → J₁ ×ᴳ J₂ →ᴳ K}) ↓ q ])
      (! (pair×=-split-l (! G-iso-Kerψ) (! K-iso-Imχ)))
      (l ∙ᵈ (m ◃ r))
      where
      l : ψ-dinv == ψ ∘ᴳ ×ᴳ-sum-hom H-abelian φ (im-inj χ)
          [ (λ {(J₁ , J₂) → J₁ ×ᴳ J₂ →ᴳ K})
            ↓ ap (λ J → J , Im χ) (! G-iso-Kerψ) ]
      l = ↓-ap-in _ (λ J → J , Im χ)
        (ap↓ (λ θ → ψ ∘ᴳ ×ᴳ-sum-hom H-abelian θ (im-inj χ))
          (!ᵈ φ-over-G-iso))

      m : ψ ∘ᴳ ×ᴳ-sum-hom H-abelian φ (im-inj χ)
          == (ψ ∘ᴳ im-inj χ) ∘ᴳ ×ᴳ-snd {G = G}
      m = hom= _ _ $ λ= $ (λ {(g , (h , _)) →
        ψ.f (H.comp (φ.f g) h)
          =⟨ ψ.pres-comp (φ.f g) h ⟩
        K.comp (ψ.f (φ.f g)) (ψ.f h)
          =⟨ itok (exact-get ex 1) (φ.f g) [ g , idp ]
             |in-ctx (λ w → K.comp w (ψ.f h))  ⟩
        K.comp K.ident (ψ.f h)
          =⟨ K.unitl (ψ.f h) ⟩
        ψ.f h ∎})

      r : (ψ ∘ᴳ im-inj χ) ∘ᴳ ×ᴳ-snd {G = G} == ×ᴳ-snd {G = G}
          [ (λ {(J₁ , J₂) → J₁ ×ᴳ J₂ →ᴳ K})
            ↓ (ap (λ J → G , J) (! K-iso-Imχ)) ]
      r = ↓-ap-in _ (λ J → G , J)
            (ap↓ (λ θ → θ ∘ᴳ ×ᴳ-snd {G = G}) (!ᵈ ψ|imχ-over-K-iso))

  φ-over-iso : φ == ×ᴳ-inl [ (λ J → G →ᴳ J) ↓ iso ]
  φ-over-iso = φ-over-decomp ∙ᵈ φ-over-G-K-isos

  ψ-over-iso : ψ == (×ᴳ-snd {G = G}) [ (λ J → J →ᴳ K) ↓ iso ]
  ψ-over-iso = ψ-over-decomp ∙ᵈ ψ-over-G-K-isos

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
open import Oscar.Prelude
open import Oscar.Class.Symmetry
open import Oscar.Class.Symmetrical
import Oscar.Data.Proposequality

module Oscar.Class.Symmetrical.Symmetry where

module _
    {𝔬} {𝔒 : Ø 𝔬}
    {ℓ} {_∼_ : 𝔒 → 𝔒 → Ø ℓ}
    ⦃ _ : Symmetry.class _∼_ ⦄
  where

  instance

    Symmetrical𝓢ymmetry : Symmetrical _∼_ (λ x∼y y∼x → x∼y → y∼x)
    Symmetrical𝓢ymmetry .𝓢ymmetrical.symmetrical _ _ = symmetry


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties imply others
------------------------------------------------------------------------

module Relation.Binary.Consequences where

open import Relation.Binary.Core hiding (refl)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality.Core
open import Function
open import Data.Sum
open import Data.Product
open import Data.Empty

-- Some of the definitions can be found in the following module:

open import Relation.Binary.Consequences.Core public

trans∧irr⟶asym :
  ∀ {a ℓ₁ ℓ₂} {A : Set a} → {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
  Reflexive _≈_ →
  Transitive _<_ → Irreflexive _≈_ _<_ → Asymmetric _<_
trans∧irr⟶asym refl trans irrefl = λ x<y y<x →
  irrefl refl (trans x<y y<x)

irr∧antisym⟶asym :
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
  Irreflexive _≈_ _<_ → Antisymmetric _≈_ _<_ → Asymmetric _<_
irr∧antisym⟶asym irrefl antisym = λ x<y y<x →
  irrefl (antisym x<y y<x) x<y

asym⟶antisym :
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
  Asymmetric _<_ → Antisymmetric _≈_ _<_
asym⟶antisym asym x<y y<x = ⊥-elim (asym x<y y<x)

asym⟶irr :
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
  _<_ Respects₂ _≈_ → Symmetric _≈_ →
  Asymmetric _<_ → Irreflexive _≈_ _<_
asym⟶irr {_<_ = _<_} resp sym asym {x} {y} x≈y x<y = asym x<y y<x
  where
  y<y : y < y
  y<y = proj₂ resp x≈y x<y
  y<x : y < x
  y<x = proj₁ resp (sym x≈y) y<y

total⟶refl :
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_∼_ : Rel A ℓ₂} →
  _∼_ Respects₂ _≈_ → Symmetric _≈_ →
  Total _∼_ → _≈_ ⇒ _∼_
total⟶refl {_≈_ = _≈_} {_∼_ = _∼_} resp sym total = refl
  where
  refl : _≈_ ⇒ _∼_
  refl {x} {y} x≈y with total x y
  ...              | inj₁ x∼y = x∼y
  ...              | inj₂ y∼x =
    proj₁ resp x≈y (proj₂ resp (sym x≈y) y∼x)

total+dec⟶dec :
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_≤_ : Rel A ℓ₂} →
  _≈_ ⇒ _≤_ → Antisymmetric _≈_ _≤_ →
  Total _≤_ → Decidable _≈_ → Decidable _≤_
total+dec⟶dec {_≈_ = _≈_} {_≤_ = _≤_} refl antisym total _≟_ = dec
  where
  dec : Decidable _≤_
  dec x y with total x y
  ... | inj₁ x≤y = yes x≤y
  ... | inj₂ y≤x with x ≟ y
  ...   | yes  x≈y = yes (refl x≈y)
  ...   | no  ¬x≈y = no (λ x≤y → ¬x≈y (antisym x≤y y≤x))

tri⟶asym :
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
  Trichotomous _≈_ _<_ → Asymmetric _<_
tri⟶asym tri {x} {y} x<y x>y with tri x y
... | tri< _   _ x≯y = x≯y x>y
... | tri≈ _   _ x≯y = x≯y x>y
... | tri> x≮y _ _   = x≮y x<y

tri⟶irr :
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
  _<_ Respects₂ _≈_ → Symmetric _≈_ →
  Trichotomous _≈_ _<_ → Irreflexive _≈_ _<_
tri⟶irr resp sym tri = asym⟶irr resp sym (tri⟶asym tri)

tri⟶dec≈ :
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
  Trichotomous _≈_ _<_ → Decidable _≈_
tri⟶dec≈ compare x y with compare x y
... | tri< _ x≉y _ = no  x≉y
... | tri≈ _ x≈y _ = yes x≈y
... | tri> _ x≉y _ = no  x≉y

tri⟶dec< :
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
  Trichotomous _≈_ _<_ → Decidable _<_
tri⟶dec< compare x y with compare x y
... | tri< x<y _ _ = yes x<y
... | tri≈ x≮y _ _ = no  x≮y
... | tri> x≮y _ _ = no  x≮y

map-NonEmpty : ∀ {a b p q} {A : Set a} {B : Set b}
                 {P : REL A B p} {Q : REL A B q} →
               P ⇒ Q → NonEmpty P → NonEmpty Q
map-NonEmpty f x = nonEmpty (f (NonEmpty.proof x))


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.RingSolver.Examples where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Int.Base hiding (_+_ ; _·_ ; _-_)
open import Cubical.Data.List

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.RingSolver.ReflectionSolving

private
  variable
    ℓ : Level

module Test (R : CommRing ℓ) where
  open CommRingStr (snd R)

  _ : 0r ≡ 0r
  _ = solve R

  _ :   1r · (1r + 0r)
      ≡ (1r · 0r) + 1r
  _ = solve R

  _ :   1r · 0r + (1r - 1r)
      ≡ 0r - 0r
  _ = solve R

  _ : (x : fst R) → x ≡ x
  _ = solve R

  _ : (x y : fst R) → x ≡ x
  _ = solve R

  _ : (x y : fst R) → x + y ≡ y + x
  _ = solve R

  _ : (x y : fst R) → (x + y) · (x - y) ≡ x · x - y · y
  _ = solve R

  {-
    A bigger example, copied from the other example files:
  -}
  _ : (x y z : (fst R)) → (x + y) · (x + y) · (x + y) · (x + y)
                ≡ x · x · x · x + (fromℤ R 4) · x · x · x · y + (fromℤ R 6) · x · x · y · y
                  + (fromℤ R 4) · x · y · y · y + y · y · y · y
  _ = solve R

  {-
    Examples that used to fail (see #513):
  -}

  _ : (x : (fst R)) → x · 0r ≡ 0r
  _ = solve R

  _ : (x y z : (fst R)) → x · (y - z) ≡ x · y - x · z
  _ = solve R

  {-
    Keep in mind, that the solver can lead to wrong error locations.
    For example, the commented code below tries to solve an equation that does not hold,
    with the result of an error at the wrong location.

  _ : (x y : (fst R)) → x ≡ y
  _ = solve R
  -}

module TestInPlaceSolving (R : CommRing ℓ) where
   open CommRingStr (snd R)

   testWithOneVariabl : (x : fst R) → x + 0r ≡ 0r + x
   testWithOneVariabl x = solveInPlace R (x ∷ [])

   testEquationalReasoning : (x : fst R) → x + 0r ≡ 0r + x
   testEquationalReasoning x =
     x + 0r                       ≡⟨solveIn R withVars (x ∷ []) ⟩
     0r + x ∎

   testWithTwoVariables :  (x y : fst R) → x + y ≡ y + x
   testWithTwoVariables x y =
     x + y                      ≡⟨solveIn R withVars (x ∷ y ∷ []) ⟩
     y + x ∎

   {-
     So far, solving during equational reasoning has a serious
     restriction:
     The solver identifies variables by deBruijn indices and the variables
     appearing in the equations to solve need to have indices 0,...,n. This
     entails that in the following code, the order of 'p' and 'x' cannot be
     switched.
   -}
   testEquationalReasoning' :  (p : (y : fst R) → 0r + y ≡ 1r) (x : fst R) → x + 0r ≡ 1r
   testEquationalReasoning' p x =
     x + 0r              ≡⟨solveIn R withVars (x ∷ []) ⟩
     0r + x              ≡⟨ p x ⟩
     1r ∎

max_stars_repo_name: ecavallo/cubical

max_issues_repo_name: ecavallo/cubical

max_forks_repo_name: ecavallo/cubical


text:
------------------------------------------------------------------------
-- Kuratowski finite subsets
------------------------------------------------------------------------

-- Based on Frumin, Geuvers, Gondelman and van der Weide's "Finite
-- Sets in Homotopy Type Theory".

{-# OPTIONS --cubical --safe #-}

import Equality.Path as P

module Finite-subset.Kuratowski
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

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

open import Bijection equality-with-J using (_↔_)
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
import Finite-subset.Listed eq as L
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Truncation.Propositional eq as Trunc
  using (∥_∥; _∥⊎∥_)
open import Monad equality-with-J as M using (Raw-monad; Monad)

private
  variable
    a b p   : Level
    A B     : Type a
    P       : A → Type p
    f g     : (x : A) → P x
    l x y z : A
    m n     : ℕ

------------------------------------------------------------------------
-- Kuratowski finite subsets

-- Kuratowski finite subsets of a given type.

infixr 5 _∪_

data Finite-subset-of (A : Type a) : Type a where
  ∅         : Finite-subset-of A
  singleton : A → Finite-subset-of A
  _∪_       : Finite-subset-of A → Finite-subset-of A →
              Finite-subset-of A
  ∅∪ᴾ       : ∅ ∪ x P.≡ x
  idem-sᴾ   : singleton x ∪ singleton x P.≡ singleton x
  assocᴾ    : x ∪ (y ∪ z) P.≡ (x ∪ y) ∪ z
  commᴾ     : x ∪ y P.≡ y ∪ x
  is-setᴾ   : P.Is-set (Finite-subset-of A)

-- Variants of some of the constructors.

∅∪ : ∅ ∪ x ≡ x
∅∪ = _↔_.from ≡↔≡ ∅∪ᴾ

idem-s : singleton x ∪ singleton x ≡ singleton x
idem-s = _↔_.from ≡↔≡ idem-sᴾ

assoc : x ∪ (y ∪ z) ≡ (x ∪ y) ∪ z
assoc = _↔_.from ≡↔≡ assocᴾ

comm : x ∪ y ≡ y ∪ x
comm = _↔_.from ≡↔≡ commᴾ

is-set : Is-set (Finite-subset-of A)
is-set = _↔_.from (H-level↔H-level 2) is-setᴾ

-- ∅ is a right identity for _∪_.

∪∅ : x ∪ ∅ ≡ x
∪∅ {x = x} =
  x ∪ ∅  ≡⟨ comm ⟩
  ∅ ∪ x  ≡⟨ ∅∪ ⟩∎
  x      ∎

------------------------------------------------------------------------
-- Eliminators

-- A dependent eliminator, expressed using paths.

record Elimᴾ {A : Type a} (P : Finite-subset-of A → Type p) :
             Type (a ⊔ p) where
  field
    ∅ʳ         : P ∅
    singletonʳ : ∀ x → P (singleton x)
    ∪ʳ         : P x → P y → P (x ∪ y)
    ∅∪ʳ        : (p : P x) →
                 P.[ (λ i → P (∅∪ᴾ {x = x} i)) ] ∪ʳ ∅ʳ p ≡ p
    idem-sʳ    : ∀ x →
                 P.[ (λ i → P (idem-sᴾ {x = x} i)) ]
                   ∪ʳ (singletonʳ x) (singletonʳ x) ≡ singletonʳ x
    assocʳ     : (p : P x) (q : P y) (r : P z) →
                 P.[ (λ i → P (assocᴾ {x = x} {y = y} {z = z} i)) ]
                   ∪ʳ p (∪ʳ q r) ≡ ∪ʳ (∪ʳ p q) r
    commʳ      : (p : P x) (q : P y) →
                 P.[ (λ i → P (commᴾ {x = x} {y = y} i)) ]
                   ∪ʳ p q ≡ ∪ʳ q p
    is-setʳ    : ∀ x → P.Is-set (P x)

open Elimᴾ public

elimᴾ : Elimᴾ P → (x : Finite-subset-of A) → P x
elimᴾ {A = A} {P = P} e = helper
  where
  module E = Elimᴾ e

  helper : (x : Finite-subset-of A) → P x
  helper ∅                                  = E.∅ʳ
  helper (singleton x)                      = E.singletonʳ x
  helper (x ∪ y)                            = E.∪ʳ (helper x) (helper y)
  helper (∅∪ᴾ {x = x} i)                    = E.∅∪ʳ (helper x) i
  helper (idem-sᴾ i)                        = E.idem-sʳ _ i
  helper (assocᴾ {x = x} {y = y} {z = z} i) = E.assocʳ
                                                (helper x) (helper y)
                                                (helper z) i
  helper (commᴾ {x = x} {y = y} i)          = E.commʳ
                                                (helper x) (helper y) i
  helper (is-setᴾ x y i j)                  =
    P.heterogeneous-UIP E.is-setʳ (is-setᴾ x y)
      (λ i → helper (x i)) (λ i → helper (y i)) i j

-- A non-dependent eliminator, expressed using paths.

record Recᴾ (A : Type a) (B : Type b) : Type (a ⊔ b) where
  field
    ∅ʳ         : B
    singletonʳ : A → B
    ∪ʳ         : Finite-subset-of A → Finite-subset-of A → B → B → B
    ∅∪ʳ        : ∀ x p → ∪ʳ ∅ x ∅ʳ p P.≡ p
    idem-sʳ    : ∀ x →
                 ∪ʳ (singleton x) (singleton x)
                    (singletonʳ x) (singletonʳ x) P.≡
                 singletonʳ x
    assocʳ     : ∀ p q r →
                 ∪ʳ x (y ∪ z) p (∪ʳ y z q r) P.≡
                 ∪ʳ (x ∪ y) z (∪ʳ x y p q) r
    commʳ      : ∀ p q → ∪ʳ x y p q P.≡ ∪ʳ y x q p
    is-setʳ    : P.Is-set B

open Recᴾ public

recᴾ : Recᴾ A B → Finite-subset-of A → B
recᴾ r = elimᴾ e
  where
  module R = Recᴾ r

  e : Elimᴾ _
  e .∅ʳ                 = R.∅ʳ
  e .singletonʳ         = R.singletonʳ
  e .∪ʳ {x = x} {y = y} = R.∪ʳ x y
  e .∅∪ʳ {x = x}        = R.∅∪ʳ x
  e .idem-sʳ            = R.idem-sʳ
  e .assocʳ             = R.assocʳ
  e .commʳ              = R.commʳ
  e .is-setʳ _          = R.is-setʳ

-- A dependent eliminator, expressed using equality.

record Elim {A : Type a} (P : Finite-subset-of A → Type p) :
            Type (a ⊔ p) where
  field
    ∅ʳ         : P ∅
    singletonʳ : ∀ x → P (singleton x)
    ∪ʳ         : P x → P y → P (x ∪ y)
    ∅∪ʳ        : (p : P x) → subst P (∅∪ {x = x}) (∪ʳ ∅ʳ p) ≡ p
    idem-sʳ    : ∀ x →
                 subst P (idem-s {x = x})
                         (∪ʳ (singletonʳ x) (singletonʳ x)) ≡
                 singletonʳ x
    assocʳ     : (p : P x) (q : P y) (r : P z) →
                 subst P (assoc {x = x} {y = y} {z = z})
                         (∪ʳ p (∪ʳ q r)) ≡
                 ∪ʳ (∪ʳ p q) r
    commʳ      : (p : P x) (q : P y) →
                 subst P (comm {x = x} {y = y}) (∪ʳ p q) ≡ ∪ʳ q p
    is-setʳ    : ∀ x → Is-set (P x)

open Elim public

elim : Elim P → (x : Finite-subset-of A) → P x
elim e = elimᴾ e′
  where
  module E = Elim e

  e′ : Elimᴾ _
  e′ .∅ʳ           = E.∅ʳ
  e′ .singletonʳ   = E.singletonʳ
  e′ .∪ʳ           = E.∪ʳ
  e′ .∅∪ʳ p        = subst≡→[]≡ (E.∅∪ʳ p)
  e′ .idem-sʳ x    = subst≡→[]≡ (E.idem-sʳ x)
  e′ .assocʳ p q r = subst≡→[]≡ (E.assocʳ p q r)
  e′ .commʳ p q    = subst≡→[]≡ (E.commʳ p q)
  e′ .is-setʳ x    = _↔_.to (H-level↔H-level 2) (E.is-setʳ x)

-- A non-dependent eliminator, expressed using equality.

record Rec (A : Type a) (B : Type b) : Type (a ⊔ b) where
  field
    ∅ʳ         : B
    singletonʳ : A → B
    ∪ʳ         : Finite-subset-of A → Finite-subset-of A → B → B → B
    ∅∪ʳ        : ∀ x p → ∪ʳ ∅ x ∅ʳ p ≡ p
    idem-sʳ    : ∀ x →
                 ∪ʳ (singleton x) (singleton x)
                    (singletonʳ x) (singletonʳ x) ≡
                 singletonʳ x
    assocʳ     : ∀ p q r →
                 ∪ʳ x (y ∪ z) p (∪ʳ y z q r) ≡
                 ∪ʳ (x ∪ y) z (∪ʳ x y p q) r
    commʳ      : ∀ p q → ∪ʳ x y p q ≡ ∪ʳ y x q p
    is-setʳ    : Is-set B

open Rec public

rec : Rec A B → Finite-subset-of A → B
rec r = recᴾ r′
  where
  module R = Rec r

  r′ : Recᴾ _ _
  r′ .∅ʳ           = R.∅ʳ
  r′ .singletonʳ   = R.singletonʳ
  r′ .∪ʳ           = R.∪ʳ
  r′ .∅∪ʳ x p      = _↔_.to ≡↔≡ (R.∅∪ʳ x p)
  r′ .idem-sʳ x    = _↔_.to ≡↔≡ (R.idem-sʳ x)
  r′ .assocʳ p q r = _↔_.to ≡↔≡ (R.assocʳ p q r)
  r′ .commʳ p q    = _↔_.to ≡↔≡ (R.commʳ p q)
  r′ .is-setʳ      = _↔_.to (H-level↔H-level 2) R.is-setʳ

-- A dependent eliminator for propositions.

record Elim-prop {A : Type a} (P : Finite-subset-of A → Type p) :
                 Type (a ⊔ p) where
  field
    ∅ʳ              : P ∅
    singletonʳ      : ∀ x → P (singleton x)
    ∪ʳ              : P x → P y → P (x ∪ y)
    is-propositionʳ : ∀ x → Is-proposition (P x)

open Elim-prop public

elim-prop : Elim-prop P → (x : Finite-subset-of A) → P x
elim-prop e = elim e′
  where
  module E = Elim-prop e

  e′ : Elim _
  e′ .∅ʳ           = E.∅ʳ
  e′ .singletonʳ   = E.singletonʳ
  e′ .∪ʳ           = E.∪ʳ
  e′ .∅∪ʳ _        = E.is-propositionʳ _ _ _
  e′ .idem-sʳ _    = E.is-propositionʳ _ _ _
  e′ .assocʳ _ _ _ = E.is-propositionʳ _ _ _
  e′ .commʳ _ _    = E.is-propositionʳ _ _ _
  e′ .is-setʳ _    = mono₁ 1 (E.is-propositionʳ _)

-- A non-dependent eliminator for propositions.

record Rec-prop (A : Type a) (B : Type b) : Type (a ⊔ b) where
  field
    ∅ʳ              : B
    singletonʳ      : A → B
    ∪ʳ              : Finite-subset-of A → Finite-subset-of A →
                      B → B → B
    is-propositionʳ : Is-proposition B

open Rec-prop public

rec-prop : Rec-prop A B → Finite-subset-of A → B
rec-prop r = elim-prop e
  where
  module R = Rec-prop r

  e : Elim-prop _
  e .∅ʳ                 = R.∅ʳ
  e .singletonʳ         = R.singletonʳ
  e .∪ʳ {x = x} {y = y} = R.∪ʳ x y
  e .is-propositionʳ _  = R.is-propositionʳ

------------------------------------------------------------------------
-- Definitions related to listed finite subsets

private

  -- Some definitions used in the implementation of Listed≃Kuratowski
  -- below.

  to : L.Finite-subset-of A → Finite-subset-of A
  to L.[]      = ∅
  to (x L.∷ y) = singleton x ∪ to y

  to (L.dropᴾ {x = x} {y = y} i) =
    (singleton x ∪ (singleton x ∪ to y)  P.≡⟨ assocᴾ ⟩
     (singleton x ∪ singleton x) ∪ to y  P.≡⟨ P.cong (_∪ to y) idem-sᴾ ⟩∎
     singleton x ∪ to y                  ∎) i

  to (L.swapᴾ {x = x} {y = y} {z = z} i) =
    (singleton x ∪ (singleton y ∪ to z)  P.≡⟨ assocᴾ ⟩
     (singleton x ∪ singleton y) ∪ to z  P.≡⟨ P.cong (_∪ to z) commᴾ ⟩
     (singleton y ∪ singleton x) ∪ to z  P.≡⟨ P.sym assocᴾ ⟩∎
     singleton y ∪ (singleton x ∪ to z)  ∎) i

  to (L.is-setᴾ x y i j) =
    is-setᴾ (λ i → to (x i)) (λ i → to (y i)) i j

  to-∪ : (x : L.Finite-subset-of A) → to (x L.∪ y) ≡ to x ∪ to y
  to-∪ {y = y} = L.elim-prop e
    where
    e : L.Elim-prop _
    e .L.is-propositionʳ _ = is-set

    e .L.[]ʳ =
      to y      ≡⟨ sym ∅∪ ⟩∎
      ∅ ∪ to y  ∎

    e .L.∷ʳ {y = z} x hyp =
      singleton x ∪ to (z L.∪ y)   ≡⟨ cong (singleton x ∪_) hyp ⟩
      singleton x ∪ (to z ∪ to y)  ≡⟨ assoc ⟩∎
      (singleton x ∪ to z) ∪ to y  ∎

-- Listed finite subsets are equivalent to Kuratowski finite subsets.

Listed≃Kuratowski : L.Finite-subset-of A ≃ Finite-subset-of A
Listed≃Kuratowski {A = A} = from-bijection (record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  })
  where
  from : Finite-subset-of A → L.Finite-subset-of A
  from ∅             = L.[]
  from (singleton x) = x L.∷ L.[]
  from (x ∪ y)       = from x L.∪ from y

  from (∅∪ᴾ {x = x} _) = from x

  from (idem-sᴾ {x = x} i) = L.dropᴾ {x = x} {y = L.[]} i

  from (assocᴾ {x = x} {y = y} {z = z} i) =
    _↔_.to ≡↔≡ (L.assoc {y = from y} {z = from z} (from x)) i

  from (commᴾ {x = x} {y = y} i) =
    _↔_.to ≡↔≡ (L.comm {y = from y} (from x)) i

  from (is-setᴾ x y i j) =
    L.is-setᴾ (λ i → from (x i)) (λ i → from (y i)) i j

  to∘from : ∀ x → to (from x) ≡ x
  to∘from = elim-prop e
    where
    e : Elim-prop _
    e .is-propositionʳ _            = is-set
    e .∅ʳ                           = refl _
    e .singletonʳ _                 = ∪∅
    e .∪ʳ {x = x} {y = y} hyp₁ hyp₂ =
      to (from x L.∪ from y)     ≡⟨ to-∪ (from x) ⟩
      to (from x) ∪ to (from y)  ≡⟨ cong₂ _∪_ hyp₁ hyp₂ ⟩∎
      x ∪ y                      ∎

  from∘to : ∀ x → from (to x) ≡ x
  from∘to = L.elim-prop e
    where
    e : L.Elim-prop _
    e .L.is-propositionʳ _ = L.is-set
    e .L.[]ʳ               = refl _
    e .L.∷ʳ {y = y} x hyp  =
      x L.∷ from (to y)  ≡⟨ cong (x L.∷_) hyp ⟩∎
      x L.∷ y            ∎

-- The forward direction of Listed≃Kuratowski is homomorphic with
-- respect to L._∪_/_∪_.

to-Listed≃Kuratowski-∪ :
  (x : L.Finite-subset-of A) →
  _≃_.to Listed≃Kuratowski (x L.∪ y) ≡
  _≃_.to Listed≃Kuratowski x ∪ _≃_.to Listed≃Kuratowski y
to-Listed≃Kuratowski-∪ = to-∪

-- The other direction of Listed≃Kuratowski is definitionally
-- homomorphic with respect to _∪_/L._∪_.

_ :
  _≃_.from Listed≃Kuratowski (x ∪ y) ≡
  _≃_.from Listed≃Kuratowski x L.∪ _≃_.from Listed≃Kuratowski y
_ = refl _

-- A list-like dependent eliminator for Finite-subset-of, for
-- propositions.

record List-elim-prop
         {A : Type a} (P : Finite-subset-of A → Type p) :
         Type (a ⊔ p) where
  field
    []ʳ             : P ∅
    ∷ʳ              : ∀ x → P y → P (singleton x ∪ y)
    is-propositionʳ : ∀ x → Is-proposition (P x)

open List-elim-prop public

list-elim-prop : List-elim-prop P → (x : Finite-subset-of A) → P x
list-elim-prop {P = P} l x =
  subst P (_≃_.right-inverse-of Listed≃Kuratowski x)
    (L.elim-prop e (_≃_.from Listed≃Kuratowski x))
  where
  module E = List-elim-prop l

  e : L.Elim-prop (P ∘ _≃_.to Listed≃Kuratowski)
  e .L.[]ʳ               = E.[]ʳ
  e .L.∷ʳ x              = E.∷ʳ x
  e .L.is-propositionʳ _ = E.is-propositionʳ _

-- A list-like non-dependent eliminator for Finite-subset-of,
-- expressed using paths.

record List-recᴾ (A : Type a) (B : Type b) : Type (a ⊔ b) where
  field
    []ʳ     : B
    ∷ʳ      : A → Finite-subset-of A → B → B
    dropʳ   : ∀ x y p →
              ∷ʳ x (singleton x ∪ y) (∷ʳ x y p) P.≡ ∷ʳ x y p
    swapʳ   : ∀ x y z p →
              ∷ʳ x (singleton y ∪ z) (∷ʳ y z p) P.≡
              ∷ʳ y (singleton x ∪ z) (∷ʳ x z p)
    is-setʳ : P.Is-set B

open List-recᴾ public

list-recᴾ : List-recᴾ A B → Finite-subset-of A → B
list-recᴾ l = L.recᴾ r ∘ _≃_.from Listed≃Kuratowski
  where
  module E = List-recᴾ l

  r : L.Recᴾ _ _
  r .L.[]ʳ         = E.[]ʳ
  r .L.∷ʳ x y      = E.∷ʳ x (_≃_.to Listed≃Kuratowski y)
  r .L.dropʳ x y   = E.dropʳ x (_≃_.to Listed≃Kuratowski y)
  r .L.swapʳ x y z = E.swapʳ x y (_≃_.to Listed≃Kuratowski z)
  r .L.is-setʳ     = E.is-setʳ

-- Unit tests documenting some of the computational behaviour of
-- list-recᴾ.

_ : list-recᴾ l ∅ ≡ l .[]ʳ
_ = refl _

_ : list-recᴾ l (singleton x) ≡ l .∷ʳ x ∅ (l .[]ʳ)
_ = refl _

_ : let y′ = _≃_.to Listed≃Kuratowski (_≃_.from Listed≃Kuratowski y) in

    list-recᴾ l (singleton x ∪ y) ≡ l .∷ʳ x y′ (list-recᴾ l y)
_ = refl _

-- A list-like non-dependent eliminator for Finite-subset-of,
-- expressed using equality.

record List-rec (A : Type a) (B : Type b) : Type (a ⊔ b) where
  field
    []ʳ     : B
    ∷ʳ      : A → Finite-subset-of A → B → B
    dropʳ   : ∀ x y p →
              ∷ʳ x (singleton x ∪ y) (∷ʳ x y p) ≡ ∷ʳ x y p
    swapʳ   : ∀ x y z p →
              ∷ʳ x (singleton y ∪ z) (∷ʳ y z p) ≡
              ∷ʳ y (singleton x ∪ z) (∷ʳ x z p)
    is-setʳ : Is-set B

open List-rec public

list-rec : List-rec A B → Finite-subset-of A → B
list-rec l = list-recᴾ l′
  where
  module R = List-rec l

  l′ : List-recᴾ _ _
  l′ .[]ʳ           = R.[]ʳ
  l′ .∷ʳ            = R.∷ʳ
  l′ .dropʳ x y p   = _↔_.to ≡↔≡ (R.dropʳ x y p)
  l′ .swapʳ x y z p = _↔_.to ≡↔≡ (R.swapʳ x y z p)
  l′ .is-setʳ       = _↔_.to (H-level↔H-level 2) R.is-setʳ

-- Unit tests documenting some of the computational behaviour of
-- list-rec.

_ : list-rec l ∅ ≡ l .[]ʳ
_ = refl _

_ : list-rec l (singleton x) ≡ l .∷ʳ x ∅ (l .[]ʳ)
_ = refl _

_ : let y′ = _≃_.to Listed≃Kuratowski (_≃_.from Listed≃Kuratowski y) in

    list-rec l (singleton x ∪ y) ≡ l .∷ʳ x y′ (list-rec l y)
_ = refl _

------------------------------------------------------------------------
-- Membership

-- Membership.

infix 4 _∈_

_∈_ : {A : Type a} → A → Finite-subset-of A → Type a
x ∈ y = x L.∈ _≃_.from Listed≃Kuratowski y

-- Membership is propositional.

∈-propositional : ∀ y → Is-proposition (x ∈ y)
∈-propositional _ = L.∈-propositional

-- A lemma characterising ∅.

∈∅≃ : (x ∈ ∅) ≃ ⊥₀
∈∅≃ = L.∈[]≃

-- A lemma characterising singleton.

∈singleton≃ : (x ∈ singleton y) ≃ ∥ x ≡ y ∥
∈singleton≃ = L.∈singleton≃

-- If x is a member of y, then x is a member of y ∪ z.

∈→∈∪ˡ : ∀ y z → x ∈ y → x ∈ y ∪ z
∈→∈∪ˡ {x = x} y z =
  x ∈ y                                                                ↔⟨⟩
  x L.∈ _≃_.from Listed≃Kuratowski y                                   ↝⟨ L.∈→∈∪ˡ ⟩
  x L.∈ _≃_.from Listed≃Kuratowski y L.∪ _≃_.from Listed≃Kuratowski z  ↔⟨⟩
  x L.∈ _≃_.from Listed≃Kuratowski (y ∪ z)                             ↔⟨⟩
  x ∈ y ∪ z                                                            □

-- If x is a member of z, then x is a member of y ∪ z.

∈→∈∪ʳ : ∀ y z → x ∈ z → x ∈ y ∪ z
∈→∈∪ʳ {x = x} y z =
  x ∈ z                                                                ↔⟨⟩
  x L.∈ _≃_.from Listed≃Kuratowski z                                   ↝⟨ L.∈→∈∪ʳ (_≃_.from Listed≃Kuratowski y) ⟩
  x L.∈ _≃_.from Listed≃Kuratowski y L.∪ _≃_.from Listed≃Kuratowski z  ↔⟨⟩
  x ∈ y ∪ z                                                            □

-- Membership of a union of two subsets can be expressed in terms of
-- membership of the subsets.

∈∪≃ : ∀ y z → (x ∈ y ∪ z) ≃ (x ∈ y ∥⊎∥ x ∈ z)
∈∪≃ {x = x} y z =
  x ∈ y ∪ z                                                            ↔⟨⟩

  x L.∈ _≃_.from Listed≃Kuratowski y L.∪ _≃_.from Listed≃Kuratowski z  ↝⟨ L.∈∪≃ ⟩

  x L.∈ _≃_.from Listed≃Kuratowski y ∥⊎∥
  x L.∈ _≃_.from Listed≃Kuratowski z                                   ↔⟨⟩

  x ∈ y ∥⊎∥ x ∈ z                                                      □

-- If truncated equality is decidable, then membership is also
-- decidable.

member? :
  ((x y : A) → Dec ∥ x ≡ y ∥) →
  (x : A) (y : Finite-subset-of A) → Dec (x ∈ y)
member? equal? x = L.member? equal? x ∘ _≃_.from Listed≃Kuratowski

-- Subsets.

_⊆_ : {A : Type a} → Finite-subset-of A → Finite-subset-of A → Type a
x ⊆ y = ∀ z → z ∈ x → z ∈ y

-- The subset property can be expressed using _∪_ and _≡_.

⊆≃∪≡ : (x ⊆ y) ≃ (x ∪ y ≡ y)
⊆≃∪≡ {x = x} {y = y} =
  x ⊆ y                                                              ↝⟨ L.⊆≃∪≡ (_≃_.from Listed≃Kuratowski x) ⟩

  _≃_.from Listed≃Kuratowski x L.∪ _≃_.from Listed≃Kuratowski y ≡
  _≃_.from Listed≃Kuratowski y                                       ↔⟨⟩

  _≃_.from Listed≃Kuratowski (x ∪ y) ≡ _≃_.from Listed≃Kuratowski y  ↝⟨ Eq.≃-≡ (inverse Listed≃Kuratowski) ⟩□

  x ∪ y ≡ y                                                          □

-- Extensionality.

extensionality :
  (x ≡ y) ≃ (∀ z → z ∈ x ⇔ z ∈ y)
extensionality {x = x} {y = y} =
  x ≡ y                                                        ↝⟨ inverse $ Eq.≃-≡ (inverse Listed≃Kuratowski) ⟩
  _≃_.from Listed≃Kuratowski x ≡ _≃_.from Listed≃Kuratowski y  ↝⟨ L.extensionality ⟩□
  (∀ z → z ∈ x ⇔ z ∈ y)                                        □

------------------------------------------------------------------------
-- A law

-- Union is idempotent.

idem : x ∪ x ≡ x
idem {x = x} = _≃_.from extensionality λ y →
  y ∈ x ∪ x        ↔⟨ ∈∪≃ x x ⟩
  y ∈ x ∥⊎∥ y ∈ x  ↔⟨ Trunc.idempotent ⟩
  ∥ y ∈ x ∥        ↔⟨ Trunc.∥∥↔ (∈-propositional x) ⟩□
  y ∈ x            □

------------------------------------------------------------------------
-- Some operations

-- A map function.

map : (A → B) → Finite-subset-of A → Finite-subset-of B
map f = recᴾ r
  where
  r : Recᴾ _ _
  r .∅ʳ           = ∅
  r .singletonʳ x = singleton (f x)
  r .∪ʳ _ _       = _∪_
  r .∅∪ʳ _ _      = ∅∪ᴾ
  r .idem-sʳ _    = idem-sᴾ
  r .assocʳ _ _ _ = assocᴾ
  r .commʳ _ _    = commᴾ
  r .is-setʳ      = is-setᴾ

-- A filter function.

filter : (A → Bool) → Finite-subset-of A → Finite-subset-of A
filter p = rec r
  where
  r : Rec _ _
  r .∅ʳ           = ∅
  r .singletonʳ x = if p x then singleton x else ∅
  r .∪ʳ _ _       = _∪_
  r .∅∪ʳ _ _      = ∅∪
  r .idem-sʳ _    = idem
  r .assocʳ _ _ _ = assoc
  r .commʳ _ _    = comm
  r .is-setʳ      = is-set

-- Join.

join : Finite-subset-of (Finite-subset-of A) → Finite-subset-of A
join = rec r
  where
  r : Rec _ _
  r .∅ʳ           = ∅
  r .singletonʳ   = id
  r .∪ʳ _ _       = _∪_
  r .∅∪ʳ _ _      = ∅∪
  r .idem-sʳ _    = idem
  r .assocʳ _ _ _ = assoc
  r .commʳ _ _    = comm
  r .is-setʳ      = is-set

-- A universe-polymorphic variant of bind.

infixl 5 _>>=′_

_>>=′_ :
  Finite-subset-of A → (A → Finite-subset-of B) → Finite-subset-of B
x >>=′ f = join (map f x)

-- Bind distributes from the right over union.

_ : (x ∪ y) >>=′ f ≡ (x >>=′ f) ∪ (y >>=′ f)
_ = refl _

-- Bind distributes from the left over union.

>>=-left-distributive :
  ∀ x → (x >>=′ λ x → f x ∪ g x) ≡ (x >>=′ f) ∪ (x >>=′ g)
>>=-left-distributive {f = f} {g = g} = elim-prop e
  where
  e : Elim-prop _
  e .∅ʳ                           = ∅      ≡⟨ sym idem ⟩∎
                                    ∅ ∪ ∅  ∎
  e .singletonʳ _                 = refl _
  e .is-propositionʳ _            = is-set
  e .∪ʳ {x = x} {y = y} hyp₁ hyp₂ =
    (x ∪ y) >>=′ (λ x → f x ∪ g x)                         ≡⟨⟩
    (x >>=′ λ x → f x ∪ g x) ∪ (y >>=′ λ x → f x ∪ g x)    ≡⟨ cong₂ _∪_ hyp₁ hyp₂ ⟩
    ((x >>=′ f) ∪ (x >>=′ g)) ∪ ((y >>=′ f) ∪ (y >>=′ g))  ≡⟨ sym assoc ⟩
    (x >>=′ f) ∪ ((x >>=′ g) ∪ ((y >>=′ f) ∪ (y >>=′ g)))  ≡⟨ cong ((x >>=′ f) ∪_) assoc ⟩
    (x >>=′ f) ∪ (((x >>=′ g) ∪ (y >>=′ f)) ∪ (y >>=′ g))  ≡⟨ cong (((x >>=′ f) ∪_) ∘ (_∪ (y >>=′ g))) comm ⟩
    (x >>=′ f) ∪ (((y >>=′ f) ∪ (x >>=′ g)) ∪ (y >>=′ g))  ≡⟨ cong ((x >>=′ f) ∪_) (sym assoc) ⟩
    (x >>=′ f) ∪ ((y >>=′ f) ∪ ((x >>=′ g) ∪ (y >>=′ g)))  ≡⟨ assoc ⟩
    ((x >>=′ f) ∪ (y >>=′ f)) ∪ ((x >>=′ g) ∪ (y >>=′ g))  ≡⟨⟩
    ((x ∪ y) >>=′ f) ∪ ((x ∪ y) >>=′ g)                    ∎

-- Monad laws.

_ : singleton x >>=′ f ≡ f x
_ = refl _

>>=-singleton : x >>=′ singleton ≡ x
>>=-singleton = elim-prop e _
  where
  e : Elim-prop (λ x → x >>=′ singleton ≡ x)
  e .∅ʳ                           = refl _
  e .singletonʳ _                 = refl _
  e .is-propositionʳ _            = is-set
  e .∪ʳ {x = x} {y = y} hyp₁ hyp₂ =
    (x ∪ y) >>=′ singleton                   ≡⟨⟩
    (x >>=′ singleton) ∪ (y >>=′ singleton)  ≡⟨ cong₂ _∪_ hyp₁ hyp₂ ⟩∎
    x ∪ y                                    ∎

>>=-assoc : ∀ x → x >>=′ (λ x → f x >>=′ g) ≡ x >>=′ f >>=′ g
>>=-assoc {f = f} {g = g} = elim-prop e
  where
  e : Elim-prop _
  e .∅ʳ                           = refl _
  e .singletonʳ _                 = refl _
  e .is-propositionʳ _            = is-set
  e .∪ʳ {x = x} {y = y} hyp₁ hyp₂ =
    (x ∪ y) >>=′ (λ x → f x >>=′ g)                        ≡⟨⟩
    (x >>=′ λ x → f x >>=′ g) ∪ (y >>=′ λ x → f x >>=′ g)  ≡⟨ cong₂ _∪_ hyp₁ hyp₂ ⟩
    (x >>=′ f >>=′ g) ∪ (y >>=′ f >>=′ g)                  ≡⟨⟩
    (x ∪ y) >>=′ f >>=′ g                                  ∎

-- A monad instance.

instance

  raw-monad : Raw-monad {d = a} Finite-subset-of
  raw-monad .M.return = singleton
  raw-monad .M._>>=_  = _>>=′_

  monad : Monad {d = a} Finite-subset-of
  monad .M.Monad.raw-monad           = raw-monad
  monad .M.Monad.left-identity _ _   = refl _
  monad .M.Monad.right-identity _    = >>=-singleton
  monad .M.Monad.associativity x _ _ = >>=-assoc x

------------------------------------------------------------------------
-- Size

-- Size.

infix 4 ∣_∣≡_

∣_∣≡_ : {A : Type a} → Finite-subset-of A → ℕ → Type a
∣ x ∣≡ n = L.∣ _≃_.from Listed≃Kuratowski x ∣≡ n

-- The size predicate is propositional.

∣∣≡-propositional :
  (x : Finite-subset-of A) → Is-proposition (∣ x ∣≡ n)
∣∣≡-propositional = L.∣∣≡-propositional ∘ _≃_.from Listed≃Kuratowski

-- Unit tests documenting some of the computational behaviour of
-- ∣_∣≡_.

_ : (∣ ∅ {A = A} ∣≡ n) ≡ ↑ _ (n ≡ 0)
_ = refl _

_ : ∀ {A : Type a} {x : A} {y} →
    (∣ singleton x ∪ y ∣≡ zero) ≡ (x ∈ y × ∣ y ∣≡ zero ⊎ ⊥)
_ = refl _

_ : (∣ singleton x ∪ y ∣≡ suc n) ≡
    (x ∈ y × ∣ y ∣≡ suc n ⊎ ¬ x ∈ y × ∣ y ∣≡ n)
_ = refl _

-- The size predicate is functional.

∣∣≡-functional :
  (x : Finite-subset-of A) → ∣ x ∣≡ m → ∣ x ∣≡ n → m ≡ n
∣∣≡-functional = L.∣∣≡-functional ∘ _≃_.from Listed≃Kuratowski

-- If truncated equality is decidable, then one can compute the size
-- of a finite subset.

size :
  ((x y : A) → Dec ∥ x ≡ y ∥) →
  (x : Finite-subset-of A) → ∃ λ n → ∣ x ∣≡ n
size equal? = L.size equal? ∘ _≃_.from Listed≃Kuratowski

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
data ⊤ : Set where
  tt : ⊤

data Identity (t : Set) : Set where
  MkIdentity : t → Identity t

let-example : Identity ⊤
let-example =
  let x = tt
      in MkIdentity x   -- Parse error

do-example : Identity ⊤
do-example = do
  MkIdentity tt
  where
    x : ⊤
    x = tt

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Data.PolyP where

open import Data.PolyP.RecursionSchemes public
open import Data.PolyP.Universe public
open import Data.PolyP.Composition public
open import Data.PolyP.Types public
open import Data.PolyP.Currying public

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

open import Categories.Category
open import Categories.Category.Monoidal

module Categories.Category.Monoidal.Symmetric {o ℓ e} {C : Category o ℓ e} (M : Monoidal C) where

open import Level

open import Data.Product using (Σ; _,_)

open import Categories.Functor.Bifunctor
open import Categories.NaturalTransformation.NaturalIsomorphism

open import Categories.Morphism C
open import Categories.Category.Monoidal.Braided M
open Category C
open Commutation

private
  variable
    X Y Z : Obj

-- symmetric monoidal category
-- commutative braided monoidal category
record Symmetric : Set (levelOfTerm M) where
  field
    braided : Braided

  module braided = Braided braided
  open braided public

  private
    B : ∀ {X Y} → X ⊗₀ Y ⇒ Y ⊗₀ X
    B {X} {Y} = braiding.⇒.η (X , Y)

  field
    commutative : B {X} {Y} ∘ B {Y} {X} ≈ id

  braided-iso : X ⊗₀ Y ≅ Y ⊗₀ X
  braided-iso = record
    { from = B
    ; to   = B
    ; iso  = record
      { isoˡ = commutative
      ; isoʳ = commutative
      }
    }


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The type for booleans and some operations
------------------------------------------------------------------------

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

module Data.Bool.Base where

open import Data.Unit.Base using (⊤)
open import Data.Empty
open import Level using (Level)

private
  variable
    a : Level
    A : Set a

------------------------------------------------------------------------
-- The boolean type

open import Agda.Builtin.Bool public

------------------------------------------------------------------------
-- Relations

infix 4 _≤_ _<_

data _≤_ : Bool → Bool → Set where
  f≤t : false ≤ true
  b≤b : ∀ {b} → b ≤ b

data _<_ : Bool → Bool → Set where
  f<t : false < true

------------------------------------------------------------------------
-- Boolean operations

infixr 6 _∧_
infixr 5 _∨_ _xor_

not : Bool → Bool
not true  = false
not false = true

_∧_ : Bool → Bool → Bool
true  ∧ b = b
false ∧ b = false

_∨_ : Bool → Bool → Bool
true  ∨ b = true
false ∨ b = b

_xor_ : Bool → Bool → Bool
true  xor b = not b
false xor b = b

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

infix  0 if_then_else_

if_then_else_ : Bool → A → A → A
if true  then t else f = t
if false then t else f = f

-- A function mapping true to an inhabited type and false to an empty
-- type.

T : Bool → Set
T true  = ⊤
T false = ⊥


text:
-- {-# OPTIONS --verbose tc.conv.term:40 #-}
-- {-# OPTIONS --verbose tc.conv.level:40 #-}
-- {-# OPTIONS --verbose tc.conv.atom:50 #-}
-- {-# OPTIONS --verbose tc.conv.elim:50 #-}

module Issue680-NeutralLevels where

open import Common.Level

postulate N : Set
          A : N → Set
          B : Set
          level' : B → Level
          lac : ∀ {n} → A n → B
          I : Level → Level → Set
          refl : ∀ {l : Level} → I l l
          Top : Set
          top : Top

data Test : Set where
  mkTest : (n : N) → (tel : A n) → Test

test : Test → Top
test (mkTest n tel) = top
  where
    test′ : I (lsuc (level' (lac tel))) (lsuc (level' (lac tel)))
    test′ = refl

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Stack where

open import Prelude public

-- Stacks, or snoc-lists.

data Stack (X : Set) : Set where
  ∅   : Stack X
  _,_ : Stack X → X → Stack X

-- Stack membership, or de Bruijn indices.

module _ {X : Set} where
  infix 3 _∈_
  data _∈_ (A : X) : Stack X → Set where
    top : ∀ {Γ}   → A ∈ Γ , A
    pop : ∀ {Γ B} → A ∈ Γ → A ∈ Γ , B

  ⌊_⌋∈ : ∀ {Γ A} → A ∈ Γ → Nat
  ⌊ top ⌋∈   = zero
  ⌊ pop i ⌋∈ = suc ⌊ i ⌋∈

  i₀ : ∀ {Γ A} → A ∈ Γ , A
  i₀ = top

  i₁ : ∀ {Γ A B} → A ∈ Γ , A , B
  i₁ = pop i₀

  i₂ : ∀ {Γ A B C} → A ∈ Γ , A , B , C
  i₂ = pop i₁

-- Stack inclusion, or order-preserving embeddings.

module _ {X : Set} where
  infix 3 _⊆_
  data _⊆_ : Stack X → Stack X → Set where
    bot  : ∀ {Γ}      → ∅ ⊆ Γ
    skip : ∀ {Γ Γ′ A} → Γ ⊆ Γ′ → Γ ⊆ Γ′ , A
    keep : ∀ {Γ Γ′ A} → Γ ⊆ Γ′ → Γ , A ⊆ Γ′ , A

  refl⊆ : ∀ {Γ} → Γ ⊆ Γ
  refl⊆ {∅}     = bot
  refl⊆ {Γ , A} = keep refl⊆

  trans⊆ : ∀ {Γ Γ′ Γ″} → Γ ⊆ Γ′ → Γ′ ⊆ Γ″ → Γ ⊆ Γ″
  trans⊆ bot      η′        = bot
  trans⊆ η        (skip η′) = skip (trans⊆ η η′)
  trans⊆ (skip η) (keep η′) = skip (trans⊆ η η′)
  trans⊆ (keep η) (keep η′) = keep (trans⊆ η η′)

  weak⊆ : ∀ {Γ A} → Γ ⊆ Γ , A
  weak⊆ = skip refl⊆

-- Monotonicity of stack membership with respect to stack inclusion.

module _ {X : Set} where
  mono∈ : ∀ {Γ Γ′ : Stack X} {A} → Γ ⊆ Γ′ → A ∈ Γ → A ∈ Γ′
  mono∈ bot      ()
  mono∈ (skip η) i       = pop (mono∈ η i)
  mono∈ (keep η) top     = top
  mono∈ (keep η) (pop i) = pop (mono∈ η i)

-- Pairs of stacks.

infixl 4 _⁏_
record Stack² (X Y : Set) : Set where
  constructor _⁏_
  field
    π₁ : Stack X
    π₂ : Stack Y

open Stack² public

-- Stack pair inclusion.

module _ {X Y : Set} where
  infix 3 _⊆²_
  _⊆²_ : Stack² X Y → Stack² X Y → Set
  Γ ⁏ Δ ⊆² Γ′ ⁏ Δ′ = Γ ⊆ Γ′ ∧ Δ ⊆ Δ′

  refl⊆² : ∀ {Γ Δ} → Γ ⁏ Δ ⊆² Γ ⁏ Δ
  refl⊆² = refl⊆ , refl⊆

  trans⊆² : ∀ {Γ Γ′ Γ″ Δ Δ′ Δ″} → Γ ⁏ Δ ⊆² Γ′ ⁏ Δ′ → Γ′ ⁏ Δ′ ⊆² Γ″ ⁏ Δ″ → Γ ⁏ Δ ⊆² Γ″ ⁏ Δ″
  trans⊆² (η , ρ) (η′ , ρ′) = trans⊆ η η′ , trans⊆ ρ ρ′


text:
{-# OPTIONS --safe --without-K #-}
module JVM.Prelude where

open import Level public hiding (zero) renaming (suc to sucℓ)
open import Function public using (case_of_; _∘_; id; const)

open import Data.List using (List; _∷_; []; [_]) public
open import Data.Unit using (⊤; tt) public
open import Data.Nat using (ℕ; suc; zero; _+_) public
open import Data.Sum using (inj₁; inj₂) renaming (_⊎_ to _⊕_)public
open import Data.Product public hiding (map; zip)

open import Relation.Unary hiding (_∈_; Empty) public
open import Relation.Binary.PropositionalEquality hiding ([_]) public

open import Relation.Ternary.Core public
open import Relation.Ternary.Structures public


text:
module Coverage where

infixr 40 _::_
data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A

data D : Set where
  c1 : D -> D
  c2 : D
  c3 : D -> D -> D -> D
  c4 : D -> D -> D

f : D -> D -> D -> D -> List D
f (c3 a (c1 b) (c1 c2)) (c1 (c1 c)) d (c1 (c1 (c1 e))) = a :: b :: c :: d :: e :: []
f (c3 (c4 c2 a) (c1 b) (c1 c)) d (c1 (c1 e)) (c1 (c1 (c1 f))) = a :: b :: c :: d :: e :: f :: []
f a b (c1 c) (c3 d (c1 e) (c1 f)) = a :: b :: c :: d :: e :: f :: []
f (c3 (c4 a c2) b (c1 c)) (c1 d) (c1 (c1 (c1 e))) (c1 (c1 (c1 f))) = a :: b :: c :: d :: e :: f :: []
-- f (c3 a (c1 b) c) (c1 (c1 (c1 d))) (c1 (c1 (c1 e))) f = a :: b :: c :: d :: e :: f :: []
-- f a b (c1 (c1 c)) (c1 (c1 (c1 c2))) = a :: b :: c :: []
f a b c d = a :: b :: c :: d :: []


text:
open import Data.Product using ( proj₁ ; proj₂ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; sym ; cong )
open import Relation.Unary using ( _⊆_ )
open import Web.Semantic.DL.ABox using ( ABox ; ⟨ABox⟩ ; Assertions )
open import Web.Semantic.DL.ABox.Interp using ( ⌊_⌋ ; ind )
open import Web.Semantic.DL.ABox.Model using ( _⊨a_ ; bnodes ; _,_ )
open import Web.Semantic.DL.Category.Object using ( Object ; IN ; fin ; iface )
open import Web.Semantic.DL.Category.Morphism using ( impl ; _≣_ ; _⊑_ ; _,_ )
open import Web.Semantic.DL.Category.Composition using ( _∙_ )
open import Web.Semantic.DL.Category.Properties.Composition.Lemmas using
  ( compose-left ; compose-right ; compose-resp-⊨a )
open import Web.Semantic.DL.Category.Wiring using
  ( wiring ; wires-≈ ; wires-≈⁻¹ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox )
open import Web.Semantic.DL.TBox.Interp using
  ( Δ ; _⊨_≈_ ; ≈-refl ; ≈-refl′ ; ≈-trans )
open import Web.Semantic.Util using
  ( _∘_ ; False ; elim ; _⊕_⊕_ ; inode ; bnode ; enode )

module Web.Semantic.DL.Category.Properties.Composition.RespectsWiring
  {Σ : Signature} {S T : TBox Σ} where

compose-resp-wiring : ∀ (A B C : Object S T) →
  (f : IN B → IN A) →
  (f✓ : Assertions (⟨ABox⟩ f (iface B)) ⊆ Assertions (iface A)) →
  (g : IN C → IN B) →
  (g✓ : Assertions (⟨ABox⟩ g (iface C)) ⊆ Assertions (iface B)) →
  (h : IN C → IN A) →
  (h✓ : Assertions (⟨ABox⟩ h (iface C)) ⊆ Assertions (iface A)) →
    (∀ x → f (g x) ≡ h x) →
      (wiring A B f f✓ ∙ wiring B C g g✓ ≣ wiring A C h h✓)
compose-resp-wiring A B C f f✓ g g✓ h h✓ fg≡h =
  (LHS⊑RHS , RHS⊑LHS) where

  LHS⊑RHS : wiring A B f f✓ ∙ wiring B C g g✓ ⊑ wiring A C h h✓
  LHS⊑RHS I I⊨STA I⊨F = (elim , I⊨RHS) where

    lemma : ∀ x → ⌊ I ⌋ ⊨ ind I (inode (h x)) ≈ ind I (enode x)
    lemma x = ≈-trans ⌊ I ⌋
      (≈-refl′ ⌊ I ⌋ (cong (ind I ∘ inode) (sym (fg≡h x))))
      (≈-trans ⌊ I ⌋
        (wires-≈ f (proj₂ (fin B) (g x))
          (compose-left (wiring A B f f✓) (wiring B C g g✓) I I⊨F))
        (wires-≈ g (proj₂ (fin C) x)
          (compose-right (wiring A B f f✓) (wiring B C g g✓) I I⊨F)))

    I⊨RHS : bnodes I elim ⊨a impl (wiring A C h h✓)
    I⊨RHS = wires-≈⁻¹ h lemma (proj₁ (fin C))

  RHS⊑LHS : wiring A C h h✓ ⊑ wiring A B f f✓ ∙ wiring B C g g✓
  RHS⊑LHS I I⊨STA I⊨F = (i , I⊨LHS) where

    i : (False ⊕ IN B ⊕ False) → Δ ⌊ I ⌋
    i (inode ())
    i (bnode y) = ind I (inode (f y))
    i (enode ())

    lemma : ∀ x → ⌊ I ⌋ ⊨ ind I (inode (f (g x))) ≈ ind I (enode x)
    lemma x = ≈-trans ⌊ I ⌋
      (≈-refl′ ⌊ I ⌋ (cong (ind I ∘ inode) (fg≡h x)))
      (wires-≈ h (proj₂ (fin C) x) I⊨F)

    I⊨LHS : bnodes I i ⊨a impl (wiring A B f f✓ ∙ wiring B C g g✓)
    I⊨LHS = compose-resp-⊨a (wiring A B f f✓) (wiring B C g g✓) (bnodes I i)
      (wires-≈⁻¹ f (λ x → ≈-refl ⌊ I ⌋) (proj₁ (fin B)))
      (wires-≈⁻¹ g lemma (proj₁ (fin C)))

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
----------------------------------------------------------------------
-- Copyright: 2013, Jan Stolarek, Lodz University of Technology     --
--                                                                  --
-- License: See LICENSE file in root of the repo                    --
-- Repo address: https://github.com/jstolarek/dep-typed-wbl-heaps   --
--                                                                  --
-- Basic implementation of weight-biased leftist heap. No proofs    --
-- and no dependent types. Uses a single-pass merging algorithm.    --
--                                                                  --
-- Now we will modify our implementation by turning a two-pass      --
-- merging algorithm into a single-pass one. We will do this by     --
-- inlining makeT into merge. See [Single-pass merging algorithm]   --
-- for a detailed description of new algorithm. Since merge         --
-- function will be the only thing that changes we will not repeat  --
-- singleton, findMin and deleteMin functions - they are exactly    --
-- same as they were in case of two-pass merging algorithm. All     --
-- data declaration also remain the same. We will focus our         --
-- attention only on merging.                                       --
----------------------------------------------------------------------

{-# OPTIONS --sized-types #-}
module SinglePassMerge.NoProofs where

open import Basics.Nat
open import Basics hiding (_≥_)
open import Sized

data Heap : {i : Size} → Set where
  empty : {i : Size} → Heap {↑ i}
  node  : {i : Size} → Priority → Rank → Heap {i} → Heap {i} → Heap {↑ i}

-- Note [Single-pass merging algorithm]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- New single-pass merging algorithm is a straightfowrward derivation
-- from two-pass merge. We obtain this new algorithm by inlining calls
-- to makeT. This means that merge creates a new node instead of
-- delegating this task to makeT. The consequence of this is that
-- merge has two more cases now (a total of six). Base cases remain
-- unchanged (we use the same notation as in [Two-pass merging
-- algorithm]:
--
--    a) h1 is empty - return h2
--
--    b) h2 is empty - return h1
--
-- There are two more cases in the inductive part of merge definition:
--
--    c) priority p1 is higher than p2 AND rank of l1 is not smaller
--       than rank of r1 + h2 - p1 becomes the root, l1 becomes the
--       left child and result of merging r1 with h2 becomes the right
--       child child.
--
--               p1
--              /  \
--             /    \
--            l1  r1+h2
--
--    d) priority p1 is higher than p2 AND rank of r1 + h2 is not
--       smaller than rank of l1 - p1 becomes the root, result of
--       merging r1 with h2 becomes the left child and l1 becomes the
--       right child child.
--
--               p1
--              /  \
--             /    \
--           r1+h2  l1
--
--    e) priority p2 is higher than p1 AND rank of l2 is not smaller
--       rank of r2 + h1 - p2 becomes the root, l2 becomes the left
--       child and result of merging r2 with h1 becomes the right
--       child child.
--
--               p2
--              /  \
--             /    \
--            l2  r2+h1
--
--    f) priority p2 is higher than p1 AND rank of r2 + h1 is not
--       smaller than rank of l2 - p2 becomes the root, result of
--       merging r2 with h1 becomes the left child and l2 becomes the
--       right child child.
--
--               p2
--              /  \
--             /    \
--           r2+h1  l2

-- We still use a helper function to get rank of a node
rank : Heap → Nat
rank empty          = zero
rank (node _ r _ _) = r

-- Note [Compacting merge]
-- ~~~~~~~~~~~~~~~~~~~~~~~
--
-- To make implementation of merge slighty shorter we check which
-- priority is higher and at the same time we compute relation between
-- ranks of new possible subtrees (l1, r1 + h2 and l2, r2 + h1).
-- Depending on result of comparing p1 with p2 we will only need to
-- know one of this relations:
--
--   1) if priority p1 is higher than p2 then we need to know whether
--      l1 ≥ r1 + h2
--
--   2) if priority p2 is higher than p1 then we need to know whether
--      l2 ≥ r2 + h1
--
-- Computing these relations at once allows us to reduce code
-- verbosity at the price of doing some extra computations. In a
-- practical application we would most likely prefer performance over
-- code readibility, but I believe that for demonstration purposes it
-- is better to have shorter code.

merge : {i j : Size} → Heap {i} → Heap {j} → Heap
merge empty h2 = h2 -- See [Single-pass merging algorithm]
merge h1 empty = h1
merge (node p1 w1 l1 r1) (node p2 w2 l2 r2)
  with p1 < p2 -- See [Compacting merge]
  | rank l1 ≥ rank r1 + w2
  | rank l2 ≥ rank r2 + w1
merge (node p1 w1 l1 r1) (node p2 w2 l2 r2)
  | true | true | _   = node p1 (w1 + w2) l1 (merge r1 (node p2 w2 l2 r2))
merge (node p1 w1 l1 r1) (node p2 w2 l2 r2)
  | true | false | _  = node p1 (w1 + w2) (merge r1 (node p2 w2 l2 r2)) l1
merge (node p1 w1 l1 r1) (node p2 w2 l2 r2)
  | false | _ | true  = node p2 (w1 + w2) l2 (merge r2 (node p1 w1 l1 r1))
merge (node p1 w1 l1 r1) (node p2 w2 l2 r2)
  | false | _ | false = node p2 (w1 + w2) (merge r2 (node p1 w1 l1 r1)) l2

max_stars_repo_name: jstolarek/dep-typed-wbl-heaps

max_issues_repo_name: jstolarek/dep-typed-wbl-heaps

max_forks_repo_name: jstolarek/dep-typed-wbl-heaps


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

module Definition.Typed.Consequences.NeTypeEq where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Injectivity
open import Definition.Typed.Consequences.Substitution

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Helper function for the same variable instance of a context have equal types.
varTypeEq′ : ∀ {n R T Γ} → n ∷ R ∈ Γ → n ∷ T ∈ Γ → R PE.≡ T
varTypeEq′ here here = PE.refl
varTypeEq′ (there n∷R) (there n∷T) rewrite varTypeEq′ n∷R n∷T = PE.refl

-- The same variable instance of a context have equal types.
varTypeEq : ∀ {x A B Γ} → Γ ⊢ A → Γ ⊢ B → x ∷ A ∈ Γ → x ∷ B ∈ Γ → Γ ⊢ A ≡ B
varTypeEq A B x∷A x∷B rewrite varTypeEq′ x∷A x∷B = refl A

-- The same neutral term have equal types.
neTypeEq : ∀ {t A B Γ} → Neutral t → Γ ⊢ t ∷ A → Γ ⊢ t ∷ B → Γ ⊢ A ≡ B
neTypeEq (var x) (var x₁ x₂) (var x₃ x₄) =
  varTypeEq (syntacticTerm (var x₃ x₂)) (syntacticTerm (var x₃ x₄)) x₂ x₄
neTypeEq (∘ₙ neT) (t∷A ∘ⱼ t∷A₁) (t∷B ∘ⱼ t∷B₁) with neTypeEq neT t∷A t∷B
... | q = let w = proj₂ (injectivity q)
          in  substTypeEq w (refl t∷A₁)
neTypeEq (natrecₙ neT) (natrecⱼ x t∷A t∷A₁ t∷A₂) (natrecⱼ x₁ t∷B t∷B₁ t∷B₂) =
  refl (substType x₁ t∷B₂)
neTypeEq x (conv t∷A x₁) t∷B = let q = neTypeEq x t∷A t∷B
                               in  trans (sym x₁) q
neTypeEq x t∷A (conv t∷B x₃) = let q = neTypeEq x t∷A t∷B
                               in  trans q x₃

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


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

open import HoTT
open import homotopy.Bouquet
open import homotopy.DisjointlyPointedSet
open import cohomology.Theory

module cohomology.DisjointlyPointedSet {i} (OT : OrdinaryTheory i) where

  open OrdinaryTheory OT
  open import cohomology.Bouquet OT

  module _ (X : Ptd i)
    (X-is-set : is-set (de⊙ X)) (X-sep : is-separable X)
    (ac : has-choice 0 (de⊙ X) i) where

    C-set : C 0 X ≃ᴳ Πᴳ (MinusPoint X) (λ _ → C2 0)
    C-set = C-Bouquet-diag 0 (MinusPoint X) (MinusPoint-has-choice X-sep ac)
        ∘eᴳ C-emap 0 (Bouquet-⊙equiv-X X-sep)

  module _ {n : ℤ} (n≠0 : n ≠ 0) (X : Ptd i)
    (X-is-set : is-set (de⊙ X)) (X-sep : is-separable X)
    (ac : has-choice 0 (de⊙ X) i) where

    abstract
      C-set-≠-is-trivial : is-trivialᴳ (C n X)
      C-set-≠-is-trivial = iso-preserves'-trivial
        (C-emap n (Bouquet-⊙equiv-X X-sep))
        (C-Bouquet-≠-is-trivial n (MinusPoint X) 0 n≠0 (MinusPoint-has-choice X-sep ac))


text:
module tests.Forcing3 where

open import Prelude.Nat
-- {-
open import Prelude.IO
open import Prelude.Product
open import Prelude.Unit
-- -}

data _**_ (A B : Set) : Set where
  _,_ : A -> B -> A ** B

data P {A B : Set} : A ** B -> Set where
  _,_ : (x : A)(y : B) -> P (x , y)

data Q {A : Set} : A ** A -> Set where
  [_] : (x : A) -> Q (x , x)

test : let t : Set
           t = (Nat ** Nat) ** Nat
         in (q : t ** t) -> Q q -> Nat
test ._   [ ( Z , Z )   , Z ]  = Z
test ._   [ ( Z , S l)  , m  ]  = S l + m
test ._   [ ( S Z , Z)  , m  ]  = S m
test ._   [ ( S Z , S l) , m ]  = S Z + m + l
test ._   [ ( S (S n) , l) , m ]  = S (S n) + m + l
test ._   [ ( n , l )  , m ]    = m

-- {-
main : IO Unit
main = let tTyp : Set
           tTyp = (Nat ** Nat) ** Nat
           t0 : tTyp
           t0 = (0 , 0) , 0
           t1 : tTyp
           t1 = ( 0 , 1 ) , 2
           t2 : tTyp
           t2  = ( 1 , 0 ) , 3
           t3 : tTyp
           t3 = ( 1 , 4 ) , 5
           t4 : tTyp
           t4 = ( 3 , 2 ) , 10
           t5 : tTyp
           t5 = ( 0 , 0 ) , 4
           pn : tTyp -> IO Unit
           pn t = printNat (test (t , t) [ t ])
        in pn t0 ,, -- 0
           pn t1 ,, -- 3
           pn t2 ,, -- 4
           pn t3 ,, -- 9
           pn t4 ,, -- 15
           pn t5 ,, -- 4
           return unit
-- -}

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
module Structure.Relator where

import Lvl
open import Functional using (_∘₂_)
open import Functional.Dependent
open import Lang.Instance
open import Logic
open import Logic.Propositional
open import Structure.Setoid
open import Structure.Relator.Names
open import Structure.Relator.Properties
open import Syntax.Function
open import Type

-- TODO: It seems possible to define UnaryRelator as a special case of Function, so let's do that

private variable ℓₒ ℓₒ₁ ℓₒ₂ ℓₒ₃ ℓₗ ℓₗ₁ ℓₗ₂ ℓₗ₃ ℓₗ₄ : Lvl.Level

module Names where
  module _ {A : Type{ℓₒ}} ⦃ _ : Equiv{ℓₗ₁}(A) ⦄ (P : A → Stmt{ℓₗ₂}) where
    Substitution₁ = ∀{x y : A} → (x ≡ y) → P(x) → P(y)

  module _ {A : Type{ℓₒ₁}} ⦃ _ : Equiv{ℓₗ₁}(A) ⦄ {B : Type{ℓₒ₂}} ⦃ _ : Equiv{ℓₗ₂}(B) ⦄ (_▫_ : A → B → Stmt{ℓₗ₃}) where
    Substitution₂ = ∀{x₁ y₁ : A}{x₂ y₂ : B} → (x₁ ≡ y₁) → (x₂ ≡ y₂) → (x₁ ▫ x₂) → (y₁ ▫ y₂)

  module _ {A : Type{ℓₒ₁}} ⦃ _ : Equiv{ℓₗ₁}(A) ⦄ {B : Type{ℓₒ₂}} ⦃ _ : Equiv{ℓₗ₂}(B) ⦄ {C : Type{ℓₒ₃}} ⦃ _ : Equiv{ℓₗ₃}(C) ⦄ (_▫_▫_ : A → B → C → Stmt{ℓₗ₄}) where
    Substitution₃ = ∀{x₁ y₁ : A}{x₂ y₂ : B}{x₃ y₃ : C} → (x₁ ≡ y₁) → (x₂ ≡ y₂) → (x₃ ≡ y₃) → (x₁ ▫ x₂ ▫ x₃) → (y₁ ▫ y₂ ▫ y₃)

-- The unary relator `P` "(behaves like)/is a relator" in the context of `_≡_` from the Equiv instance.
module _ {A : Type{ℓₒ}} ⦃ _ : Equiv{ℓₗ₁}(A) ⦄ (P : A → Stmt{ℓₗ₂}) where
  record UnaryRelator : Stmt{ℓₒ Lvl.⊔ ℓₗ₁ Lvl.⊔ ℓₗ₂} where
    constructor intro
    field
      substitution : Names.Substitution₁(P)
    substitution-sym : ∀{x y : A} → (x ≡ y) → P(x) ← P(y)
    substitution-sym = substitution ∘ Structure.Relator.Properties.symmetry(_≡_)
    substitution-equivalence : ∀{x y : A} → (x ≡ y) → (P(x) ↔ P(y))
    substitution-equivalence xy = [↔]-intro (substitution-sym xy) (substitution xy)
  substitute₁ₗ = inst-fn UnaryRelator.substitution-sym
  substitute₁ᵣ = inst-fn UnaryRelator.substitution
  substitute₁ₗᵣ = inst-fn UnaryRelator.substitution-equivalence
  substitute₁ = substitute₁ᵣ
  unaryRelator = resolve UnaryRelator

-- The binary relator `_▫_` "(behaves like)/is a relator" in the context of `_≡_` from the Equiv instance.
module _ {A : Type{ℓₒ₁}} ⦃ _ : Equiv{ℓₗ₁}(A) ⦄ {B : Type{ℓₒ₂}} ⦃ _ : Equiv{ℓₗ₂}(B) ⦄ (_▫_ : A → B → Stmt{ℓₗ₃}) where
  open Structure.Relator.Properties

  record BinaryRelator : Stmt{ℓₒ₁ Lvl.⊔ ℓₒ₂ Lvl.⊔ ℓₗ₁ Lvl.⊔ ℓₗ₂ Lvl.⊔ ℓₗ₃} where
    constructor intro
    field
      substitution : Names.Substitution₂(_▫_)
    left : ∀{x} → UnaryRelator(_▫ x)
    left = intro(\p → substitution p (reflexivity(_≡_)))
    right : ∀{x} → UnaryRelator(x ▫_)
    right = intro(\p → substitution (reflexivity(_≡_)) p)
    substitutionₗ = \{a x y} → UnaryRelator.substitution(left {a}) {x}{y}
    substitutionᵣ = \{a x y} → UnaryRelator.substitution(right{a}) {x}{y}
    substitution-sym : ∀{x₁ y₁ : A}{x₂ y₂ : B} → (x₁ ≡ y₁) → (x₂ ≡ y₂) → ((x₁ ▫ x₂) ← (y₁ ▫ y₂))
    substitution-sym xy1 xy2 = substitution (Structure.Relator.Properties.symmetry(_≡_) xy1) (Structure.Relator.Properties.symmetry(_≡_) xy2)
    substitution-equivalence : ∀{x₁ y₁ : A}{x₂ y₂ : B} → (x₁ ≡ y₁) → (x₂ ≡ y₂) → ((x₁ ▫ x₂) ↔ (y₁ ▫ y₂))
    substitution-equivalence xy1 xy2 = [↔]-intro (substitution-sym xy1 xy2) (substitution xy1 xy2)
  substitute₂ = inst-fn BinaryRelator.substitution
  substitute₂ₗ = inst-fn BinaryRelator.substitutionₗ
  substitute₂ᵣ = inst-fn BinaryRelator.substitutionᵣ
  substitute₂ₗᵣ = inst-fn BinaryRelator.substitution-equivalence
  binaryRelator = resolve BinaryRelator

module _ {A : Type{ℓₒ₁}} ⦃ _ : Equiv{ℓₗ₁}(A) ⦄ {B : Type{ℓₒ₂}} ⦃ _ : Equiv{ℓₗ₂}(B) ⦄ {C : Type{ℓₒ₃}} ⦃ _ : Equiv{ℓₗ₃}(C) ⦄ (_▫_▫_ : A → B → C → Stmt{ℓₗ₄}) where
  open Structure.Relator.Properties

  record TrinaryRelator : Stmt{ℓₒ₁ Lvl.⊔ ℓₒ₂ Lvl.⊔ ℓₒ₃ Lvl.⊔ ℓₗ₁ Lvl.⊔ ℓₗ₂ Lvl.⊔ ℓₗ₃ Lvl.⊔ ℓₗ₄} where
    constructor intro
    field
      substitution : Names.Substitution₃(_▫_▫_)
    unary₁ : ∀{y z} → UnaryRelator(_▫ y ▫ z)
    unary₁ = intro(\p → substitution p (reflexivity(_≡_)) (reflexivity(_≡_)))
    unary₂ : ∀{x z} → UnaryRelator(x ▫_▫ z)
    unary₂ = intro(\p → substitution (reflexivity(_≡_)) p (reflexivity(_≡_)))
    unary₃ : ∀{x y} → UnaryRelator(x ▫ y ▫_)
    unary₃ = intro(\p → substitution (reflexivity(_≡_)) (reflexivity(_≡_)) p)
    binary₁₂ : ∀{z} → BinaryRelator(_▫_▫ z)
    binary₁₂ = intro(\p q → substitution p q (reflexivity(_≡_)))
    binary₁₃ : ∀{y} → BinaryRelator(_▫ y ▫_)
    binary₁₃ = intro(\p q → substitution p (reflexivity(_≡_)) q)
    binary₂₃ : ∀{x} → BinaryRelator(x ▫_▫_)
    binary₂₃ = intro(\p q → substitution (reflexivity(_≡_)) p q)
    substitution-unary₁ = \{a b x y} → UnaryRelator.substitution(unary₁ {a}{b}) {x}{y}
    substitution-unary₂ = \{a b x y} → UnaryRelator.substitution(unary₂ {a}{b}) {x}{y}
    substitution-unary₃ = \{a b x y} → UnaryRelator.substitution(unary₃ {a}{b}) {x}{y}
    substitution-binary₁₂ = \{a x₁ x₂ y₁ y₂} → BinaryRelator.substitution(binary₁₂ {a}) {x₁}{x₂}{y₁}{y₂}
    substitution-binary₁₃ = \{a x₁ x₂ y₁ y₂} → BinaryRelator.substitution(binary₁₃ {a}) {x₁}{x₂}{y₁}{y₂}
    substitution-binary₂₃ = \{a x₁ x₂ y₁ y₂} → BinaryRelator.substitution(binary₂₃ {a}) {x₁}{x₂}{y₁}{y₂}
  substitute₃ = inst-fn TrinaryRelator.substitution
  substitute₃-unary₁ = inst-fn TrinaryRelator.substitution-unary₁
  substitute₃-unary₂ = inst-fn TrinaryRelator.substitution-unary₂
  substitute₃-unary₃ = inst-fn TrinaryRelator.substitution-unary₃
  substitute₃-binary₁₂ = inst-fn TrinaryRelator.substitution-binary₁₂
  substitute₃-binary₁₃ = inst-fn TrinaryRelator.substitution-binary₁₃
  substitute₃-binary₂₃ = inst-fn TrinaryRelator.substitution-binary₂₃
  trinaryRelator = resolve TrinaryRelator

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:
module IID-Proof-Test where

open import LF
open import Identity
open import IID
open import IIDr
open import DefinitionalEquality
open import IID-Proof-Setup

η : {I : Set}(γ : OPg I)(U : I -> Set) -> Args γ U -> Args γ U
η (ι i)	  U _ = ★
η (σ A γ) U a = < a₀ | η (γ a₀) U a₁ >
  where
    a₀ = π₀ a
    a₁ = π₁ a
η (δ A i γ) U a = < a₀ | η γ U a₁ >
  where
    a₀ = π₀ a
    a₁ = π₁ a

r←→gArgs-equal :
  {I : Set}(γ : OPg I)(U : I -> Set)
  (i : I)(a : Args (ε γ i) U) ->
  _==_ {I × \i -> Args (ε γ i) U}
  < index γ U (r→gArgs γ U i a) |
    g→rArgs γ U (r→gArgs γ U i a)
  > < i | a >
r←→gArgs-equal {I} (ι i) U j < p | ★ > = elim== i (\k q -> _==_ {I × \k -> Args (ε (ι i) k) U}
								< i | < refl | ★ > >
								< k | < q | ★ > >
						  ) refl j p
r←→gArgs-equal {I} (σ A γ)   U j < a | b > = cong f ih
  where ih = r←→gArgs-equal (γ a) U j b
	f : (I × \i -> Args (ε (γ a) i) U) -> (I × \i -> Args (ε (σ A γ) i) U)
	f < k | q > = < k | < a | q > >
r←→gArgs-equal {I} (δ H i γ) U j < g | b > = cong f ih
  where ih = r←→gArgs-equal γ U j b
	f : (I × \k -> Args (ε γ k) U) -> (I × \k -> Args (ε (δ H i γ) k) U)
	f < k | q > = < k | < g | q > >

{-
r←→gArgs-subst-identity' :
  {I  : Set}(γ : OPg I) ->

  (\(U : I -> Set)(C  : (i : I) -> rArgs (ε γ) U i -> Set)
    (a : Args γ U)(h : C (index γ U   (r→gArgs γ U (index γ U (η γ U a)) (g→rArgs γ U (η γ U a))))
			 (g→rArgs γ U (r→gArgs γ U (index γ U (η γ U a)) (g→rArgs γ U (η γ U a))))
		  ) -> r←→gArgs-subst γ U C (index γ U (η γ U a)) (g→rArgs γ U (η γ U a)) h
  ) ==¹
  (\(U : I -> Set)(C  : (i : I) -> rArgs (ε γ) U i -> Set)
    (a : Args γ U)(h : C (index γ U   (r→gArgs γ U (index γ U (η γ U a)) (g→rArgs γ U (η γ U a))))
			 (g→rArgs γ U (r→gArgs γ U (index γ U (η γ U a)) (g→rArgs γ U (η γ U a))))
		  ) -> h
  )
r←→gArgs-subst-identity' (ι i)	   = refl¹
r←→gArgs-subst-identity' (σ A γ)   = ?
r←→gArgs-subst-identity' (δ A i γ) = subst¹ (\ ∙ -> f ∙ ==¹ f (\U C a h -> h))
					    (r←→gArgs-subst-identity' γ) ?
  where
    ih = r←→gArgs-subst-identity' γ
    f = \g U C a h -> g U (\i c -> C i < π₀ a | c >) (π₁ a) h
-}


text:
module Nat where

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

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --allow-unsolved-metas #-}

module StateSizedIO.GUI.BaseStateDependent where

open import Size renaming (Size to AgdaSize)
open import NativeIO
open import Function
open import Agda.Primitive
open import Level using (_⊔_) renaming (suc to lsuc)
open import Data.Product
open import Relation.Binary.PropositionalEquality

record IOInterfaceˢ {γ ρ μ} : Set (lsuc (γ ⊔ ρ ⊔ μ )) where
  field
    Stateˢ    : Set γ
    Commandˢ  : Stateˢ → Set ρ
    Responseˢ : (s : Stateˢ) → Commandˢ s → Set μ
    nextˢ     : (s : Stateˢ) → (c : Commandˢ s) → Responseˢ s c → Stateˢ
open IOInterfaceˢ public

module _  {γ ρ μ}(i   : IOInterfaceˢ {γ} {ρ} {μ} )
                                (let S = Stateˢ i)     (let C  = Commandˢ i)
                                (let  R  = Responseˢ i) (let next = nextˢ i)

  where
    mutual
      record IOˢ {α} (i : AgdaSize)  (A : S → Set α) (s : S) : Set (lsuc (α ⊔ γ ⊔ ρ ⊔ μ )) where
        coinductive
        constructor delay
        field
          forceˢ : {j : Size< i} → IOˢ' j A s

      data IOˢ' {α} (i : AgdaSize)  (A : S → Set α) : S → Set (lsuc (α ⊔ γ ⊔ ρ ⊔ μ )) where
        doˢ'     : {s : S} → (c : C s) → (f : (r : R s c) → IOˢ i A (next s c r) )
                   → IOˢ' i A s
        returnˢ' : {s : S} → (a : A s) → IOˢ' i A s

    data IOˢ+ {α} (i : AgdaSize)  (A : S → Set α ) : S → Set (lsuc (α ⊔ γ ⊔ ρ ⊔ μ )) where
      doˢ' : {s : S} → (c : C s) (f : (r : R s c) → IOˢ i A  (next s c r))
            → IOˢ+ i A s

    IOₚˢ : ∀{α}(i : AgdaSize)(A : Set α)(t t' : S) → Set (lsuc (α ⊔ γ ⊔ ρ ⊔ μ ))
    IOₚˢ i A t t' = IOˢ i (λ s → s ≡ t' × A) t

    IOₚˢ' : ∀{α}(i : AgdaSize)(A : Set α)(t t' : S) → Set (lsuc (α ⊔ γ ⊔ ρ ⊔ μ ))
    IOₚˢ' i A t t' = IOˢ' i (λ s → s ≡ t' × A) t

    IOₚsemiˢ : ∀{i}{α}{β}{A : Set α }{B : S → Set β}{t : S}
               (t' : A → S) → Set (lsuc α ⊔ (lsuc μ ⊔ (lsuc ρ ⊔ lsuc γ)))
    IOₚsemiˢ{i}{α}{β}{A}{B}{t} t' = IOˢ i (λ s → Σ[ a ∈ A ] (s ≡ t' a)) t

{-
Add also this later:
IO A t t'     where t' : A -> S
Programs which start in t end with an a : A and a state t' a
IO A t t' = IO   (lambda s.Sigma a : A. s = t' a) t
>==   : (p : IO A t t') (f : (a : A) ->  IO  B (t' a) ) ->   IO B a
-}

open IOˢ public

module _  {α γ ρ μ}{I   : IOInterfaceˢ {γ} {ρ} {μ}}
                   (let S = Stateˢ I)     (let C  = Commandˢ I)
                   (let  R  = Responseˢ I) (let next = nextˢ I) where
  returnˢ : ∀{i}{A : S → Set α} {s : S} (a : A s) → IOˢ  I i A s
  forceˢ (returnˢ a) = returnˢ' a

  doˢ  : ∀{i}{A : S → Set α}{s : S}
         (c : C s)
         (f : (r : R s c) → IOˢ I i A (next s c r))
         → IOˢ I i A s
  forceˢ (doˢ c f) = doˢ' c f

module _  {α β γ ρ μ}{I   : IOInterfaceˢ {γ} {ρ} {μ}}
                   (let S = Stateˢ I)     (let C  = Commandˢ I)
                   (let  R  = Responseˢ I) (let next = nextˢ I) where

  mutual  -- TODO: check that next state is honored
    fmapˢ : ∀ {i} → {A : S → Set α}{B : S → Set β}
                      (f : (s : S)(a : A s) → B s)
                      {s : S}
                      (p : (IOˢ I i A s))
                      → IOˢ I i B s
    fmapˢ f {s} p .forceˢ = fmapˢ' f {s} (p .forceˢ)

    fmapˢ' : ∀ {i} → {A : S → Set α}{B : S → Set β}
                      (f : (s : S)(a : A s) → B s)
                      {s : S}
                      (p : (IOˢ' I i A s))
                      → IOˢ' I i B s
    fmapˢ' f {s} (doˢ' c g) = doˢ' c  (λ r → fmapˢ f (g r))
    fmapˢ' f {s} (returnˢ' a) = returnˢ' (f s a)

module _  {α γ ρ μ}{I   : IOInterfaceˢ {γ} {ρ} {μ}}
                   (let S = Stateˢ I)     (let C  = Commandˢ I)
                   (let  R  = Responseˢ I) (let next = nextˢ I) where

  delayˢ : ∀ {i}{A : S → Set α}{s : S} → IOˢ' I i A s → IOˢ I (↑ i) A s
  delayˢ p .forceˢ = p

module _  {γ ρ μ}{I   : IOInterfaceˢ {γ} {ρ} {μ}}
                   (let S = Stateˢ I)     (let C  = Commandˢ I)
                   (let  R  = Responseˢ I) (let next = nextˢ I) where

  mutual

    _>>=ˢ'_ : ∀{i α β}{A : S → Set α}{B : S → Set β}{t : S}
               (m : IOˢ' I i A t)
               (f : (s : S)(a : A s) → IOˢ I (↑ i) B s)
               → IOˢ' I i B t
    doˢ' c f >>=ˢ' k = doˢ' c λ x → f x >>=ˢ k
    _>>=ˢ'_ {_} {_} {_} {_} {_} {t} (returnˢ' a) f =  f t a .forceˢ

    _>>=ˢ_ : ∀{i α β}{A : S → Set α}{B : S → Set β}{t : S}
             (m : IOˢ I i A t)
             (k : (s : S)(a : A s) → IOˢ I i B s)
             → IOˢ I i B t
    forceˢ (m >>=ˢ k) = (forceˢ m) >>=ˢ' k

    _>>=ₚˢ'_ : ∀{i}{α}{β}{A : Set α }{B : S → Set β}{t t' : S}
               (p : IOˢ' I i (λ s → s ≡ t' × A) t)
               (f : (a : A) → IOˢ I (↑ i) B t')
               → IOˢ' {γ} {ρ} {μ}  I i B t
    _>>=ₚˢ'_ {i} {α} {β} p  f =  p >>=ˢ' (λ s → λ {(refl , a) → f a})

    _>>=ₚˢ_ : ∀{i}{α}{β}{A : Set α }{B : S → Set β}{t t' : S}
               (p : IOˢ I i (λ s → s ≡ t' × A) t)
               (f : (a : A) → IOˢ I (↑ i) B t')
               → IOˢ I i B t
    _>>=ₚˢ_ {i} {α} {β} p  f = p >>=ˢ (λ s → λ {(refl , a) → f a})

    _>>=ₚsemiˢ_ : ∀{i}{α}{β}{A : Set α }{B : S → Set β}{t : S}
               {t' : A → S}
               -- IOs starts in t, returns a, and ends in a state t' a:
               (p : IOˢ I i (λ s → Σ[ a ∈ A ] (s ≡ t' a)) t)
               (f : (a : A) → IOˢ I (↑ i) B (t' a))
               → IOˢ I i B t
    _>>=ₚsemiˢ_ {i} {α} {β}{A}{B}{t}{t'} p f = p >>=ˢ f'
      module aux where
      f' : (s : Stateˢ I) → Σ[ a ∈ A ] (s ≡ t' a) → IOˢ I i B s
      f' .(t' a) (a , refl) = f a

module _  {γ ρ}{I   : IOInterfaceˢ {γ} {ρ} {lzero}}
                (let S = Stateˢ I)     (let C  = Commandˢ I)
                (let  R  = Responseˢ I) (let next = nextˢ I) where
  {-# NON_TERMINATING #-}

  translateIOˢ : ∀{A : Set }{s : S}
    →  (translateLocal : (s : S) → (c : C s) → NativeIO (R s c))
    →  IOˢ I ∞ (λ s → A) s
    →  NativeIO A
  translateIOˢ {A} {s} translateLocal p = case (forceˢ p {_}) of
    λ{ (doˢ' {.s} c f)    → (translateLocal s c)     native>>= λ r →
                             translateIOˢ translateLocal (f r)
     ; (returnˢ' a) → nativeReturn a
     }

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


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

module Control.Monad.Levels.Definition where

open import Prelude
open import Data.Bag

data Levels (A : Type a) : Type a where
  _∷_ : ⟅ A ⟆ → Levels A → Levels A
  []  : Levels A

  trail : [] ∷ [] ≡ []
  trunc : isSet (Levels A)


text:
module Issue474 where

open import Common.Level

postulate
  a b c : Level
  A : Set a
  B : Set b
  C : Set c

data Foo : Set (lsuc lzero ⊔ (a ⊔ (b ⊔ c))) where
  foo : (Set → A → B) → Foo


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

-- A cartesian functor preserves products (of cartesian categories)
module Categories.Functor.Cartesian where

open import Level

open import Categories.Category.Cartesian.Structure
open import Categories.Functor using (Functor; _∘F_)
open import Categories.Functor.Properties

import Categories.Object.Product as P
import Categories.Object.Terminal as ⊤
import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e o′ ℓ′ e′ : Level

record IsCartesianF (C : CartesianCategory o ℓ e) (D : CartesianCategory o′ ℓ′ e′)
  (F : Functor (CartesianCategory.U C) (CartesianCategory.U D)) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  private
    module C = CartesianCategory C
    module D = CartesianCategory D
    open P D.U
    open ⊤ D.U
    open M D.U
    open Functor F

  field
    F-resp-⊤ : IsTerminal (F₀ C.⊤)
    F-resp-× : ∀ {A B} → IsProduct {P = F₀ (A C.× B)} (F₁ C.π₁) (F₁ C.π₂)

  module F-resp-⊤ = IsTerminal F-resp-⊤
  module F-resp-× {A B} = IsProduct (F-resp-× {A} {B})

  F-prod : ∀ A B → Product (F₀ A) (F₀ B)
  F-prod _ _ = IsProduct⇒Product F-resp-×

  module F-prod A B = Product (F-prod A B)

  F-resp-⟨⟩ : ∀ {A B X} → (f : X C.⇒ A) (g : X C.⇒ B) → D.⟨ F₁ C.π₁ , F₁ C.π₂ ⟩ D.∘ F₁ C.⟨ f , g ⟩ D.≈ D.⟨ F₁ f , F₁ g ⟩
  F-resp-⟨⟩ f g = begin
    D.⟨ F₁ C.π₁ , F₁ C.π₂ ⟩ D.∘ F₁ C.⟨ f , g ⟩                    ≈⟨ D.⟨⟩∘ ⟩
    D.⟨ F₁ C.π₁ D.∘ F₁ C.⟨ f , g ⟩ , F₁ C.π₂ D.∘ F₁ C.⟨ f , g ⟩ ⟩ ≈⟨ D.⟨⟩-cong₂ ([ F ]-resp-∘ C.project₁) ([ F ]-resp-∘ C.project₂) ⟩
    D.⟨ F₁ f , F₁ g ⟩                                             ∎
    where open D.HomReasoning

  ⊤-iso : F₀ C.⊤ ≅ D.⊤
  ⊤-iso = ⊤.up-to-iso D.U (record { ⊤-is-terminal = F-resp-⊤ }) D.terminal

  module ⊤-iso = _≅_ ⊤-iso

  ×-iso : ∀ A B → F₀ (A C.× B) ≅ F₀ A D.× F₀ B
  ×-iso A B = record
    { from = D.⟨ F₁ C.π₁ , F₁ C.π₂ ⟩
    ; to   = F-resp-×.⟨ D.π₁ , D.π₂ ⟩
    ; iso  = record
      { isoˡ = begin
        F-resp-×.⟨ D.π₁ , D.π₂ ⟩ D.∘ D.⟨ F₁ C.π₁ , F₁ C.π₂ ⟩ ≈⟨ [ F-prod A B ]⟨⟩∘ ⟩
        F-resp-×.⟨ D.π₁ D.∘ _ , D.π₂ D.∘ _ ⟩                 ≈⟨ F-prod.⟨⟩-cong₂ A B D.project₁ D.project₂ ⟩
        F-resp-×.⟨ F₁ C.π₁ , F₁ C.π₂ ⟩                       ≈⟨ F-prod.η A B ⟩
        D.id                                                 ∎
      ; isoʳ = begin
        D.⟨ F₁ C.π₁ , F₁ C.π₂ ⟩ D.∘ F-resp-×.⟨ D.π₁ , D.π₂ ⟩ ≈⟨ D.⟨⟩∘ ⟩
        D.⟨ F₁ C.π₁ D.∘ _ , F₁ C.π₂ D.∘ _ ⟩                  ≈⟨ D.⟨⟩-cong₂ (F-prod.project₁ A B) (F-prod.project₂ A B) ⟩
        D.⟨ D.π₁ , D.π₂ ⟩                                    ≈⟨ D.η ⟩
        D.id                                                 ∎
      }
    }
    where open D.HomReasoning

  module ×-iso A B = _≅_ (×-iso A B)

  F-resp-⟨⟩′ : ∀ {A B X} → (f : X C.⇒ A) (g : X C.⇒ B) → F₁ C.⟨ f , g ⟩ D.≈ F-resp-×.⟨ F₁ f , F₁ g ⟩
  F-resp-⟨⟩′ f g = begin
    F₁ C.⟨ f , g ⟩                     ≈⟨ switch-fromtoˡ (×-iso _ _) (F-resp-⟨⟩ f g) ⟩
    ×-iso.to _ _ D.∘ D.⟨ F₁ f , F₁ g ⟩ ≈⟨ ([ F-prod _ _ ]⟨⟩∘ ○ F-prod.⟨⟩-cong₂ _ _ D.project₁ D.project₂) ⟩
    F-resp-×.⟨ F₁ f , F₁ g ⟩           ∎
    where open MR D.U
          open D.HomReasoning

record CartesianF (C : CartesianCategory o ℓ e) (D : CartesianCategory o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  private
    module C = CartesianCategory C
    module D = CartesianCategory D

  field
    F           : Functor C.U D.U
    isCartesian : IsCartesianF C D F

  open Functor F public
  open IsCartesianF isCartesian public

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
module Text.Greek.Bible where

open import Data.Nat
open import Data.List
open import Data.String
open import Text.Greek.Script

data Word : Set where
  word : (List Token) → String → Word

max_stars_repo_name: scott-fleischman/GreekGrammar

max_issues_repo_name: scott-fleischman/GreekGrammar

max_forks_repo_name: scott-fleischman/GreekGrammar