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

open import lib.Basics
open import lib.NType2
open import lib.types.Pi
open import lib.types.Group
open import lib.types.Int
open import lib.types.List
open import lib.types.Word
open import lib.types.SetQuotient
open import lib.groups.Homomorphism

module lib.groups.GeneratedGroup {i m} where

module GeneratedGroup (A : Type i) (R : Rel (Word A) m) where

  -- [qwr-sym] is not needed, but it seems more principled to
  -- make [QuotWordRel] an equivalence relation.
  data QuotWordRel : Word A → Word A → Type (lmax i m) where
    qwr-refl : ∀ {l₁ l₂} → l₁ == l₂ → QuotWordRel l₁ l₂
    qwr-trans : ∀ {l₁ l₂ l₃} → QuotWordRel l₁ l₂ → QuotWordRel l₂ l₃ → QuotWordRel l₁ l₃
    qwr-sym : ∀ {l₁ l₂} → QuotWordRel l₁ l₂ → QuotWordRel l₂ l₁
    qwr-cong : ∀ {l₁ l₂ l₃ l₄} → QuotWordRel l₁ l₂ → QuotWordRel l₃ l₄ → QuotWordRel (l₁ ++ l₃) (l₂ ++ l₄)
    qwr-flip-r : ∀ x₁ → QuotWordRel (x₁ :: flip x₁ :: nil) nil
    qwr-rel : ∀ {l₁ l₂} → R l₁ l₂ → QuotWordRel l₁ l₂

  qwr-cong-l : ∀ {l₁ l₂} → QuotWordRel l₁ l₂ → ∀ l₃ → QuotWordRel (l₁ ++ l₃) (l₂ ++ l₃)
  qwr-cong-l qwr l₃ = qwr-cong qwr (qwr-refl idp)

  qwr-cong-r : ∀ l₁ {l₂ l₃} → QuotWordRel l₂ l₃ → QuotWordRel (l₁ ++ l₂) (l₁ ++ l₃)
  qwr-cong-r l₁ qwr = qwr-cong (qwr-refl (idp {a = l₁})) qwr

  abstract
    infixr 10 _qwr⟨_⟩_
    infixr 10 _qwr⟨id⟩_
    infix  15 _qwr∎

    _qwr⟨_⟩_ : ∀  l₁ {l₂ l₃} → QuotWordRel l₁ l₂ → QuotWordRel l₂ l₃ → QuotWordRel l₁ l₃
    _ qwr⟨ p ⟩ q = qwr-trans p q

    _qwr⟨id⟩_ : ∀  l₁ {l₂} → QuotWordRel l₁ l₂ → QuotWordRel l₁ l₂
    _ qwr⟨id⟩ q = q

    _qwr∎ : ∀ l → QuotWordRel l l
    _ qwr∎ = qwr-refl idp

  qwr-flip-l : ∀ x₁ → QuotWordRel (flip x₁ :: x₁ :: nil) nil
  qwr-flip-l x₁ =
    flip x₁ :: x₁ :: nil
      qwr⟨ qwr-refl (ap (λ s → flip x₁ :: s :: nil) (! (flip-flip x₁))) ⟩
    flip x₁ :: flip (flip x₁) :: nil
      qwr⟨ qwr-flip-r (flip x₁) ⟩
    nil qwr∎

  -- The quotient
  QuotWord : Type (lmax i m)
  QuotWord = SetQuot QuotWordRel

  qw[_] : Word A → QuotWord
  qw[_] = q[_]

  {-
    In the case where this module is used to realize some free construction F
    (e.g. free group, free abelian group), this function becomes the unit of
    the adjunction F -| U (where U is the forgetful functor).
  -}
  insert : A → QuotWord
  insert a = qw[ inl a :: nil ]

  module QuotWordElim {k} {P : QuotWord → Type k}
    {{_ : {x : QuotWord} → is-set (P x)}} (incl* : (a : Word A) → P qw[ a ])
    (rel* : ∀ {a₁ a₂} (r : QuotWordRel a₁ a₂) → incl* a₁ == incl* a₂ [ P ↓ quot-rel r ])
    = SetQuotElim incl* rel*
  open QuotWordElim public renaming (f to QuotWord-elim) hiding (quot-rel-β)

  module QuotWordRec {k} {B : Type k} {{_ : is-set B}} (incl* : Word A → B)
    (rel* : ∀ {a₁ a₂} (r : QuotWordRel a₁ a₂) → incl* a₁ == incl* a₂)
    = SetQuotRec incl* rel*
  open QuotWordRec public renaming (f to QuotWord-rec)

  private
    infixl 80 _⊞_
    _⊞_ : QuotWord → QuotWord → QuotWord
    _⊞_ = QuotWord-rec
      (λ l₁ → QuotWord-rec (λ l₂ → qw[ l₁ ++ l₂ ])
        (λ r → quot-rel $ qwr-cong-r l₁ r))
      (λ {l₁} {l₁'} r → λ= $ QuotWord-elim
        (λ l₂ → quot-rel $ qwr-cong-l r l₂)
        (λ _ → prop-has-all-paths-↓))

    abstract
      qwr-cancel-l : ∀ l
        → QuotWordRel (Word-inverse l ++ l) nil
      qwr-cancel-l nil = qwr-refl idp
      qwr-cancel-l (x :: l) =
        Word-inverse (x :: l) ++ (x :: l)
          qwr⟨id⟩
        (Word-inverse l ++ (flip x :: nil)) ++ (x :: l)
          qwr⟨ qwr-refl (++-assoc (reverse (Word-flip l)) (flip x :: nil) (x :: l)) ⟩
        Word-inverse l ++ ((flip x :: nil) ++ (x :: l))
          qwr⟨id⟩
        Word-inverse l ++ (flip x :: x :: l)
          qwr⟨ qwr-cong-r (reverse (Word-flip l)) (qwr-cong-l (qwr-flip-l x) l) ⟩
        Word-inverse l ++ l
          qwr⟨ qwr-cancel-l l ⟩
        nil qwr∎

      qwr-cancel-r : ∀ l
        → QuotWordRel (l ++ Word-inverse l) nil
      qwr-cancel-r l =
        l ++ Word-inverse l
          qwr⟨ qwr-refl (ap (_++ Word-inverse l) (! (Word-inverse-inverse l))) ⟩
        Word-inverse (Word-inverse l) ++ Word-inverse l
          qwr⟨ qwr-cancel-l (Word-inverse l) ⟩
        nil qwr∎

      qwr-cong-inverse : ∀ {l₁ l₂}
        → QuotWordRel l₁ l₂ → QuotWordRel (Word-inverse l₁) (Word-inverse l₂)
      qwr-cong-inverse {l₁} {l₂} r =
        Word-inverse l₁
          qwr⟨ qwr-refl (! (++-unit-r (Word-inverse l₁))) ⟩
        Word-inverse l₁ ++ nil
          qwr⟨ qwr-cong-r (Word-inverse l₁) (qwr-sym (qwr-cancel-r l₂)) ⟩
        Word-inverse l₁ ++ (l₂ ++ Word-inverse l₂)
          qwr⟨ qwr-cong-r (Word-inverse l₁) (qwr-cong-l (qwr-sym r) (Word-inverse l₂)) ⟩
        reverse (Word-flip l₁) ++ (l₁ ++ Word-inverse l₂)
          qwr⟨ qwr-refl (! (++-assoc (Word-inverse l₁) l₁ (Word-inverse l₂))) ⟩
        (Word-inverse l₁ ++ l₁) ++ Word-inverse l₂
          qwr⟨ qwr-cong-l (qwr-cancel-l l₁) (Word-inverse l₂) ⟩
        Word-inverse l₂ qwr∎

    ⊟ : QuotWord → QuotWord
    ⊟ = QuotWord-rec (qw[_] ∘ Word-inverse)
      (λ r → quot-rel $ qwr-cong-inverse r)

    ⊞-unit : QuotWord
    ⊞-unit = qw[ nil ]

    abstract
      ⊞-unit-l : ∀ g → ⊞-unit ⊞ g == g
      ⊞-unit-l = QuotWord-elim
        (λ _ → idp)
        (λ _ → prop-has-all-paths-↓)

      ⊞-assoc : ∀ g₁ g₂ g₃ → (g₁ ⊞ g₂) ⊞ g₃ == g₁ ⊞ (g₂ ⊞ g₃)
      ⊞-assoc = QuotWord-elim
        (λ l₁ → QuotWord-elim
          (λ l₂ → QuotWord-elim
            (λ l₃ → ap qw[_] $ ++-assoc l₁ l₂ l₃)
            (λ _ → prop-has-all-paths-↓))
          (λ _ → prop-has-all-paths-↓))
        (λ _ → prop-has-all-paths-↓)

      ⊟-inv-l : ∀ g → (⊟ g) ⊞ g == ⊞-unit
      ⊟-inv-l = QuotWord-elim
        (λ l → quot-rel (qwr-cancel-l l))
        (λ _ → prop-has-all-paths-↓)

  QuotWord-group-structure : GroupStructure QuotWord
  QuotWord-group-structure = record
    { ident = ⊞-unit
    ; inv = ⊟
    ; comp = _⊞_
    ; unit-l = ⊞-unit-l
    ; assoc = ⊞-assoc
    ; inv-l = ⊟-inv-l
    }

  GenGroup : Group (lmax i m)
  GenGroup = group _ QuotWord-group-structure

  module GenGroup = Group GenGroup
  open GenGroup using (El) public

  abstract
    pres-exp : ∀ (a : A) z →
      qw[ Word-exp a z ] == GenGroup.exp qw[ inl a :: nil ] z
    pres-exp a (pos O) = idp
    pres-exp a (pos (S O)) = idp
    pres-exp a (pos (S (S n))) =
      ap (GenGroup.comp qw[ inl a :: nil ]) (pres-exp a (pos (S n)))
    pres-exp a (negsucc O) = idp
    pres-exp a (negsucc (S n)) =
      ap (GenGroup.comp qw[ inr a :: nil ]) (pres-exp a (negsucc n))

    rel-holds : ∀ {w₁} {w₂} (r : R w₁ w₂) → qw[ w₁ ] == qw[ w₂ ]
    rel-holds r = quot-rel (qwr-rel r)

  -- freeness
  module HomomorphismEquiv {j} (G : Group j) where

    private
      module G = Group G
    open RelationRespectingFunctions A R G public

    module _ (fun : RelationRespectingFunction) where

      private
        module fun = RelationRespectingFunction fun
        f* = fun.f

        abstract
          Word-extendᴳ-emap : ∀ {l₁ l₂}
            → QuotWordRel l₁ l₂
            → Word-extendᴳ G f* l₁ == Word-extendᴳ G f* l₂
          Word-extendᴳ-emap (qwr-refl idp) = idp
          Word-extendᴳ-emap (qwr-trans qwr qwr₁) = (Word-extendᴳ-emap qwr) ∙ (Word-extendᴳ-emap qwr₁)
          Word-extendᴳ-emap (qwr-sym qwr) = ! (Word-extendᴳ-emap qwr)
          Word-extendᴳ-emap (qwr-flip-r x) =
            G.comp (PlusMinus-extendᴳ G f* x) (PlusMinus-extendᴳ G f* (flip x))
              =⟨ ap (G.comp (PlusMinus-extendᴳ G f* x)) (PlusMinus-extendᴳ-flip G f* x) ⟩
            G.comp (PlusMinus-extendᴳ G f* x) (G.inv (PlusMinus-extendᴳ G f* x))
              =⟨ G.inv-r (PlusMinus-extendᴳ G f* x) ⟩
            G.ident =∎
          Word-extendᴳ-emap (qwr-cong {l₁} {l₂} {l₃} {l₄} qwr qwr') =
            Word-extendᴳ G f* (l₁ ++ l₃)
              =⟨ Word-extendᴳ-++ G f* l₁ l₃ ⟩
            G.comp (Word-extendᴳ G f* l₁) (Word-extendᴳ G f* l₃)
              =⟨ ap2 G.comp (Word-extendᴳ-emap qwr) (Word-extendᴳ-emap qwr') ⟩
            G.comp (Word-extendᴳ G f* l₂) (Word-extendᴳ G f* l₄)
              =⟨ ! (Word-extendᴳ-++ G f* l₂ l₄) ⟩
            Word-extendᴳ G f* (l₂ ++ l₄) =∎
          Word-extendᴳ-emap (qwr-rel r) = fun.respects r

      extend : (GenGroup →ᴳ G)
      extend = record {M} where
        module M where
          f : QuotWord → G.El
          f = QuotWord-rec (Word-extendᴳ G f*)
              (λ r → Word-extendᴳ-emap r)
          abstract
            pres-comp : preserves-comp GenGroup.comp G.comp f
            pres-comp =
              QuotWord-elim
                (λ l₁ → QuotWord-elim
                  (λ l₂ → Word-extendᴳ-++ G f* l₁ l₂)
                  (λ _ → prop-has-all-paths-↓))
                (λ _ → prop-has-all-paths-↓)

    private
      module Lemma (hom : GenGroup →ᴳ G) where
        private
          open GroupHom hom
          restr : A → G.El
          restr a = f qw[ inl a :: nil ]

        abstract
          PlusMinus-extendᴳ-hom : ∀ x → PlusMinus-extendᴳ G restr x == f qw[ x :: nil ]
          PlusMinus-extendᴳ-hom (inl x) = idp
          PlusMinus-extendᴳ-hom (inr x) = ! $ pres-inv qw[ inl x :: nil ]

          Word-extendᴳ-hom : ∀ l → Word-extendᴳ G restr l == f qw[ l ]
          Word-extendᴳ-hom nil = ! pres-ident
          Word-extendᴳ-hom (x :: nil) = PlusMinus-extendᴳ-hom x
          Word-extendᴳ-hom (x :: l@(_ :: _)) =
            G.comp (PlusMinus-extendᴳ G restr x) (Word-extendᴳ G restr l)
              =⟨ ap2 G.comp (PlusMinus-extendᴳ-hom x) (Word-extendᴳ-hom l) ⟩
            G.comp (f qw[ x :: nil ]) (f qw[ l ])
              =⟨ ! (pres-comp _ _) ⟩
            f qw[ x :: l ] =∎

          restr-respects-rel : ∀ {l₁ l₂} → R l₁ l₂ → Word-extendᴳ G restr l₁ == Word-extendᴳ G restr l₂
          restr-respects-rel {l₁} {l₂} r =
            Word-extendᴳ G restr l₁
              =⟨ Word-extendᴳ-hom l₁ ⟩
            f qw[ l₁ ]
              =⟨ ap f (quot-rel (qwr-rel r)) ⟩
            f qw[ l₂ ]
              =⟨ ! (Word-extendᴳ-hom l₂) ⟩
            Word-extendᴳ G restr l₂ =∎

        restrict : RelationRespectingFunction
        restrict = rel-res-fun restr restr-respects-rel

      open Lemma

    extend-is-equiv : is-equiv extend
    extend-is-equiv = is-eq _ from to-from from-to where
      to = extend
      from = restrict

      abstract
        to-from : ∀ h → to (from h) == h
        to-from h = group-hom= $ λ= $ QuotWord-elim
          (λ l → Word-extendᴳ-hom h l)
          (λ _ → prop-has-all-paths-↓)

        from-to : ∀ fun → from (to fun) == fun
        from-to fun = RelationRespectingFunction= (λ= λ a → idp)

    extend-equiv : RelationRespectingFunction ≃ (GenGroup →ᴳ G)
    extend-equiv = extend , extend-is-equiv

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
module Nat.Class where

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

record Nat (ℕ : Set) : Set₁ where
  field
    zero : ℕ
    succ : ℕ → ℕ

    ind : (P : ℕ → Set) → P zero → (∀ {k} → P k → P (succ k)) → ∀ n → P n

    _+_ : ℕ → ℕ → ℕ
    +-zero : ∀ {n} → zero + n ≡ n
    +-succ : ∀ {m n} → succ m + n ≡ m + succ n

module _ {ℕ : Set} {{nn : Nat ℕ}} where
  open Nat nn

  +-succˡ : {m n : ℕ} → succ m + n ≡ succ (m + n)
  +-succˡ {m} {n} = ind Succˡ Succˡ-zero Succˡ-succ m n
    where
      Succˡ : ℕ → Set
      Succˡ m′ = ∀ n′ → succ m′ + n′ ≡ succ (m′ + n′)

      Succˡ-zero : Succˡ zero
      Succˡ-zero n′ =
        begin
          succ zero + n′
        ≡⟨ +-succ ⟩
          zero + succ n′
        ≡⟨ +-zero ⟩
          succ n′
        ≡⟨ cong succ (sym +-zero) ⟩
          succ (zero + n′)
        ∎

      Succˡ-succ : ∀ {m′} → Succˡ m′ → Succˡ (succ m′)
      Succˡ-succ {m′} ih n′ =
        begin
          succ (succ m′) + n′
        ≡⟨ +-succ ⟩
          succ m′ + succ n′
        ≡⟨ ih (succ n′) ⟩
          succ (m′ + succ n′)
        ≡⟨ cong succ (sym +-succ) ⟩
          succ (succ m′ + n′)
        ∎

  +-succʳ : {m n : ℕ} → m + succ n ≡ succ (m + n)
  +-succʳ = trans (sym +-succ) +-succˡ

  +-assoc : {m n p : ℕ} → (m + n) + p ≡ m + (n + p)
  +-assoc {m} {n} {p} = ind Assoc Assoc-zero Assoc-succ m
    where
      Assoc : ℕ → Set
      Assoc k = (k + n) + p ≡ k + (n + p)

      Assoc-zero : Assoc zero
      Assoc-zero =
        begin
          (zero + n) + p
        ≡⟨ cong (_+ p) +-zero ⟩
          n + p
        ≡⟨ sym +-zero ⟩
          zero + (n + p)
        ∎

      Assoc-succ : ∀ {k} → Assoc k → Assoc (succ k)
      Assoc-succ {k} ih =
        begin
          (succ k + n) + p
        ≡⟨ cong (_+ p) +-succˡ ⟩
          succ (k + n) + p
        ≡⟨ +-succˡ ⟩
          succ ((k + n) + p)
        ≡⟨ cong succ ih ⟩
          succ (k + (n + p))
        ≡⟨ sym +-succˡ ⟩
          succ k + (n + p)
        ∎

ext: agda

max_stars_repo_name: iblech/agda-quotients

max_issues_repo_name: iblech/agda-quotients

max_forks_repo_name: iblech/agda-quotients


text:
------------------------------------------------------------------------
-- Small parser combinator library used by Mixfix.Cyclic.Grammar
------------------------------------------------------------------------

module Mixfix.Cyclic.Lib where

open import Algebra
open import Codata.Musical.Notation
open import Function using (const)
open import Data.Bool using (Bool; true; false)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.List using (List; []; _∷_; _++_)
import Data.List.Properties
private module LM {A : Set} = Monoid (Data.List.Properties.++-monoid A)
open import Data.List.NonEmpty using (List⁺; _∷_; [_]; _∷⁺_)
open import Data.Maybe using (Maybe; just; nothing; maybe)
open import Data.Vec using (Vec; []; _∷_)
open import Data.Product
import Data.String.Properties as String
open import Relation.Binary
open DecSetoid String.≡-decSetoid using (_≟_)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)

open import TotalParserCombinators.Parser
  renaming (_⊛_ to _⊛′_; _<$>_ to _<$>′_)
import TotalParserCombinators.Lib as Lib
open import Mixfix.Operator using (NamePart)

private
  open module Tok = Lib.Token NamePart _≟_ using (tok)

------------------------------------------------------------------------
-- Programs

-- Agda's termination checker only accepts corecursive definitions if
-- they are /syntactically/ guarded by constructors. The following
-- small language of "parser programs" reifies a selection of parser
-- combinators as /constructors/. These constructors are then used in
-- Mixfix.Cyclic.Grammar in order to ensure that Agda accepts the
-- grammars defined there.

infix  55 _+
infixl 50 _⊛_ _⊛∞_ _<$>_
infixl  5 _∣_
infixr  5 _∥_

data ParserProg : Set → Set₁ where
  fail      : ∀ {R} → ParserProg R
  _∣_       : ∀ {R}
              (p₁ : ParserProg R)
              (p₂ : ParserProg R) →
                    ParserProg R
  _⊛_       : ∀ {R₁ R₂}
              (p₁ : ParserProg (R₁ → R₂))
              (p₂ : ParserProg R₁) →
                    ParserProg R₂
  _⊛∞_      : ∀ {R₁ R₂}
              (p₁ : ∞ (ParserProg (R₁ → R₂)))
              (p₂ : ∞ (ParserProg R₁)) →
                       ParserProg R₂
  _<$>_     : ∀ {R₁ R₂} (f : R₁ → R₂)
              (p : ParserProg R₁) →
                   ParserProg R₂
  _+        : ∀ {R} (p : ParserProg R) →
                         ParserProg (List⁺ R)
  _between_ : ∀ {R n}
              (p : ∞ (ParserProg R)) (toks : Vec NamePart (1 + n)) →
              ParserProg (Vec R n)
  _∥_       : ∀ {I i} {R : I → Set}
              (p₁ : ParserProg (R i))
              (p₂ : ParserProg (∃ R)) →
                    ParserProg (∃ R)

-- Interprets the parser programs as parsers.

⟦_⟧ : ∀ {R} → ParserProg R → Parser NamePart R []
⟦ fail               ⟧ = fail
⟦ p₁ ∣ p₂            ⟧ = ⟦ p₁ ⟧ ∣ ⟦ p₂ ⟧
⟦ p₁ ⊛  p₂           ⟧ =   ⟦   p₁ ⟧ ⊛′   ⟦   p₂ ⟧
⟦ p₁ ⊛∞ p₂           ⟧ = ♯ ⟦ ♭ p₁ ⟧ ⊛′ ♯ ⟦ ♭ p₂ ⟧
⟦ f <$> p            ⟧ = f <$>′ ⟦ p ⟧
⟦ p +                ⟧ = one <$>′  ⟦ p ⟧
                              ⊛′ ♯ (⟦ just <$> p + ⟧ ∣ return nothing)
                         where one = λ x → maybe (_∷⁺_ x) [ x ]
⟦ p between (t ∷ []) ⟧ = const [] <$>′ tok t
⟦ p between
       (t ∷ t′ ∷ ts) ⟧ = const _∷_ <$>′  tok t
                                    ⊛′ ♯ ⟦ ♭ p ⟧
                                    ⊛′ ♯ ⟦ p between (t′ ∷ ts) ⟧
⟦ p₁ ∥ p₂            ⟧ = -,_ <$>′ ⟦ p₁ ⟧
                       ∣          ⟦ p₂ ⟧

------------------------------------------------------------------------
-- Semantics of the programs

module Semantics where

  open import TotalParserCombinators.Semantics as Sem
    renaming ([_-_]_⊛_ to [_-_]_⊛′_)

  -- This definition may seem unnecessary: why not simply define
  --
  --   x ∈⟦ p ⟧· s  =  x ∈ ⟦ p ⟧ · s?
  --
  -- One reason is that it is hard for Agda to infer the value of p
  -- from ⟦ p ⟧ (note that ⟦_⟧ is a function which evaluates). By
  -- using the definition below this problem is avoided. A more
  -- important reason may be that the definition below ensures that
  -- the details of ⟦_⟧ do not need to be understood.

  infix  60 <$>_
  infixl 50 _⊛_ _⊛∞_
  infix  4  _∈⟦_⟧·_

  data _∈⟦_⟧·_ : ∀ {R} → R → ParserProg R → List NamePart → Set₁ where
    ∣ˡ         : ∀ {R x s}
                   {p₁ : ParserProg R} {p₂ : ParserProg R}
                 (x∈p₁ : x ∈⟦ p₁ ⟧· s) → x ∈⟦ p₁ ∣ p₂ ⟧· s
    ∣ʳ         : ∀ {R x s}
                   {p₁ : ParserProg R} {p₂ : ParserProg R}
                 (x∈p₂ : x ∈⟦ p₂ ⟧· s) → x ∈⟦ p₁ ∣ p₂ ⟧· s
    _⊛_        : ∀ {s₁ s₂ R₁ R₂ f x}
                   {p₁ : ParserProg (R₁ → R₂)}
                   {p₂ : ParserProg R₁}
                 (f∈p₁ : f ∈⟦ p₁ ⟧· s₁)
                 (x∈p₂ : x ∈⟦ p₂ ⟧· s₂) →
                 f x ∈⟦ p₁ ⊛ p₂ ⟧· s₁ ++ s₂
    _⊛∞_       : ∀ {s₁ s₂ R₁ R₂ f x}
                   {p₁ : ∞ (ParserProg (R₁ → R₂))}
                   {p₂ : ∞ (ParserProg R₁)}
                 (f∈p₁ : f ∈⟦ ♭ p₁ ⟧· s₁)
                 (x∈p₂ : x ∈⟦ ♭ p₂ ⟧· s₂) →
                 f x ∈⟦ p₁ ⊛∞ p₂ ⟧· s₁ ++ s₂
    <$>_       : ∀ {s R₁ R₂ x} {f : R₁ → R₂} {p : ParserProg R₁}
                 (x∈p : x ∈⟦ p ⟧· s) → f x ∈⟦ f <$> p ⟧· s
    +-[]       : ∀ {R x s} {p : ParserProg R}
                 (x∈p : x ∈⟦ p ⟧· s) → [ x ] ∈⟦ p + ⟧· s
    +-∷        : ∀ {R x s₁ s₂ xs} {p : ParserProg R}
                 (x∈p : x ∈⟦ p ⟧· s₁) (xs∈p : xs ∈⟦ p + ⟧· s₂) →
                 x ∷⁺ xs ∈⟦ p + ⟧· s₁ ++ s₂
    between-[] : ∀ {R t} {p : ∞ (ParserProg R)} →
                 [] ∈⟦ p between (t ∷ []) ⟧· t ∷ []
    between-∷  : ∀ {R n t x xs s₁ s₂}
                   {p : ∞ (ParserProg R)} {ts : Vec NamePart (suc n)}
                 (x∈p : x ∈⟦ ♭ p ⟧· s₁)
                 (xs∈⋯ : xs ∈⟦ p between ts ⟧· s₂) →
                 x ∷ xs ∈⟦ p between (t ∷ ts) ⟧· t ∷ s₁ ++ s₂
    ∥ˡ         : ∀ {I i} {R : I → Set} {x s}
                   {p₁ : ParserProg (R i)}
                   {p₂ : ParserProg (∃ R)}
                 (x∈p₁ : x ∈⟦ p₁ ⟧· s) → (-, x) ∈⟦ p₁ ∥ p₂ ⟧· s
    ∥ʳ         : ∀ {I i} {R : I → Set} {s i′} {x : R i′}
                   {p₁ : ParserProg (R i)}
                   {p₂ : ParserProg (∃ R)}
                 (x∈p₂ : (-, x) ∈⟦ p₂ ⟧· s) → (-, x) ∈⟦ p₁ ∥ p₂ ⟧· s

  -- The semantics is correct. (Note that this proof only establishes
  -- language equivalence, not parser equivalence; see
  -- TotalParserCombinators.Semantics.)

  sound : ∀ {R x s} {p : ParserProg R} →
          x ∈⟦ p ⟧· s → x ∈ ⟦ p ⟧ · s
  sound (∣ˡ x∈p₁)      = ∣-left     (sound x∈p₁)
  sound (∣ʳ x∈p₂)      = ∣-right [] (sound x∈p₂)
  sound (f∈p₁ ⊛  x∈p₂) = [ ○ - ○ ] sound f∈p₁ ⊛′ sound x∈p₂
  sound (f∈p₁ ⊛∞ x∈p₂) = [ ◌ - ◌ ] sound f∈p₁ ⊛′ sound x∈p₂
  sound (<$> x∈p)      = <$> sound x∈p
  sound (+-[] x∈p)     = cast∈ refl refl (proj₂ LM.identity _)
                           ([ ○ - ◌ ] <$> sound x∈p ⊛′ ∣-right [] return)
  sound (+-∷ x∈p xs∈p) = [ ○ - ◌ ] <$> sound x∈p ⊛′ ∣-left (<$> sound xs∈p)
  sound (∥ˡ x∈p₁)      = ∣-left {x = (-, _)} (<$> sound x∈p₁)
  sound (∥ʳ x∈p₂)      = ∣-right [] (sound x∈p₂)
  sound between-[]     = <$> Tok.complete
  sound (between-∷ {ts = _ ∷ _} x∈p xs∈⋯) =
    [ ○ - ◌ ] [ ○ - ◌ ] <$> Tok.complete ⊛′ sound x∈p ⊛′ sound xs∈⋯

  complete : ∀ {R x s} (p : ParserProg R) →
             x ∈ ⟦ p ⟧ · s → x ∈⟦ p ⟧· s
  complete fail      ()

  complete (p₁ ∣ p₂) (∣-left      x∈p₁) = ∣ˡ (complete p₁ x∈p₁)
  complete (p₁ ∣ p₂) (∣-right .[] x∈p₂) = ∣ʳ (complete p₂ x∈p₂)

  complete (p₁ ⊛  p₂) (f∈p₁ ⊛ y∈p₂) = complete    p₁  f∈p₁ ⊛  complete    p₂  y∈p₂
  complete (p₁ ⊛∞ p₂) (f∈p₁ ⊛ y∈p₂) = complete (♭ p₁) f∈p₁ ⊛∞ complete (♭ p₂) y∈p₂

  complete (f <$> p) (<$> x∈p) = <$> complete p x∈p

  complete (p +) (<$> x∈p ⊛ ∣-left (<$> xs∈p+)) =
    +-∷ (complete p x∈p) (complete (p +) xs∈p+)
  complete (p +) (_⊛_ {s₁ = s} (<$> x∈p) (∣-right .[] return)) =
    P.subst (λ s → _ ∈⟦ p + ⟧· s)
            (P.sym (proj₂ LM.identity s))
            (+-[] (complete p x∈p))

  complete (p between (t ∷ [])) (<$> t∈) with Tok.sound t t∈
  ... | (refl , refl) = between-[]
  complete (p between (t ∷ t′ ∷ ts)) (<$> t∈ ⊛ x∈p ⊛ xs∈)
    with Tok.sound t t∈
  ... | (refl , refl) =
    between-∷ (complete (♭ p) x∈p) (complete (p between (t′ ∷ ts)) xs∈)

  complete (p₁ ∥ p₂) (∣-left (<$> x∈p₁)) = ∥ˡ (complete p₁ x∈p₁)
  complete (p₁ ∥ p₂) (∣-right .[] x∈p₂)  = ∥ʳ (complete p₂ x∈p₂)

------------------------------------------------------------------------
-- A variant of the semantics

-- The alternative semantics defined below may be slightly harder to
-- understand, but it is (language) equivalent to the one above, and
-- it simplifies the proof in Mixfix.Cyclic.Show.

module Semantics-⊕ where

  open import TotalParserCombinators.Semantics.Continuation as ContSem
    hiding (sound; complete)

  infix  60 <$>_
  infixl 50 _⊛_ _⊛∞_
  infix  4  _⊕_∈⟦_⟧·_

  data _⊕_∈⟦_⟧·_ : ∀ {R} →
                   R → List NamePart →
                   ParserProg R → List NamePart → Set₁ where
    ∣ˡ         : ∀ {R x s s₁}
                   {p₁ : ParserProg R} {p₂ : ParserProg R}
                 (x∈p₁ : x ⊕ s₁ ∈⟦ p₁ ⟧· s) → x ⊕ s₁ ∈⟦ p₁ ∣ p₂ ⟧· s
    ∣ʳ         : ∀ {R x s s₁}
                   {p₁ : ParserProg R} {p₂ : ParserProg R}
                 (x∈p₂ : x ⊕ s₁ ∈⟦ p₂ ⟧· s) → x ⊕ s₁ ∈⟦ p₁ ∣ p₂ ⟧· s
    _⊛_        : ∀ {s s₁ s₂ R₁ R₂ f x}
                   {p₁ : ParserProg (R₁ → R₂)}
                   {p₂ : ParserProg R₁}
                 (f∈p₁ : f ⊕ s₁ ∈⟦ p₁ ⟧· s)
                 (x∈p₂ : x ⊕ s₂ ∈⟦ p₂ ⟧· s₁) →
                 f x ⊕ s₂ ∈⟦ p₁ ⊛ p₂ ⟧· s
    _⊛∞_       : ∀ {s s₁ s₂ R₁ R₂ f x}
                   {p₁ : ∞ (ParserProg (R₁ → R₂))}
                   {p₂ : ∞ (ParserProg R₁)}
                 (f∈p₁ : f ⊕ s₁ ∈⟦ ♭ p₁ ⟧· s)
                 (x∈p₂ : x ⊕ s₂ ∈⟦ ♭ p₂ ⟧· s₁) →
                 f x ⊕ s₂ ∈⟦ p₁ ⊛∞ p₂ ⟧· s
    <$>_       : ∀ {s s′ R₁ R₂ x} {f : R₁ → R₂} {p : ParserProg R₁}
                 (x∈p : x ⊕ s′ ∈⟦ p ⟧· s) → f x ⊕ s′ ∈⟦ f <$> p ⟧· s
    +-[]       : ∀ {R x s s₁} {p : ParserProg R}
                 (x∈p : x ⊕ s₁ ∈⟦ p ⟧· s) → [ x ] ⊕ s₁ ∈⟦ p + ⟧· s
    +-∷        : ∀ {R x s s₁ s₂ xs} {p : ParserProg R}
                 (x∈p : x ⊕ s₁ ∈⟦ p ⟧· s) (xs∈p : xs ⊕ s₂ ∈⟦ p + ⟧· s₁) →
                 x ∷⁺ xs ⊕ s₂ ∈⟦ p + ⟧· s
    between-[] : ∀ {R t s} {p : ∞ (ParserProg R)} →
                 [] ⊕ s ∈⟦ p between (t ∷ []) ⟧· t ∷ s
    between-∷  : ∀ {R n t x xs s s₁ s₂}
                   {p : ∞ (ParserProg R)} {ts : Vec NamePart (suc n)}
                 (x∈p : x ⊕ s₁ ∈⟦ ♭ p ⟧· s)
                 (xs∈⋯ : xs ⊕ s₂ ∈⟦ p between ts ⟧· s₁) →
                 x ∷ xs ⊕ s₂ ∈⟦ p between (t ∷ ts) ⟧· t ∷ s
    ∥ˡ         : ∀ {I i} {R : I → Set} {x s s′}
                   {p₁ : ParserProg (R i)}
                   {p₂ : ParserProg (∃ R)}
                 (x∈p₁ : x ⊕ s′ ∈⟦ p₁ ⟧· s) →
                 (-, x) ⊕ s′ ∈⟦ p₁ ∥ p₂ ⟧· s
    ∥ʳ         : ∀ {I i} {R : I → Set} {s s′ i′} {x : R i′}
                   {p₁ : ParserProg (R i)}
                   {p₂ : ParserProg (∃ R)}
                 (x∈p₂ : (-, x) ⊕ s′ ∈⟦ p₂ ⟧· s) →
                 (-, x) ⊕ s′ ∈⟦ p₁ ∥ p₂ ⟧· s

  tok-sound : ∀ t {t′ s₁ s} →
              t′ ⊕ s₁ ∈ tok t · s →
              t ≡ t′ × s ≡ t′ ∷ s₁
  tok-sound t ∈ with ContSem.sound′ ∈
  tok-sound t ∈ | (s         , refl , ∈′) with Tok.sound t ∈′
  tok-sound t ∈ | (.(t ∷ []) , refl , ∈′) | (refl , refl) = (refl , refl)

  tok-complete : ∀ {t s} → t ⊕ s ∈ tok t · t ∷ s
  tok-complete = ContSem.complete′ (_ , refl , Tok.complete)

  sound : ∀ {R x s s′} {p : ParserProg R} →
          x ⊕ s′ ∈⟦ p ⟧· s → x ⊕ s′ ∈ ⟦ p ⟧ · s
  sound (∣ˡ x∈p₁)      = ∣-left     (sound x∈p₁)
  sound (∣ʳ x∈p₂)      = ∣-right [] (sound x∈p₂)
  sound (f∈p₁ ⊛  x∈p₂) = [ ○ - ○ ] sound f∈p₁ ⊛ sound x∈p₂
  sound (f∈p₁ ⊛∞ x∈p₂) = [ ◌ - ◌ ] sound f∈p₁ ⊛ sound x∈p₂
  sound (<$> x∈p)      = <$> sound x∈p
  sound (+-[] x∈p)     = [ ○ - ◌ ] <$> sound x∈p ⊛ ∣-right [] return
  sound (+-∷ x∈p xs∈p) = [ ○ - ◌ ] <$> sound x∈p ⊛ ∣-left (<$> sound xs∈p)
  sound (∥ˡ x∈p₁)      = ∣-left {x = (-, _)} (<$> sound x∈p₁)
  sound (∥ʳ x∈p₂)      = ∣-right [] (sound x∈p₂)
  sound between-[]     = <$> tok-complete
  sound (between-∷ {ts = _ ∷ _} x∈p xs∈⋯) =
    [ ○ - ◌ ] [ ○ - ◌ ] <$> tok-complete ⊛ sound x∈p ⊛ sound xs∈⋯

  complete : ∀ {R x s s′} (p : ParserProg R) →
             x ⊕ s′ ∈ ⟦ p ⟧ · s → x ⊕ s′ ∈⟦ p ⟧· s
  complete fail      ()

  complete (p₁ ∣ p₂) (∣-left      x∈p₁) = ∣ˡ (complete p₁ x∈p₁)
  complete (p₁ ∣ p₂) (∣-right .[] x∈p₂) = ∣ʳ (complete p₂ x∈p₂)

  complete (p₁ ⊛  p₂) ([ .○ - .○ ] f∈p₁ ⊛ y∈p₂) = complete    p₁  f∈p₁ ⊛  complete    p₂  y∈p₂
  complete (p₁ ⊛∞ p₂) ([ .◌ - .◌ ] f∈p₁ ⊛ y∈p₂) = complete (♭ p₁) f∈p₁ ⊛∞ complete (♭ p₂) y∈p₂

  complete (f <$> p) (<$> x∈p) = <$> complete p x∈p

  complete (p +) ([ .○ - .◌ ] <$> x∈p ⊛ ∣-left (<$> xs∈p+)) = +-∷  (complete p x∈p) (complete (p +) xs∈p+)
  complete (p +) ([ .○ - .◌ ] <$> x∈p ⊛ ∣-right .[] return) = +-[] (complete p x∈p)

  complete (p between (t ∷ [])) (<$> t∈) with tok-sound t t∈
  ... | (refl , refl) = between-[]
  complete (p between (t ∷ t′ ∷ ts)) ([ .○ - .◌ ] [ .○ - .◌ ] <$> t∈ ⊛ x∈p ⊛ xs∈)
    with tok-sound t t∈
  ... | (refl , refl) =
    between-∷ (complete (♭ p) x∈p) (complete (p between (t′ ∷ ts)) xs∈)

  complete (p₁ ∥ p₂) (∣-left (<$> x∈p₁)) = ∥ˡ (complete p₁ x∈p₁)
  complete (p₁ ∥ p₂) (∣-right .[] x∈p₂)  = ∥ʳ (complete p₂ x∈p₂)

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


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

module Demos.AgdaBasics where

open import Level
open import Data.Nat
open import Data.String

data Bool : Type where
  false : Bool
  true  : Bool

_,not! : Bool → Bool
false ,not! = true
true  ,not! = false

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

infixr 1 if_then_else_
if_then_else_ : Bool → A → A → A
if false then true-path else false-path = false-path
if true  then true-path else false-path = true-path

natOrString : (x : Bool) → if x then ℕ else String
natOrString true  = 4
natOrString false = "false"

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module PairUnifier where

record PairUnifier {t} {T : Set t} (t₁ t₂ : T) : Set t where
  field


text:
------------------------------------------------------------------------
-- Weak bisimilarity
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --sized-types #-}

open import Prelude hiding (module W)

module Delay-monad.Alternative.Weak-bisimilarity {a} {A : Type a} where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)

open import Equivalence-relation equality-with-J
open import Function-universe equality-with-J
open import H-level equality-with-J
open import H-level.Closure equality-with-J

open import Delay-monad.Alternative
open import Delay-monad.Alternative.Equivalence
open import Delay-monad.Alternative.Partial-order
import Delay-monad.Bisimilarity as B
import Delay-monad.Partial-order as PO

infix 4 _≈_

-- Weak bisimilarity.

_≈_ : Delay A → Delay A → Type a
x ≈ y = x ∥⊑∥ y × y ∥⊑∥ x

-- Weak bisimilarity is pointwise propositional.

≈-propositional : ∀ x y → Is-proposition (x ≈ y)
≈-propositional x y =
  ×-closure 1 (∥⊑∥-propositional x y) (∥⊑∥-propositional y x)

-- Weak bisimilarity is an equivalence relation.

≈-is-equivalence-relation : Is-equivalence-relation _≈_
≈-is-equivalence-relation = record
  { reflexive  = λ {x} → ∥⊑∥-reflexive x , ∥⊑∥-reflexive x
  ; symmetric  = λ { (p , q) → q , p }
  ; transitive = λ {x y z} → Σ-zip (∥⊑∥-transitive x y z)
                                   (flip (∥⊑∥-transitive z y x))
  }

-- The notion of weak bisimilarity defined here is logically
-- equivalent (via Delay⇔Delay) to the one defined for the
-- coinductive delay monad (if A is a set).

≈⇔≈ :
  Is-set A →
  ∀ x y → x ≈ y ⇔ _⇔_.to Delay⇔Delay x B.≈ _⇔_.to Delay⇔Delay y
≈⇔≈ A-set x y =
  x ∥⊑∥ y × y ∥⊑∥ x                ↝⟨ inverse (⊑⇔∥⊑∥ A-set x y ×-cong ⊑⇔∥⊑∥ A-set y x) ⟩
  x ⊑ y × y ⊑ x                    ↝⟨ ⊑⇔⊑ x y ×-cong ⊑⇔⊑ y x ⟩
  to x PO.⊑ to y × to y PO.⊑ to x  ↝⟨ inverse PO.≈⇔⊑×⊒ ⟩□
  to x B.≈ to y                    □
  where
  open _⇔_ Delay⇔Delay

≈⇔≈′ :
  Is-set A →
  ∀ {x y} → x B.≈ y ⇔ _⇔_.from Delay⇔Delay x ≈ _⇔_.from Delay⇔Delay y
≈⇔≈′ A-set {x} {y} =
  x B.≈ y                                ↝⟨ PO.≈⇔⊑×⊒ ⟩
  x PO.⊑ y × y PO.⊑ x                    ↝⟨ ⊑⇔⊑′ ×-cong ⊑⇔⊑′ ⟩
  from x ⊑ from y × from y ⊑ from x      ↝⟨ ⊑⇔∥⊑∥ A-set (from x) (from y) ×-cong ⊑⇔∥⊑∥ A-set (from y) (from x) ⟩□
  from x ∥⊑∥ from y × from y ∥⊑∥ from x  □
  where
  open _⇔_ Delay⇔Delay

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
-- This code is closely based on code due to Andy Morris.

data _≡⁰_ {A : Set} (@0 x : A) : @0 A → Set where refl : x ≡⁰ x
data _≡ʷ_ {A : Set} (@ω x : A) : @ω A → Set where refl : x ≡ʷ x

works : ∀ {A} {@0 x y : A} → x ≡⁰ y → x ≡ʷ y
works refl = refl

also-works : ∀ {A} {@0 x y : A} → x ≡⁰ y → x ≡ʷ y
also-works {x = x} refl = refl {x = x}

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-
  Definition of various kinds of categories.

  This library follows the UniMath terminology, that is:

  Concept              Ob C   Hom C  Univalence

  Precategory          Type   Type   No
  Category             Type   Set    No
  Univalent Category   Type   Set    Yes

  This file also contains
    - pathToIso : Turns a path between two objects into an isomorphism between them
    - opposite categories

-}

{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.Categories.Category where

open import Cubical.Core.Glue
open import Cubical.Foundations.Prelude

private
  variable
    ℓ ℓ' : Level

-- Precategories

record Precategory ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  -- no-eta-equality ; NOTE: need eta equality for `opop`
  field
    ob : Type ℓ
    Hom[_,_] : ob → ob → Type ℓ'
    id : ∀ x → Hom[ x , x ]
    _⋆_ : ∀ {x y z} (f : Hom[ x , y ]) (g : Hom[ y , z ]) → Hom[ x , z ]
    ⋆IdL : ∀ {x y : ob} (f : Hom[ x , y ]) → (id x) ⋆ f ≡ f
    ⋆IdR : ∀ {x y} (f : Hom[ x , y ]) → f ⋆ (id y) ≡ f
    ⋆Assoc : ∀ {u v w x} (f : Hom[ u , v ]) (g : Hom[ v , w ]) (h : Hom[ w , x ]) → (f ⋆ g) ⋆ h ≡ f ⋆ (g ⋆ h)

  -- composition: alternative to diagramatic order
  _∘_ : ∀ {x y z} (g : Hom[ y , z ]) (f : Hom[ x , y ]) → Hom[ x , z ]
  g ∘ f = f ⋆ g

open Precategory

-- Helpful syntax/notation

_[_,_] : (C : Precategory ℓ ℓ') → (x y : C .ob) → Type ℓ'
_[_,_] = Hom[_,_]

-- needed to define this in order to be able to make the subsequence syntax declaration
seq' : ∀ (C : Precategory ℓ ℓ') {x y z} (f : C [ x , y ]) (g : C [ y , z ]) → C [ x , z ]
seq' = _⋆_

infix 15 seq'
syntax seq' C f g = f ⋆⟨ C ⟩ g

-- composition
comp' : ∀ (C : Precategory ℓ ℓ') {x y z} (g : C [ y , z ]) (f : C [ x , y ]) → C [ x , z ]
comp' = _∘_

infix 16 comp'
syntax comp' C g f = g ∘⟨ C ⟩ f

-- Categories

record isCategory (C : Precategory ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
  field
    isSetHom : ∀ {x y} → isSet (C [ x , y ])

-- Isomorphisms and paths in precategories

record CatIso {C : Precategory ℓ ℓ'} (x y : C .Precategory.ob) : Type ℓ' where
  constructor catiso
  field
    mor : C [ x , y ]
    inv : C [ y , x ]
    sec : inv ⋆⟨ C ⟩ mor ≡ C .id y
    ret : mor ⋆⟨ C ⟩ inv ≡ C .id x

pathToIso : {C : Precategory ℓ ℓ'} (x y : C .ob) (p : x ≡ y) → CatIso {C = C} x y
pathToIso {C = C} x y p = J (λ z _ → CatIso x z) (catiso (C .id x) idx (C .⋆IdL idx) (C .⋆IdL idx)) p
  where
    idx = C .id x

-- Univalent Categories

record isUnivalent (C : Precategory ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
  field
    univ : (x y : C .ob) → isEquiv (pathToIso {C = C} x y)

open isUnivalent public

-- Opposite Categories

_^op : Precategory ℓ ℓ' → Precategory ℓ ℓ'
(C ^op) .ob = C .ob
(C ^op) .Hom[_,_] x y = C .Hom[_,_] y x
(C ^op) .id = C .id
(C ^op) ._⋆_ f g = C ._⋆_ g f
(C ^op) .⋆IdL = C .⋆IdR
(C ^op) .⋆IdR = C .⋆IdL
(C ^op) .⋆Assoc f g h = sym (C .⋆Assoc _ _ _)

open isCategory public

-- opposite of opposite is definitionally equal to itself
involutiveOp : ∀ {C : Precategory ℓ ℓ'} → (C ^op) ^op ≡ C
involutiveOp = refl

-- Other useful operations on categories

-- whisker the parallel morphisms g and g' with f
lPrecatWhisker : {C : Precategory ℓ ℓ'} {x y z : C .ob} (f : C [ x , y ]) (g g' : C [ y , z ]) (p : g ≡ g') → f ⋆⟨ C ⟩ g ≡ f ⋆⟨ C ⟩ g'
lPrecatWhisker {C = C} f _ _ p = cong (_⋆_ C f) p


text:
open import Coinduction using ( ♭ ; ♯_ )
open import Data.Unit using ( ⊤ ; tt )
open import System.IO.Transducers.Syntax
  using ( lazy ; strict ; _⇒_is_ ; inp ; out ; done )
  renaming ( _⟫_ to _⟫'_ ; _[&]_ to _[&]'_ ; _⟨&⟩_ to _⟨&⟩'_ ;
    discard to discard' ; π₁ to π₁' ; π₂ to π₂' ;
    ⟦_⟧ to ⟦_⟧' )
open import System.IO.Transducers.Session using ( Session ; I ; Σ ; _&_ )
open import System.IO.Transducers.Trace using ( Trace )

module System.IO.Transducers.Function where

-- We can regard strict transducers as functions.
-- Note that in the case of S ⇒ T where S is a Σ session,
-- this agrees with the type of inp, so we can regard
-- inp as a function of type ∞ (S ⇒ T) → (S to T is s).

LHS : Session → Set
LHS I           = ⊤
LHS (Σ {A} V F) = A

RHS : (S T : Session) → (LHS S) → Set₁
RHS I       T a = I ⇒ T is strict
RHS (Σ V F) T a = ♭ F a ⇒ T is lazy

_⇛_ : Session → Session → Set₁
S ⇛ T = (a : LHS S) → (RHS S T a)

-- Map from functions to syntax and back.

φ : ∀ {S T} → (S ⇒ T is strict) → (S ⇛ T)
φ {I}     done    a = done
φ {Σ W F} (inp P) a = ♭ P a
φ {Σ W F} done    a = out a done

φ' : ∀ {S T} → (S ⇛ T) → (S ⇒ T is strict)
φ' {I}     P = P tt
φ' {Σ W F} P = inp (♯ P)

-- Semantics of functions is inherited from semantics on syntax

⟦_⟧ : ∀ {S T} → (S ⇛ T) → (Trace S) → (Trace T)
⟦ P ⟧ = ⟦ φ' P ⟧'

-- Structure on functions is inherited from structure on syntax

id : ∀ {S} → (S ⇛ S)
id {S} = φ (done {S})

_⟫_ : ∀ {S T U} → (S ⇛ T) → (T ⇛ U) → (S ⇛ U)
_⟫_ {S} P Q = φ (φ' {S} P ⟫' φ' Q)

_[&]_ : ∀ {S T U V} → (S ⇛ T) → (U ⇛ V) → ((S & U) ⇛ (T & V))
_[&]_ {S} P Q = φ (φ' {S} P [&]' φ' Q)

_⟨&⟩_ : ∀ {S T U} → (S ⇛ T) → (S ⇛ U) → (S ⇛ (T & U))
_⟨&⟩_ {S} P Q = φ (φ' {S} P ⟨&⟩' φ' Q)

discard : ∀ {S} → (S ⇛ I)
discard {S} = φ (discard' {S})

π₁ : ∀ {S T} → ((S & T) ⇛ S)
π₁ {S} = φ (π₁' {S})

π₂ : ∀ {S T} → ((S & T) ⇛ T)
π₂ {S} = φ (π₂' {S})

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


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

open import HoTT
open import homotopy.HSpace renaming (HSpaceStructure to HSS)
open import homotopy.Freudenthal
open import homotopy.IterSuspensionStable
open import homotopy.Pi2HSusp
open import homotopy.EM1HSpace

module homotopy.EilenbergMacLane where

-- EM(G,n) when G is π₁(A,a₀)
module EMImplicit {i} (A : Type i) (cA : is-connected ⟨0⟩ A)
  (gA : has-level ⟨ 1 ⟩ A) (A-H : HSS A)
  (μcoh : HSS.μe- A-H (HSS.e A-H) == HSS.μ-e A-H (HSS.e A-H)) where

  private
    a₀ = HSS.e A-H
    X = ⊙[ A , a₀ ]

  ⊙EM : (n : ℕ) → Ptd i
  ⊙EM O = ⊙Ω X
  ⊙EM (S n) = ⊙Trunc ⟨ S n ⟩ (⊙Susp^ n X)

  module _ (n : ℕ) where
    EM = fst (⊙EM n)
    embase = snd (⊙EM n)

  EM-level : (n : ℕ) → has-level ⟨ n ⟩ (fst (⊙EM n))
  EM-level O = gA a₀ a₀
  EM-level (S n) = Trunc-level

  EM-conn : (n : ℕ) → is-connected ⟨ n ⟩ (EM (S n))
  EM-conn n = Trunc-preserves-conn ⟨ S n ⟩
                  (transport (λ t → is-connected t (fst (⊙Susp^ n X)))
                    (nlemma n) (⊙Susp^-conn n cA))
    where nlemma : (n : ℕ) → (n -2) +2+ ⟨0⟩ == ⟨ n ⟩
          nlemma O = idp
          nlemma (S n) = ap S (nlemma n)

  {-
  π (S k) (EM (S n)) (embase (S n)) == π k (EM n) (embase n)
  where k > 0 and n = S (S n')
  -}
  module Stable (k n' : ℕ) (tk : k ≠ 0) (tsk : S k ≠ 0)
    (indexing : k ≤ S (S n'))
    where

    private
      n : ℕ
      n = S (S n')

      lte : ⟨ k ⟩ ≤T ⟨ n ⟩
      lte = ⟨⟩-monotone-≤ $ indexing

      kle : k ≤ (S n') *2
      kle = ≤-trans indexing (lemma n')
        where lemma : (n' : ℕ) → S (S n') ≤ (S n') *2
              lemma O = inl idp
              lemma (S n') = ≤-trans (≤-ap-S (lemma n')) (inr ltS)

    private
      module SS = Susp^Stable X cA (S n') k tk tsk kle

    abstract
      stable : π (S k) tsk (⊙EM (S n))
             == π k tk (⊙EM n)
      stable =
        π (S k) tsk (⊙EM (S n))
          =⟨ π-below-trunc _ tsk _ _ (≤T-ap-S lte) ⟩
        π (S k) tsk (⊙Susp^ n X)
          =⟨ SS.stable ⟩
        π k tk (⊙Susp^ (S n') X)
          =⟨ ! (π-below-trunc _ tk _ _ lte) ⟩
        π k tk (⊙EM n) ∎

  module BelowDiagonal where

    π₁ : (n : ℕ) (t1 : 1 ≠ 0 )
      → π 1 t1 (⊙EM (S (S n))) == LiftUnit-Group
    π₁ n t1 =
      contr-is-0ᴳ (π 1 t1 (⊙EM (S (S n))))
        (connected-at-level-is-contr
          (raise-level-≤T (≤T-ap-S (≤T-ap-S (-2≤T (n -2))))
                          (Trunc-level {n = ⟨0⟩}))
          (Trunc-preserves-conn ⟨0⟩ (path-conn (EM-conn (S n)))))

    -- some clutter here arises from the definition of <;
    -- any simple way to avoid this?
    π-below : (k n : ℕ) (tk : k ≠ 0) → (k < n)
      → π k tk (⊙EM n) == LiftUnit-Group
    π-below 0 _ tk lt = ⊥-rec (tk idp)
    π-below 1 .2 tk ltS = π₁ 0 tk
    π-below 1 .3 tk (ltSR ltS) = π₁ 1 tk
    π-below 1 (S (S n)) tk (ltSR (ltSR _)) = π₁ n tk
    π-below (S (S k)) ._ tssk ltS =
      Stable.stable (S k) k (ℕ-S≠O k) tssk (inr ltS)
      ∙ π-below (S k) _ (ℕ-S≠O k) ltS
    π-below (S (S k)) ._ tssk (ltSR ltS) =
      Stable.stable (S k) (S k) (ℕ-S≠O k) tssk (inr (ltSR ltS))
      ∙ π-below (S k) _ (ℕ-S≠O k) (ltSR ltS)
    π-below (S (S k)) ._ tssk (ltSR (ltSR ltS)) =
      Stable.stable (S k) (S (S k)) (ℕ-S≠O k) tssk (inr (ltSR (ltSR ltS)))
      ∙ π-below (S k) _ (ℕ-S≠O k) (ltSR (ltSR ltS))
    π-below (S (S k)) (S (S (S n))) tssk (ltSR (ltSR (ltSR lt))) =
      Stable.stable (S k) n (ℕ-S≠O k) tssk
        (inr (<-cancel-S (ltSR (ltSR (ltSR lt)))))
      ∙ π-below (S k) _ (ℕ-S≠O k) (<-cancel-S (ltSR (ltSR (ltSR lt))))

  module OnDiagonal where

    π₁ : (tn : 1 ≠ O) (t1 : 1 ≠ O)
      → π 1 tn (⊙EM 1) == π 1 t1 X
    π₁ tn t1 =
      π-below-trunc 1 tn ⟨ 1 ⟩ X ≤T-refl
      ∙ ap (λ t → π 1 t X)
           (prop-has-all-paths (Π-level (λ _ → ⊥-is-prop)) tn t1)

    private
      module Π₂ = Pi2HSusp A gA cA A-H μcoh

    π₂ : (tn : 2 ≠ O) (t1 : 1 ≠ O)
      → π 2 tn (⊙EM 2) == π 1 t1 X
    π₂ tn t1 =
      π-below-trunc 2 tn ⟨ 2 ⟩ (⊙Susp X) ≤T-refl
      ∙ Π₂.π₂-Suspension t1 tn

    π-diag : (n : ℕ) (tn : n ≠ 0) (t1 : 1 ≠ O)
      → π n tn (⊙EM n) == π 1 t1 X
    π-diag 0 tn _ = ⊥-rec (tn idp)
    π-diag 1 tn t1 = π₁ tn t1
    π-diag 2 tn t1 = π₂ tn t1
    π-diag (S (S (S n))) tn t1 =
      Stable.stable (S (S n)) n (ℕ-S≠O _) tn ≤-refl
      ∙ π-diag (S (S n)) (ℕ-S≠O _) t1

  module AboveDiagonal where

    π-above : (k n : ℕ) (tk : k ≠ 0) → (n < k)
      → π k tk (⊙EM n) == LiftUnit-Group
    π-above k n tk lt =
      contr-is-0ᴳ (π k tk (⊙EM n))
        (inhab-prop-is-contr
          [ idp^ k ]
          (Trunc-preserves-level ⟨0⟩ (Ω^-level-in ⟨-1⟩ k _
            (raise-level-≤T (lemma lt) (EM-level n)))))
      where lemma : {k n : ℕ} → n < k → S (S (n -2)) ≤T ((k -2) +2+ ⟨-1⟩)
            lemma ltS = inl (! (+2+-comm _ ⟨-1⟩))
            lemma (ltSR lt) = ≤T-trans (lemma lt) (inr ltS)

  module Spectrum where

    private
      module Π₂ = Pi2HSusp A gA cA A-H μcoh

    spectrum0 : ⊙Ω (⊙EM 1) == ⊙EM 0
    spectrum0 =
      ⊙Ω (⊙EM 1)
        =⟨ ⊙ua (Trunc=-equiv _ _) idp ⟩
      ⊙Trunc ⟨ 0 ⟩ (⊙Ω X)
        =⟨ ⊙ua (unTrunc-equiv _ (gA a₀ a₀)) idp ⟩
      ⊙Ω X ∎

    spectrum1 : ⊙Ω (⊙EM 2) == ⊙EM 1
    spectrum1 =
      ⊙Ω (⊙EM 2)
        =⟨ ⊙ua (Trunc=-equiv _ _) idp ⟩
      ⊙Trunc ⟨ 1 ⟩ (⊙Ω (⊙Susp X))
        =⟨ Π₂.⊙main-lemma ⟩
      X
        =⟨ ! (⊙ua (unTrunc-equiv _ gA) idp) ⟩
      ⊙EM 1 ∎

    private
      nlemma : (n : ℕ) → Path {A = ℕ₋₂} (S ((n -2) +2+ ⟨0⟩)) (S (S (n -1)))
      nlemma O = idp
      nlemma (S n) = ap S (nlemma n)

      sconn : (n : ℕ) → is-connected (S (S (n -1))) (fst (⊙Susp^ (S n) X))
      sconn n = transport (λ t → is-connected t (fst (⊙Susp^ (S n) X)))
                          (nlemma n) (⊙Susp^-conn (S n) cA)

      kle : (n : ℕ) → ⟨ S (S n) ⟩ ≤T S ((n -1) +2+ S (n -1))
      kle O = inl idp
      kle (S n) = ≤T-trans (≤T-ap-S (kle n))
                   (≤T-trans (inl (! (+2+-βr (S n -1) (S n -1))))
                               (inr ltS))

      module FS (n : ℕ) =
        FreudenthalEquiv (n -1) (⟨ S (S n) ⟩) (kle n)
          (fst (⊙Susp^ (S n) X)) (snd (⊙Susp^ (S n) X)) (sconn n)

    spectrumSS : (n : ℕ)
      → ⊙Ω (⊙EM (S (S (S n)))) == ⊙EM (S (S n))
    spectrumSS n =
      ⊙Ω (⊙EM (S (S (S n))))
        =⟨ ⊙ua (Trunc=-equiv _ _) idp ⟩
      ⊙Trunc ⟨ S (S n) ⟩ (⊙Ω (⊙Susp^ (S (S n)) X))
        =⟨ ! (FS.⊙path n) ⟩
      ⊙EM (S (S n)) ∎

    abstract
      spectrum : (n : ℕ) → ⊙Ω (⊙EM (S n)) == ⊙EM n
      spectrum 0 = spectrum0
      spectrum 1 = spectrum1
      spectrum (S (S n)) = spectrumSS n

module EMExplicit {i} (G : Group i) (G-abelian : is-abelian G) where
  module K₁ = EM₁ G
  module HSpace = EM₁HSpace G G-abelian
  open EMImplicit K₁.EM₁ K₁.EM₁-conn K₁.emlevel HSpace.H-EM₁ HSpace.μcoh public

  open BelowDiagonal public using (π-below)

  π-diag : (n : ℕ) (tn : n ≠ 0) → π n tn (⊙EM n) == G
  π-diag n tn =
    OnDiagonal.π-diag n tn (ℕ-S≠O 0) ∙ K₁.π₁.π₁-iso

  open AboveDiagonal public using (π-above)
  open Spectrum public using (spectrum)

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
------------------------------------------------------------------------
-- An example
------------------------------------------------------------------------

module RecursiveTypes.Subtyping.Example where

open import Codata.Musical.Notation
open import Data.Fin
open import Data.Nat

open import RecursiveTypes.Syntax
open import RecursiveTypes.Subtyping.Semantic.Coinductive

-- σ = μX. X ⟶ X.

σ : Ty 0
σ = μ var zero ⟶ var zero

-- τ = μX. (X ⟶ ⊥) ⟶ ⊤.

τ : Ty 0
τ = μ (var zero ⟶ ⊥) ⟶ ⊤

-- σ is a subtype of τ.

σ≤τ : σ ≤Coind τ
σ≤τ = ♯ (♯ σ≤τ ⟶ ♯ ⊥) ⟶ ♯ ⊤

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
module Sigma.Subst.Properties where

open import Data.Nat using (ℕ; _+_; zero; suc)
open import Data.Fin using (Fin; zero; suc)

open import Sigma.Subst.Core
open import Sigma.Renaming.Base

open import Function using (_∘_)

open import Data.Product using (∃₂; _×_) renaming ( _,_ to ⟨_,_⟩ )

open import Relation.Binary.PropositionalEquality as Eq
  using (_≡_; refl; sym; trans; cong; cong₂; cong-app)
open Eq.≡-Reasoning

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

-- We require a restricted form of functional extensionality
-- to prove whether to subsitutions are equivalent

postulate
  extensionality : ∀ { T U : Set } { f g : T → U }
    → (∀ (x : T) → f x ≡ g x)
    → f ≡ g

-- ------------------------------------------------------------------------
-- Expansion law
-- ------------------------------------------------------------------------

expansion : ∀ { T } ( σ₁ σ₂ : Sub T 0 )
  → σ₁ ≡ σ₂
expansion σ₁ σ₂ = extensionality λ ()

-- ------------------------------------------------------------------------
-- ∷-laws
-- ------------------------------------------------------------------------
-- Also known as the Interaction laws

∷-cong : ∀ { n } { T } { x₁ x₂ : T } { σ₁ σ₂ : Sub T n }
  → x₁ ≡ x₂
  → σ₁ ≡ σ₂
  -- ----------------
  → x₁ ∷ σ₁ ≡ x₂ ∷ σ₂
∷-cong x₁≡x₂ σ₁≡σ₂ = cong₂ (_∷_) x₁≡x₂ σ₁≡σ₂

∷-head : ∀ { n } { T } { x : T } { σ : Sub T n }
  → head (x ∷ σ) ≡ x
∷-head = refl

∷-tail : ∀ { n } { T } { x : T } { σ : Sub T n }
  → tail (x ∷ σ) ≡ σ
∷-tail = refl

∷-uncons : ∀ { n } { T } { x : T } { σ : Sub T n }
  → uncons (x ∷ σ) ≡ ⟨ x , σ ⟩
∷-uncons = refl

∷-head-tail-id : ∀ { n } { T } ( σ : Sub T (1 + n) )
  → head σ ∷ tail σ ≡ σ
∷-head-tail-id σ = extensionality lemma
  where
    lemma : ∀ x → (head σ ∷ tail σ) x ≡ σ x
    lemma zero = refl
    lemma (suc x) = refl

∷-id-η : ∀ { n } → ( zero ∷ ↑ ) ≡ id { n = 1 + n }
∷-id-η = ∷-head-tail-id id

∷-∘-distrib : ∀ { n } { T U } { x : T } ( σ : Sub T n ) ( f : T → U )
  → f ∘ ( x ∷ σ ) ≡ f x ∷ f ∘ σ
∷-∘-distrib { x = x } σ f = extensionality lemma
  where
    lemma : ∀ y → (f ∘ (x ∷ σ)) y ≡ ( f x ∷ (f ∘ σ) ) y
    lemma zero = refl
    lemma (suc y) = refl

∃-split : ∀ { n } { T } ( σ₁ : Sub T (1 + n) )
  → ∃₂ λ ( x : T ) ( σ₂ : Sub T n ) → σ₁ ≡ x ∷ σ₂
∃-split σ = ⟨ head σ , ⟨ tail σ , sym (∷-head-tail-id σ) ⟩ ⟩

-- TODO: Prove these.
-- x₁ ≡ head (x₁ ∷ σ₁) ::-head
--    ≡ head (x₂ ∷ σ₂) cong
--    ≡ x₂             ::-head

postulate
  ∷-injectiveˡ : ∀ { n } { T } ( x₁ x₂ : T ) ( σ₁ σ₂ : Sub T n )
    → x₁ ∷ σ₁ ≡ x₁ ∷ σ₂ → x₁ ≡ x₂

  ∷-injectiveʳ : ∀ { n } { T } ( x₁ x₂ : T ) ( σ₁ σ₂ : Sub T n )
    → x₁ ∷ σ₁ ≡ x₁ ∷ σ₂ → σ₁ ≡ σ₂

∷-injective : ∀ { n } { T } ( x₁ x₂ : T ) ( σ₁ σ₂ : Sub T n )
  → x₁ ∷ σ₁ ≡ x₁ ∷ σ₂ → (x₁ ≡ x₂) × (σ₁ ≡ σ₂)
∷-injective x₁ x₂ σ₁ σ₂ x₁∷σ₁≡x₁∷σ₂ = ⟨ (∷-injectiveˡ x₁ x₂ σ₁ σ₂ x₁∷σ₁≡x₁∷σ₂) , (∷-injectiveʳ x₁ x₂ σ₁ σ₂ x₁∷σ₁≡x₁∷σ₂) ⟩

-- ------------------------------------------------------------------------
-- Coincidence laws
-- ------------------------------------------------------------------------
-- Equivalences between uni and multi-variate primitives

++-∷ : ∀ { n } { T } (x : T) (σ : Sub T n)
  → x ∷ σ ≡ [ x ] ++ σ
++-∷ x σ = refl

-- ------------------------------------------------------------------------
-- Multi-variate interaction laws
-- ------------------------------------------------------------------------

++-cong : ∀ { m n } { T } {σ₁¹ σ₁² : Sub T m} {σ₂¹ σ₂² : Sub T n}
  → σ₁¹ ≡ σ₁²
  → σ₂¹ ≡ σ₂²
  -- -----------------------
  → σ₁¹ ++ σ₂¹ ≡ σ₁² ++ σ₂²
++-cong refl refl = refl

-- TODO: ++-injective
-- TODO: ++-≥ and ++-<

∷-drop : ∀ { m n } { T } (x : T) (σ : Sub T (m + n))
  → drop (suc m) (x ∷ σ) ≡ drop m σ
∷-drop x σ = extensionality (lemma x σ)
  where
    lemma : ∀ { m n } { T } (x : T) (σ : Sub T (m + n))
      → ∀ y → drop (suc m) (x ∷ σ) y ≡ drop m σ y
    lemma {zero} x σ y = refl
    lemma {suc m} x σ y = refl

++-drop : ∀ { m n : ℕ } { T } (σ₁ : Sub T m) (σ₂ : Sub T n)
  → drop m (σ₁ ++ σ₂) ≡ σ₂
++-drop σ₁ σ₂ = extensionality (lemma σ₁ σ₂)
  where
    lemma : ∀ { m n } { T } (σ₁ : Sub T m) (σ₂ : Sub T n)
      → ∀ x → drop m (σ₁ ++ σ₂) x ≡ σ₂ x
    lemma {zero} σ₁ σ₂ x = refl
    lemma {suc m} σ₁ σ₂ x = lemma (σ₁ ∘ ↑) σ₂ x

∷-take : ∀ { m n } { T } (x : T) (σ : Sub T (m + n))
  → take (suc m) (x ∷ σ) ≡ x ∷ take m σ
∷-take x σ = extensionality (lemma x σ)
  where
    lemma : ∀ { m n } { T } (x : T) (σ : Sub T (m + n))
      → ∀ y → take (suc m) (x ∷ σ) y ≡ (x ∷ take m σ) y
    lemma x σ zero = refl
    lemma x σ (suc y) = refl

++-take : ∀ { m n } { T } (σ₁ : Sub T m) (σ₂ : Sub T n)
  → take m (σ₁ ++ σ₂) ≡ σ₁
++-take σ₁ σ₂ = extensionality (lemma σ₁ σ₂)
  where
    lemma : ∀ { m n } { T } (σ₁ : Sub T m) (σ₂ : Sub T n)
      → ∀ x → take m (σ₁ ++ σ₂) x ≡ σ₁ x
    lemma σ₁ σ₂ zero = refl
    lemma σ₁ σ₂ (suc x) = lemma (σ₁ ∘ ↑) σ₂ x

++-take-drop-id : ∀ m { n } { T } (σ : Sub T (m + n))
  → take m σ ++ drop m σ ≡ σ
++-take-drop-id m σ = extensionality (lemma m σ)
  where
    lemma : ∀ m { n } { T } (σ : Sub T (m + n))
      → ∀ x → (take m σ ++ drop m σ) x ≡ σ x
    lemma zero σ x = refl
    lemma (suc m) σ zero = refl
    lemma (suc m) σ (suc x) = lemma m (σ ∘ ↑) x

∃-splitAt : ∀ m { n } { T } ( σ : Sub T (m + n) )
  → ∃₂ λ ( σ₁ : Sub T m ) ( σ₂ : Sub T n ) → σ ≡ σ₁ ++ σ₂
∃-splitAt m σ = ⟨ take m σ , ⟨ drop m σ , sym (++-take-drop-id m σ) ⟩ ⟩

take-∘-distrib : ∀ m { n } { T U } (σ : Sub T (m + n)) (f : T → U)
  → take m (f ∘ σ) ≡ f ∘ (take m σ)
take-∘-distrib m σ f = extensionality (lemma m σ f)
  where
    lemma : ∀ m { n } { T U } (σ : Sub T (m + n)) (f : T → U)
      → ∀ x → take m (f ∘ σ) x ≡ (f ∘ (take m σ)) x
    lemma .(suc _) σ f zero = refl
    lemma .(suc _) σ f (suc x) = refl

drop-∘-distrib : ∀ m { n } { T U } (σ : Sub T (m + n)) (f : T → U)
  → drop m (f ∘ σ) ≡ f ∘ (drop m σ)
drop-∘-distrib m σ f = extensionality (lemma m σ f)
  where
    lemma : ∀ m { n } { T U } (σ : Sub T (m + n)) (f : T → U)
      → ∀ x → drop m (f ∘ σ) x ≡ (f ∘ (drop m σ)) x
    lemma zero σ f x = refl
    lemma (suc m) σ f x = refl

++-∘-distrib : ∀ { m n } { T U } (σ₁ : Sub T m) (σ₂ : Sub T n) (f : T → U)
  → f ∘ ( σ₁ ++ σ₂ ) ≡ (f ∘ σ₁) ++ (f ∘ σ₂)
++-∘-distrib { m } σ₁ σ₂ f =
  let σ = σ₁ ++ σ₂ in
  begin
    f ∘ σ
  ≡⟨ sym (++-take-drop-id m (f ∘ σ)) ⟩
    take m (f ∘ σ) ++ drop m (f ∘ σ)
  ≡⟨ cong₂ _++_ (take-∘-distrib m σ f) (drop-∘-distrib m σ f) ⟩
    f ∘ (take m σ) ++ f ∘ (drop m σ)
  ≡⟨ cong₂ (λ σ₁ σ₂ → f ∘ σ₁ ++ f ∘ σ₂) (++-take σ₁ σ₂) (++-drop σ₁ σ₂) ⟩
    (f ∘ σ₁) ++ (f ∘ σ₂)
  ∎

-- ------------------------------------------------------------------------
-- Sub↔Vec
-- ------------------------------------------------------------------------
-- TODO

max_stars_repo_name: johnyob/agda-sigma

max_issues_repo_name: johnyob/agda-sigma

max_forks_repo_name: johnyob/agda-sigma


text:
------------------------------------------------------------------------
-- Parsing of mixfix operators
------------------------------------------------------------------------

-- This module defines a grammar for the precedence graph g.

open import Mixfix.Expr

module Mixfix.Cyclic.Grammar
         (i : PrecedenceGraphInterface)
         (g : PrecedenceGraphInterface.PrecedenceGraph i)
         where

open import Codata.Musical.Notation
open import Function using (flip; _$_)
open import Data.List using (List; []; _∷_)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.Product
import Relation.Binary.PropositionalEquality as P

open PrecedenceCorrect i g

import TotalParserCombinators.Parser as Parser
open import Mixfix.Fixity
open import Mixfix.Operator
open import Mixfix.Cyclic.Lib renaming (ParserProg to Parser)

-- The following definition uses a lexicographic combination of
-- guarded corecursion and structural recursion.

mutual

  -- Expressions.

  expr : ∞ (Parser (Expr anyPrecedence))
  expr = ♯ precs anyPrecedence

  -- Expressions corresponding to zero or more nodes in the precedence
  -- graph: operator applications where the outermost operator has one
  -- of the precedences ps. The graph g is used for internal
  -- expressions.

  precs : (ps : List Precedence) → Parser (Expr ps)
  precs []       = fail
  precs (p ∷ ps) = (λ e → here P.refl ∙ proj₂ e) <$> prec p
                 ∣ weakenE                       <$> precs ps

  -- Expressions corresponding to one node in the precedence graph:
  -- operator applications where the outermost operator has
  -- precedence p. The graph g is used for internal expressions.

  -- The code would be more readable if the delay constructors (♯_)
  -- could be omitted.

  prec : (p : Precedence) → Parser (∃ (ExprIn p))
  prec p = closedOps ∥ nonAssoc ∥ preRight⁺ ∥ postLeft⁺ ∥ fail
    module Prec where
    -- [ fix ] parses the internal parts of operators with the
    -- current precedence level and fixity fix.
    [_] = λ (fix : Fixity) → inner (ops p fix)

    -- Operator applications where the outermost operator binds
    -- tighter than the current precedence level.
    p↑ = precs (↑ p)

    -- Closed operators.
    closedOps : Parser (ExprIn p non)
    closedOps = ⟪_⟫ <$> [ closed ]

    -- Non-associative infix operators.
    nonAssoc : Parser (ExprIn p non)
    nonAssoc = ♯ (_⟨_⟩_ <$> p↑ ⊛ [ infx non ]) ⊛∞ ♯ p↑

    -- Right associative and prefix operators.
    preRight : Parser (Outer p right → ExprIn p right)
    preRight =  ⟪_⟩_  <$>      [ prefx      ]
             ∣ _⟨_⟩ʳ_ <$> p↑ ⊛ [ infx right ]

    preRight⁺ : Parser (ExprIn p right)
    preRight⁺ = ♯ preRight
                ⊛∞
                ♯ (similar <$> preRight⁺ ∣ tighter <$> p↑)

    -- Left associative and postfix operators.
    postLeft : Parser (Outer p left → ExprIn p left)
    postLeft = (λ op    e₁ → e₁ ⟨ op ⟫    ) <$> [ postfx    ]
             ∣ (λ op e₂ e₁ → e₁ ⟨ op ⟩ˡ e₂) <$> [ infx left ] ⊛ p↑

    postLeft⁺ : Parser (ExprIn p left)
    postLeft⁺ = ♯ (flip _$_ <$> ( similar <$> postLeft⁺
                                ∣ tighter <$> p↑
                                ))
                ⊛∞
                ♯ postLeft

  -- Internal parts (all name parts plus internal expressions) of
  -- operators of the given precedence and fixity.

  inner : ∀ {fix} (ops : List (∃ (Operator fix))) →
          Parser (Inner ops)
  inner []               = fail
  inner ((_ , op) ∷ ops) =
      (λ args → here P.refl ∙ args) <$> (expr between nameParts op)
    ∣ weakenI                       <$> inner ops

-- Expression parsers.

expression : Parser.Parser NamePart (Expr anyPrecedence) []
expression = ⟦ ♭ expr ⟧


text:
{-
This second-order equational theory was created from the following second-order syntax description:

syntax PCF

type
  N   : 0-ary
  _↣_ : 2-ary | r30
  B   : 0-ary

term
  app : α ↣ β  α  ->  β | _$_ l20
  lam : α.β  ->  α ↣ β | ƛ_ r10
  tr  : B
  fl  : B
  ze  : N
  su  : N  ->  N
  pr  : N  ->  N
  iz  : N  ->  B | 0?
  if  : B  α  α  ->  α
  fix : α.α  ->  α

theory
  (ƛβ) b : α.β  a : α |> app (lam(x.b[x]), a) = b[a]
  (ƛη) f : α ↣ β      |> lam (x. app(f, x))   = f
  (zz)       |> iz (ze)       = tr
  (zs) n : N |> iz (su (n)) = fl
  (ps) n : N |> pr (su (n)) = n
  (ift) t f : α |> if (tr, t, f) = t
  (iff) t f : α |> if (fl, t, f) = f
  (fix) t : α.α |> fix (x.t[x]) = t[fix (x.t[x])]
-}

module PCF.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import PCF.Signature
open import PCF.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution PCF:Syn
open import SOAS.Metatheory.SecondOrder.Equality PCF:Syn

private
  variable
    α β γ τ : PCFT
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ PCF) α Γ → (𝔐 ▷ PCF) α Γ → Set where
  ƛβ  : ⁅ α ⊩ β ⁆ ⁅ α ⁆̣ ▹ ∅ ⊢ (ƛ 𝔞⟨ x₀ ⟩) $ 𝔟 ≋ₐ 𝔞⟨ 𝔟 ⟩
  ƛη  : ⁅ α ↣ β ⁆̣       ▹ ∅ ⊢      ƛ (𝔞 $ x₀) ≋ₐ 𝔞
  zz  : ⁅⁆              ▹ ∅ ⊢           0? ze ≋ₐ tr
  zs  : ⁅ N ⁆̣           ▹ ∅ ⊢       0? (su 𝔞) ≋ₐ fl
  ps  : ⁅ N ⁆̣           ▹ ∅ ⊢       pr (su 𝔞) ≋ₐ 𝔞
  ift : ⁅ α ⁆ ⁅ α ⁆̣     ▹ ∅ ⊢       if tr 𝔞 𝔟 ≋ₐ 𝔞
  iff : ⁅ α ⁆ ⁅ α ⁆̣     ▹ ∅ ⊢       if fl 𝔞 𝔟 ≋ₐ 𝔟
  fix : ⁅ α ⊩ α ⁆̣       ▹ ∅ ⊢   fix (𝔞⟨ x₀ ⟩) ≋ₐ 𝔞⟨ (fix (𝔞⟨ x₀ ⟩)) ⟩

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
{-

This file contains:

- Definition of propositional truncation

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.PropositionalTruncation.Base where

open import Cubical.Core.Primitives

-- Propositional truncation as a higher inductive type:

data ∥_∥ {ℓ} (A : Type ℓ) : Type ℓ where
  ∣_∣ : A → ∥ A ∥
  squash : ∀ (x y : ∥ A ∥) → x ≡ y

-- Mere existence

∃ : ∀ {ℓ ℓ'} (A : Type ℓ) (B : A → Type ℓ') → Type (ℓ-max ℓ ℓ')
∃ A B = ∥ Σ A B ∥

infix 2 ∃-syntax

∃-syntax : ∀ {ℓ ℓ'} (A : Type ℓ) (B : A → Type ℓ') → Type (ℓ-max ℓ ℓ')
∃-syntax = ∃

syntax ∃-syntax A (λ x → B) = ∃[ x ∈ A ] B


text:
-- Andreas, 2017-01-18, issue #2408

-- DLubs were not serialized, thus, there was a problem with
-- level dependent on unused values.

{-# OPTIONS --show-irrelevant #-}

-- {-# OPTIONS -v tc:20 #-}

open import Agda.Primitive

data ⊥ : Set where

data Unit : Set where
  unit : Unit

-- Argument a is unused in l
l : (u : Unit) (a : ⊥) → Level
l unit a = lzero

postulate
  u : Unit
  F : (a : ⊥) → Set (l u a)

-- checked type signature
--   F : (a : ⊥) → Set (l u a)
--   of sort  dLub Set (λ a → Set (lsuc (l u a)))

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

-- First and second species counterpoint for Frog's song
module Frog where

open import Data.Fin
open import Data.List using (List; []; _∷_; _++_; map)
open import Data.Maybe using (fromMaybe)
open import Data.Nat
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Function using (_∘_)

open import Relation.Binary.PropositionalEquality using (refl)

open import Counterpoint
open import Note
open import Music
open import MidiEvent
open import Pitch
open import Interval
open import Util

-- First species counterpoint (musical content)
first : PitchInterval
first = (c 5 , per8)

middle : List PitchInterval
middle = (d 5 , maj6) ∷ (e 5 , min6) ∷ (f 5 , maj3) ∷ (e 5 , min3) ∷ (d 5 , maj6) ∷ []

middle' : List PitchInterval
middle' = (d 5 , per8) ∷ (e 5 , min6) ∷ (f 5 , maj3) ∷ (e 5 , min3) ∷ (d 5 , maj6) ∷ []

last : PitchInterval
last = (c 5 , per8)

-- Second species counterpoint (musical content)
first2 : PitchInterval
first2 = (c 5 , per5)

middle2 : List PitchInterval2
middle2 = (d 5 , min3 , per5) ∷ (e 5 , min3 , min6) ∷ (f 5 , maj3 , aug4) ∷
          (e 5 , min6 , per1) ∷ (d 5 , min3 , maj6) ∷ []

last2 : PitchInterval
last2 = (c 5 , per8)

-- Correct first species counterpoint
fs : FirstSpecies
fs = firstSpecies first middle last refl refl refl refl

{-
-- Parallel octave example from Section 3.3; ill-typed
fs' : FirstSpecies
fs' = firstSpecies first middle' last refl refl refl refl
-}

-- Correct second species counterpoint
ss : SecondSpecies
ss = secondSpecies first2 middle2 last2 refl refl refl refl refl

-- Music as list of notes
cf cp1 cp2 : List Note
cf =
  tone whole (proj₁ (FirstSpecies.firstBar fs)) ∷
  map (tone whole ∘ proj₁ ∘ pitchIntervalToPitchPair) (FirstSpecies.middleBars fs) ++
  tone whole (proj₁ (FirstSpecies.lastBar fs)) ∷
  []

cp1 =
  tone whole ((proj₂ ∘ pitchIntervalToPitchPair) (FirstSpecies.firstBar fs)) ∷
  map (tone whole ∘ proj₂ ∘ pitchIntervalToPitchPair) (FirstSpecies.middleBars fs) ++
  tone whole ((proj₂ ∘ pitchIntervalToPitchPair) (FirstSpecies.lastBar fs)) ∷
  []

cp2 =
  rest half ∷
  (tone half ((proj₂ ∘ pitchIntervalToPitchPair) (SecondSpecies.firstBar ss))) ∷
  map (tone half ∘ proj₂ ∘ pitchIntervalToPitchPair) (expandPitchIntervals2 (SecondSpecies.middleBars ss)) ++
  tone whole ((proj₂ ∘ pitchIntervalToPitchPair) (SecondSpecies.lastBar ss)) ∷
  []

----

-- MIDI generation
piano marimba : InstrumentNumber-1
piano   = # 0
marimba = # 12

channel1 channel2 : Channel-1
channel1 = # 0
channel2 = # 1

tempo : ℕ
tempo = 120

cfVelocity cpVelocity : Velocity
cfVelocity = # 60
cpVelocity = # 30

cfTrack : MidiTrack
cfTrack = track "Cantus Firmus" piano channel1 tempo (notes→events cfVelocity cf)

cpTrack1 : MidiTrack
cpTrack1 = track "Counterpoint 1" piano channel2 tempo (notes→events cpVelocity cp1)

cfcpTracks1 : List MidiTrack
cfcpTracks1 = cpTrack1 ∷ cfTrack ∷ []

cpTrack2 : MidiTrack
cpTrack2 = track "Counterpoint 2" piano channel2 tempo (notes→events cpVelocity cp2)

cfcpTracks2 : List MidiTrack
cfcpTracks2 = cpTrack2 ∷ cfTrack ∷ []

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
open import Type

module Graph.Properties.Proofs where

open import Data.Either.Proofs
open import Functional
open import Function.Equals
open import Lang.Instance
open import Logic
open import Logic.Propositional
open import Logic.Propositional.Theorems
import      Lvl
open import Graph
open import Graph.Properties
open import Relator.Equals.Proofs.Equiv
open import Structure.Setoid.Uniqueness
open import Structure.Relator.Properties
open import Type.Properties.Singleton

module _ {ℓ₁ ℓ₂} {V : Type{ℓ₁}} (_⟶_ : Graph{ℓ₁}{ℓ₂}(V)) where
  instance
    undirect-undirected : Undirected(undirect(_⟶_))
    Undirected.reversable         undirect-undirected = intro [∨]-symmetry
    Undirected.reverse-involution undirect-undirected = intro (_⊜_.proof swap-involution)

  -- [++]-visits : ∀{ae be a₁ b₁ a₂ b₂}{e : ae ⟶ be}{w₁ : Walk(_⟶_) a₁ b₁}{w₂ : Walk(_⟶_) a₂ b₂} → (Visits(_⟶_) e w₁) ∨ (Visits(_⟶_) e w₂) → Visits(_⟶_) e (w₁ ++ w₂)

  complete-singular-is-undirected : ⦃ CompleteWithLoops(_⟶_) ⦄ → ⦃ Singular(_⟶_) ⦄ → Undirected(_⟶_)
  Undirected.reversable         complete-singular-is-undirected = intro(const (completeWithLoops(_⟶_)))
  Undirected.reverse-involution complete-singular-is-undirected = intro(singular(_⟶_))

  -- traceable-is-connected : ⦃ Traceable(_⟶_) ⦄ → Connected(_⟶_)

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:
--------------------------------------------------------------------------------
-- This is part of Agda Inference Systems

{-# OPTIONS --sized-types #-}

open import Data.Nat
open import Data.Vec
open import Data.Fin
open import Data.Product
open import Data.Sum
open import Data.Unit
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Size

open import is-lib.SInfSys
open import Examples.Lambda.Lambda

module Examples.Lambda.BigStep where

  data Value∞ : Set where
    res : Value → Value∞
    div : Value∞

  U : Set
  U = Term 0 × Value∞

  data BigStepRN : Set where
    VAL APP L-DIV R-DIV : BigStepRN

  data BigStepCoRN : Set where
    COA : BigStepCoRN

  coa-r : FinMetaRule U
  coa-r .Ctx = Term 0
  coa-r .comp t =
    [] ,
    -------------------------
    (t , div)

  val-r : FinMetaRule U
  val-r .Ctx = Value
  val-r .comp v =
    [] ,
    -------------------------
    (term v , res v)

  app-r : FinMetaRule U
  app-r .Ctx = Term 0 × Term 1 × Term 0 × Value × Value∞
  app-r .comp (t1 , t , t2 , v , v∞) =
    (t1 , res (lambda t))  ∷ (t2 , res v) ∷ (subst-0 t (term v) , v∞) ∷ [] ,
    -------------------------
    (app t1 t2 , v∞)

  l-div-r : FinMetaRule U
  l-div-r .Ctx = Term 0 × Term 0
  l-div-r .comp (t1 , t2) =
    (t1 , div) ∷ [] ,
    -------------------------
    (app t1 t2 , div)

  r-div-r : FinMetaRule U
  r-div-r .Ctx = Term 0 × Term 0 × Value
  r-div-r .comp (t1 , t2 , v) =
    (t1 , res v) ∷ (t2 , div) ∷ [] ,
    -------------------------
    (app t1 t2 , div)

  BigStepIS : IS U
  BigStepIS .Names = BigStepRN
  BigStepIS .rules VAL = from val-r
  BigStepIS .rules APP = from app-r
  BigStepIS .rules L-DIV = from l-div-r
  BigStepIS .rules R-DIV = from r-div-r

  BigStepCOIS : IS U
  BigStepCOIS .Names = BigStepCoRN
  BigStepCOIS .rules COA = from coa-r

  _⇓_ : Term 0 → Value∞ → Size → Set
  (t ⇓ v∞) i = SFCoInd⟦ BigStepIS , BigStepCOIS ⟧ (t , v∞) i

  _⇓ᵢ_ : Term 0 → Value∞ → Set
  t ⇓ᵢ v∞ = Ind⟦ BigStepIS ∪ BigStepCOIS ⟧ (t , v∞)

  {- Properties -}

  val-not-reduce⇓ : ∀{v} → ¬ (∀{i} → ((term v) ⇓ div) i)
  val-not-reduce⇓ {lambda _} bs with bs
  val-not-reduce⇓ {lambda _} bs | (sfold (VAL , _ , () , _))

  val-⇓ᵢ-≡ : ∀{v v'} → term v ⇓ᵢ res v' → v ≡ v'
  val-⇓ᵢ-≡ {lambda x} {lambda .x} (fold (inj₁ VAL , .(lambda x) , refl , _)) = refl
  val-⇓ᵢ-≡ {lambda x} {lambda x₁} (fold (inj₁ APP , _ , () , _))
  val-⇓ᵢ-≡ {v} {v'} (fold (inj₂ COA , _ , () , _))

  val-⇓-≡ : ∀{v v'} → (∀{i} → (term v ⇓ res v') i) → v ≡ v'
  val-⇓-≡ bs = val-⇓ᵢ-≡ (sfcoind-to-ind bs)

max_stars_repo_name: LcicC/inference-systems-agda

max_issues_repo_name: LcicC/inference-systems-agda

max_forks_repo_name: LcicC/inference-systems-agda


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

module Testers where

open import Prelude
open import Data.List using (List; map; _⋯_)
open import Data.List.Sugar using (liftA2)

testIso : (fns : A ↔ B) → List A → Type _
testIso (to iff fro) xs = xs ≡ map (fro ∘ to) xs

testIsoℕ : (fns : ℕ ↔ A) → ℕ → Type _
testIsoℕ fns n = testIso fns (0 ⋯ n)

testUnary : (A → B) → (A → A) → (B → B) → List A → Type _
testUnary to f g xs =
  map (to ∘ f) xs ≡ map (g ∘ to) xs

testBinary : (A → B) → (A → A → A) → (B → B → B) → List A → Type _
testBinary to f g xs =
  liftA2 (λ x y → to (f x y)) xs xs ≡ liftA2 (λ x y → g (to x) (to y)) xs xs

testUnaryℕ : (ℕ → A) → (ℕ → ℕ) → (A → A) → ℕ → Type _
testUnaryℕ to f g n = testUnary to f g (0 ⋯ n)

testBinaryℕ : (ℕ → A) → (ℕ → ℕ → ℕ) → (A → A → A) → ℕ → Type _
testBinaryℕ to f g n = testBinary to f g (0 ⋯ n)


text:
open import Data.Nat

{- This is a test line ∀ , yeah it works ≡ -}

ten : ℕ
ten = 10


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

module Data.Binary.Conversion.Fast.Properties where

open import Prelude
open import Data.Binary.Conversion
open import Data.Binary.Definition
open import Data.Binary.Increment
import Data.Binary.Conversion.Fast as F
open import Data.Binary.Conversion.Fast using (⟦_⇑⟧⟨_⟩)
open import Data.Nat.Properties
open import Data.Nat.DivMod
open import Data.Maybe.Sugar
open import Data.Maybe

tail𝔹 : 𝔹 → 𝔹
tail𝔹 0ᵇ = 0ᵇ
tail𝔹 (1ᵇ xs) = xs
tail𝔹 (2ᵇ xs) = xs

tail𝔹-inc : ∀ xs → inc (tail𝔹 (inc xs)) ≡ tail𝔹 (inc (inc (inc xs)))
tail𝔹-inc 0ᵇ = refl
tail𝔹-inc (1ᵇ xs) = refl
tail𝔹-inc (2ᵇ xs) = refl

tail-homo : ∀ n → tail𝔹 (inc ⟦ n ⇑⟧) ≡ ⟦ n ÷ 2 ⇑⟧
tail-homo n = go n ; cong ⟦_⇑⟧ (sym (div-helper-lemma 0 1 n 1))
  where
  go : ∀ n → tail𝔹 (inc ⟦ n ⇑⟧) ≡ ⟦ div-helper′ 1 n 1 ⇑⟧
  go zero = refl
  go (suc zero) = refl
  go (suc (suc n)) = sym (tail𝔹-inc ⟦ n ⇑⟧) ; cong inc (go n)

head𝔹 : 𝔹 → Maybe Bool
head𝔹 0ᵇ = nothing
head𝔹 (1ᵇ xs) = just true
head𝔹 (2ᵇ xs) = just false

head𝔹-inc : ∀ xs → head𝔹 (inc (inc (inc xs))) ≡ head𝔹 (inc xs)
head𝔹-inc 0ᵇ = refl
head𝔹-inc (1ᵇ xs) = refl
head𝔹-inc (2ᵇ xs) = refl

head𝔹-homo : ∀ n → head𝔹 (inc ⟦ n ⇑⟧) ≡ just (even n)
head𝔹-homo zero    = refl
head𝔹-homo (suc zero) = refl
head𝔹-homo (suc (suc n)) = head𝔹-inc ⟦ n ⇑⟧ ; head𝔹-homo n

open import Data.Bool.Properties
open import Data.Maybe.Properties

head-tail-cong : ∀ xs ys → head𝔹 xs ≡ head𝔹 ys → tail𝔹 xs ≡ tail𝔹 ys → xs ≡ ys
head-tail-cong 0ᵇ 0ᵇ h≡ t≡ = refl
head-tail-cong 0ᵇ (1ᵇ ys) h≡ t≡ = ⊥-elim (nothing≢just h≡)
head-tail-cong 0ᵇ (2ᵇ ys) h≡ t≡ = ⊥-elim (nothing≢just h≡)
head-tail-cong (1ᵇ xs) 0ᵇ h≡ t≡ = ⊥-elim (just≢nothing h≡)
head-tail-cong (1ᵇ xs) (1ᵇ ys) h≡ t≡ = cong 1ᵇ_ t≡
head-tail-cong (1ᵇ xs) (2ᵇ ys) h≡ t≡ = ⊥-elim (subst (bool ⊥ ⊤) (just-inj h≡) tt)
head-tail-cong (2ᵇ xs) 0ᵇ h≡ t≡ = ⊥-elim (just≢nothing h≡)
head-tail-cong (2ᵇ xs) (1ᵇ ys) h≡ t≡ = ⊥-elim (subst (bool ⊤ ⊥) (just-inj h≡) tt)
head-tail-cong (2ᵇ xs) (2ᵇ ys) h≡ t≡ = cong 2ᵇ_ t≡

div2≤ : ∀ n m → n ≤ m → n ÷ 2 ≤ m
div2≤ n m = ≤-trans (n ÷ 2) n m (div-≤ n 1)

fast-correct-helper : ∀ n w → n ≤ w → ⟦ n ⇑⟧⟨ w ⟩ ≡ ⟦ n ⇑⟧
fast-correct-helper zero    w       p = refl
fast-correct-helper (suc n) (suc w) p =
    head-tail-cong _ (inc ⟦ n ⇑⟧)
      (lemma₁ (even n) ⟦ n ÷ 2 ⇑⟧⟨ w ⟩ ; sym (head𝔹-homo n))
      (lemma₂ (even n) ⟦ n ÷ 2 ⇑⟧⟨ w ⟩ ; fast-correct-helper (n ÷ 2) w (div2≤ n w (p≤p n w p)) ; sym (tail-homo n))
  where
  lemma₁ : ∀ x xs → head𝔹 (if x then 1ᵇ xs else 2ᵇ xs) ≡ just x
  lemma₁ false xs = refl
  lemma₁ true  xs = refl

  lemma₂ : ∀ x xs → tail𝔹 (if x then 1ᵇ xs else 2ᵇ xs) ≡ xs
  lemma₂ false xs = refl
  lemma₂ true xs  = refl

fast-correct : ∀ n → F.⟦ n ⇑⟧ ≡ ⟦ n ⇑⟧
fast-correct n = fast-correct-helper n n (≤-refl n)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Homogeneously-indexed binary relations
--
-- Indexed structures are laid out in a similar manner as to those
-- in Relation.Binary. The main difference is each structure also
-- contains proofs for the lifted version of the relation.
------------------------------------------------------------------------

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

module Relation.Binary.Indexed.Homogeneous where

open import Function using (_⟨_⟩_)
open import Level using (Level; _⊔_; suc)
open import Relation.Binary as B using (_⇒_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary using (¬_)
open import Data.Product using (_,_)

------------------------------------------------------------------------
-- Publically export core definitions

open import Relation.Binary.Indexed.Homogeneous.Core public

------------------------------------------------------------------------
-- Equivalences

record IsIndexedEquivalence {i a ℓ} {I : Set i} (A : I → Set a)
                            (_≈ᵢ_ : IRel A ℓ) : Set (i ⊔ a ⊔ ℓ) where
  field
    reflᵢ  : Reflexive  A _≈ᵢ_
    symᵢ   : Symmetric  A _≈ᵢ_
    transᵢ : Transitive A _≈ᵢ_

  reflexiveᵢ : ∀ {i} → _≡_ ⟨ _⇒_ ⟩ _≈ᵢ_ {i}
  reflexiveᵢ P.refl = reflᵢ

  -- Lift properties

  reflexive : _≡_ ⇒ (Lift A _≈ᵢ_)
  reflexive P.refl i = reflᵢ

  refl : B.Reflexive (Lift A _≈ᵢ_)
  refl i = reflᵢ

  sym : B.Symmetric (Lift A _≈ᵢ_)
  sym x≈y i = symᵢ (x≈y i)

  trans : B.Transitive (Lift A _≈ᵢ_)
  trans x≈y y≈z i = transᵢ (x≈y i) (y≈z i)

  isEquivalence : B.IsEquivalence (Lift A _≈ᵢ_)
  isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }

record IndexedSetoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where
  infix 4 _≈ᵢ_ _≈_
  field
    Carrierᵢ       : I → Set c
    _≈ᵢ_           : IRel Carrierᵢ ℓ
    isEquivalenceᵢ : IsIndexedEquivalence Carrierᵢ _≈ᵢ_

  open IsIndexedEquivalence isEquivalenceᵢ public

  Carrier : Set _
  Carrier = ∀ i → Carrierᵢ i

  _≈_ : B.Rel Carrier _
  _≈_ = Lift Carrierᵢ _≈ᵢ_

  _≉_ : B.Rel Carrier _
  x ≉ y = ¬ (x ≈ y)

  setoid : B.Setoid _ _
  setoid = record
    { isEquivalence = isEquivalence
    }

------------------------------------------------------------------------
-- Decidable equivalences

record IsIndexedDecEquivalence {i a ℓ} {I : Set i} (A : I → Set a)
                               (_≈ᵢ_ : IRel A ℓ) : Set (i ⊔ a ⊔ ℓ) where
  infix 4 _≟ᵢ_
  field
    _≟ᵢ_           : Decidable A _≈ᵢ_
    isEquivalenceᵢ : IsIndexedEquivalence A _≈ᵢ_

  open IsIndexedEquivalence isEquivalenceᵢ public

record IndexedDecSetoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where
  infix 4 _≈ᵢ_
  field
    Carrierᵢ          : I → Set c
    _≈ᵢ_              : IRel Carrierᵢ ℓ
    isDecEquivalenceᵢ : IsIndexedDecEquivalence Carrierᵢ _≈ᵢ_

  open IsIndexedDecEquivalence isDecEquivalenceᵢ public

  indexedSetoid : IndexedSetoid I c ℓ
  indexedSetoid = record { isEquivalenceᵢ = isEquivalenceᵢ }

  open IndexedSetoid indexedSetoid public
    using (Carrier; _≈_; _≉_; setoid)

------------------------------------------------------------------------
-- Preorders

record IsIndexedPreorder {i a ℓ₁ ℓ₂} {I : Set i} (A : I → Set a)
                         (_≈ᵢ_ : IRel A ℓ₁) (_∼ᵢ_ : IRel A ℓ₂)
                         : Set (i ⊔ a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isEquivalenceᵢ : IsIndexedEquivalence A _≈ᵢ_
    reflexiveᵢ     : _≈ᵢ_ ⇒[ A ] _∼ᵢ_
    transᵢ         : Transitive A _∼ᵢ_

  module Eq = IsIndexedEquivalence isEquivalenceᵢ

  reflᵢ : Reflexive A _∼ᵢ_
  reflᵢ = reflexiveᵢ Eq.reflᵢ

  ∼ᵢ-respˡ-≈ᵢ : Respectsˡ A _∼ᵢ_ _≈ᵢ_
  ∼ᵢ-respˡ-≈ᵢ x≈y x∼z = transᵢ (reflexiveᵢ (Eq.symᵢ x≈y)) x∼z

  ∼ᵢ-respʳ-≈ᵢ : Respectsʳ A _∼ᵢ_ _≈ᵢ_
  ∼ᵢ-respʳ-≈ᵢ x≈y z∼x = transᵢ z∼x (reflexiveᵢ x≈y)

  ∼ᵢ-resp-≈ᵢ : Respects₂ A _∼ᵢ_ _≈ᵢ_
  ∼ᵢ-resp-≈ᵢ = ∼ᵢ-respʳ-≈ᵢ , ∼ᵢ-respˡ-≈ᵢ

  -- Lifted properties

  reflexive : Lift A _≈ᵢ_ B.⇒ Lift A _∼ᵢ_
  reflexive x≈y i = reflexiveᵢ (x≈y i)

  refl : B.Reflexive (Lift A _∼ᵢ_)
  refl i = reflᵢ

  trans : B.Transitive (Lift A _∼ᵢ_)
  trans x≈y y≈z i = transᵢ (x≈y i) (y≈z i)

  ∼-respˡ-≈ : (Lift A _∼ᵢ_) B.Respectsˡ (Lift A _≈ᵢ_)
  ∼-respˡ-≈ x≈y x∼z i = ∼ᵢ-respˡ-≈ᵢ (x≈y i) (x∼z i)

  ∼-respʳ-≈ : (Lift A _∼ᵢ_) B.Respectsʳ (Lift A _≈ᵢ_)
  ∼-respʳ-≈ x≈y z∼x i = ∼ᵢ-respʳ-≈ᵢ (x≈y i) (z∼x i)

  ∼-resp-≈ : (Lift A _∼ᵢ_) B.Respects₂ (Lift A _≈ᵢ_)
  ∼-resp-≈ = ∼-respʳ-≈ , ∼-respˡ-≈

  isPreorder : B.IsPreorder (Lift A _≈ᵢ_) (Lift A _∼ᵢ_)
  isPreorder = record
    { isEquivalence = Eq.isEquivalence
    ; reflexive     = reflexive
    ; trans         = trans
    }

record IndexedPreorder {i} (I : Set i) c ℓ₁ ℓ₂ :
                       Set (suc (i ⊔ c ⊔ ℓ₁ ⊔ ℓ₂)) where

  infix 4 _≈ᵢ_ _∼ᵢ_ _≈_ _∼_

  field
    Carrierᵢ    : I → Set c
    _≈ᵢ_        : IRel Carrierᵢ ℓ₁
    _∼ᵢ_        : IRel Carrierᵢ ℓ₂
    isPreorderᵢ : IsIndexedPreorder Carrierᵢ _≈ᵢ_ _∼ᵢ_

  open IsIndexedPreorder isPreorderᵢ public

  Carrier : Set _
  Carrier = ∀ i → Carrierᵢ i

  _≈_ : B.Rel Carrier _
  x ≈ y = ∀ i → x i ≈ᵢ y i

  _∼_ : B.Rel Carrier _
  x ∼ y = ∀ i → x i ∼ᵢ y i

  preorder : B.Preorder _ _ _
  preorder = record { isPreorder = isPreorder }

------------------------------------------------------------------------
-- Partial orders

record IsIndexedPartialOrder {i a ℓ₁ ℓ₂} {I : Set i} (A : I → Set a)
                             (_≈ᵢ_ : IRel A ℓ₁) (_≤ᵢ_ : IRel A ℓ₂) :
                             Set (i ⊔ a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isPreorderᵢ : IsIndexedPreorder A _≈ᵢ_ _≤ᵢ_
    antisymᵢ    : Antisymmetric A _≈ᵢ_ _≤ᵢ_

  open IsIndexedPreorder isPreorderᵢ public
    renaming
    ( ∼ᵢ-respˡ-≈ᵢ to ≤ᵢ-respˡ-≈ᵢ
    ; ∼ᵢ-respʳ-≈ᵢ to ≤ᵢ-respʳ-≈ᵢ
    ; ∼ᵢ-resp-≈ᵢ  to ≤ᵢ-resp-≈ᵢ
    ; ∼-respˡ-≈  to ≤-respˡ-≈
    ; ∼-respʳ-≈  to ≤-respʳ-≈
    ; ∼-resp-≈   to ≤-resp-≈
    )

  antisym : B.Antisymmetric (Lift A _≈ᵢ_) (Lift A _≤ᵢ_)
  antisym x≤y y≤x i = antisymᵢ (x≤y i) (y≤x i)

  isPartialOrder : B.IsPartialOrder (Lift A _≈ᵢ_) (Lift A _≤ᵢ_)
  isPartialOrder = record
    { isPreorder = isPreorder
    ; antisym    = antisym
    }

record IndexedPoset {i} (I : Set i) c ℓ₁ ℓ₂ :
                    Set (suc (i ⊔ c ⊔ ℓ₁ ⊔ ℓ₂)) where
  field
    Carrierᵢ        : I → Set c
    _≈ᵢ_            : IRel Carrierᵢ ℓ₁
    _≤ᵢ_            : IRel Carrierᵢ ℓ₂
    isPartialOrderᵢ : IsIndexedPartialOrder Carrierᵢ _≈ᵢ_ _≤ᵢ_

  open IsIndexedPartialOrder isPartialOrderᵢ public

  preorderᵢ : IndexedPreorder I c ℓ₁ ℓ₂
  preorderᵢ = record { isPreorderᵢ = isPreorderᵢ }

  open IndexedPreorder preorderᵢ public
    using (Carrier; _≈_; preorder)
    renaming
    (_∼_ to _≤_)

  poset : B.Poset _ _ _
  poset = record { isPartialOrder = isPartialOrder }

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.17

REL = IREL
{-# WARNING_ON_USAGE REL
"Warning: REL was deprecated in v0.17.
Please use IREL instead."
#-}
Rel = IRel
{-# WARNING_ON_USAGE Rel
"Warning: Rel was deprecated in v0.17.
Please use IRel instead."
#-}


text:
------------------------------------------------------------------------------
-- Totality properties for Tree using induction instance
------------------------------------------------------------------------------

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

module FOT.FOTC.Program.Mirror.Tree.Induction.Instances.TotalityATP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.List
open import FOTC.Program.Mirror.Forest.TotalityATP
open import FOTC.Program.Mirror.Mirror
open import FOTC.Program.Mirror.Type

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

mirror-Tree-ind-instance :
  (∀ d {ts} → Forest ts → Forest (map mirror ts) → Tree (mirror · node d ts)) →
  Forest (map mirror []) →
  (∀ {t ts} → Tree t → Tree (mirror · t) → Forest ts →
    Forest (map mirror ts) → Forest (map mirror (t ∷ ts))) →
  ∀ {t} → Tree t → Tree (mirror · t)
mirror-Tree-ind-instance = Tree-mutual-ind

postulate mirror-Tree : ∀ {t} → Tree t → Tree (mirror · t)
{-# ATP prove mirror-Tree mirror-Tree-ind-instance reverse-Forest #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Montuno where

open import Data.Fin using (#_)
open import Data.Integer using (+_)
open import Data.List using (List; _∷_; []; map; concat; _++_; replicate; zip)
open import Data.Nat using (_*_; ℕ; suc; _+_)
open import Data.Product using (_,_)
open import Function using (_∘_)

open import Note

{-
double : List Chord → List Chord
double = map (λ c → flatten (c ∷ (transposeChord (+ chromaticScaleSize) c) ∷ []))

-- add the base note of the first chord to the first chord, transposed up 2 octaves
add2octave :  List Chord → List Chord
add2octave []                        = []
add2octave cs@(chord [] ∷ _)         = cs
add2octave (c@(chord (n ∷ ns)) ∷ cs) = (appendNote (transpose (+ (chromaticScaleSize * 2)) n) c) ∷ cs

baseOctave : Chord
baseOctave = chord (map (note ∘ +_ ∘ (_* chromaticScaleSize)) (0 ∷ 1 ∷ 2 ∷ []))

makeUnit : {n : ℕ} → Scale (suc n) → (Chord → List Chord) → ScaleDegree (suc n) → List Chord
makeUnit scale f = add2octave ∘ double ∘ f ∘ relativeChordToChord ∘ triad scale ∘ (λ d → (d , octave (+ 0)))

-- TODO: See if we can use the one in Data.List
_≫=_ : {A B : Set} → List A → (A → List B) → List B
xs ≫= f = concat (map f xs)

make2 : {n : ℕ} → Scale (5 + n) → (Chord → List Chord) → ScaleDegree (5 + n) → List Chord
make2 scale f secondScaleDegree =
  let scaleDegrees = secondScaleDegree ∷ map scaleDegree (# 4 ∷ # 3 ∷ [])
  in makeUnit scale f (scaleDegree (# 0)) ++ (scaleDegrees ≫= makeUnit scale oompah) ++ (baseOctave ∷ [])

rhythm rhythma : List Duration
rhythm  = map duration (+ 2       ∷ + 1 ∷ (replicate 6 (+ 2) ++ (+ 1 ∷ [])))
rhythma = map duration (+ 1 ∷ + 1 ∷ + 1 ∷ (replicate 6 (+ 2) ++ (+ 1 ∷ [])))

ex8 ex9 ex10 : {n : ℕ} → Scale (5 + n) → List TimedChord
ex8  scale = zip (make2 scale oompah    (scaleDegree (# 3))) rhythm
ex9  scale = zip (make2 scale arpegiate (scaleDegree (# 3))) rhythm
ex10 scale = zip (make2 scale arpegiate (scaleDegree (# 1))) rhythma ++ ex8 scale
-}


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open Iso

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

flip₀₂S³ : S³ → S³
flip₀₂S³ base = base
flip₀₂S³ (surf j i i₁) = surf i₁ i j

flip₀₂S³Id : (x : S³) → flip₀₂S³ (flip₀₂S³ x) ≡ x
flip₀₂S³Id base = refl
flip₀₂S³Id (surf j i i₁) = refl

flip₀₂S³Iso : Iso S³ S³
fun flip₀₂S³Iso = flip₀₂S³
inv flip₀₂S³Iso = flip₀₂S³
rightInv flip₀₂S³Iso = flip₀₂S³Id
leftInv flip₀₂S³Iso = flip₀₂S³Id

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
open import Prelude hiding (id; erase)

module Implicits.WellTyped where

open import Data.Fin.Substitution
open import Data.Vec hiding ([_])
open import Data.List as List hiding ([_]; map)

open import Implicits.Syntax.Type
open import Implicits.Syntax.Term
open import Implicits.Syntax.Context
open import Implicits.Substitutions

module TypingRules (_⊢ᵣ_ : ∀ {ν} → ICtx ν → Type ν → Set) where
  infixl 4 _⊢_∈_

  -----------------------------------------------------------------------------
  -- typings

  data _⊢_∈_ {ν n} (K : Ktx ν n) : Term ν n → Type ν → Set where
    var : (x : Fin n) → K ⊢ var x ∈ (lookup x (proj₁ K))
    λ' : ∀ {t b} a → a ∷Γ K ⊢ t ∈ b → K ⊢ λ' a t ∈ simpl (a →' b)
    Λ : ∀ {t} {a : Type (suc ν)} → ktx-weaken K ⊢ t ∈ a → K ⊢ Λ t ∈ ∀' a
    _[_] : ∀ {t} {a : Type (suc ν)} →
           K ⊢ t ∈ ∀' a → (b : Type ν) → K ⊢ t [ b ] ∈ a tp[/tp b ]
    _·_  : ∀ {f t a b} → K ⊢ f ∈ simpl (a →' b) → K ⊢ t ∈ a → K ⊢ f · t ∈ b

    -- implicit abstract/application
    ρ : ∀ {t b a} → [] ⊢unamb a → a ∷K K ⊢ t ∈ b → K ⊢ ρ a t ∈ (a ⇒ b)
    _⟨_⟩ : ∀ {a b f} → K ⊢ f ∈ a ⇒ b → (proj₂ K) ⊢ᵣ a → K ⊢ f ⟨⟩ ∈ b
    _with'_ : ∀ {r e a b} → K ⊢ r ∈ a ⇒ b → K ⊢ e ∈ a → K ⊢ r with' e ∈ b

  _⊢_∉_ : ∀ {ν n} → (K : Ktx ν n) → Term ν n → Type ν → Set
  _⊢_∉_ K t τ = ¬ K ⊢ t ∈ τ

  -----------------------------------------------------------------------------
  -- syntactic sugar

  let'_in'_ : ∀ {ν n} {e₁ : Term ν n} {e₂ : Term ν (suc n)} {a b} {K} →
              K ⊢ e₁ ∈ a → a ∷Γ K ⊢ e₂ ∈ b → K ⊢ (let' e₁ ∶ a in' e₂) ∈ b
  let' e₁ in' e₂ = (λ' _ e₂) · e₁

  implicit'_∶_in'_ : ∀ {ν n} {e₁ : Term ν n} {e₂ : Term ν (suc n)} {a b} {K} →
              K ⊢ e₁ ∈ a → [] ⊢unamb a → a ∷K K ⊢ e₂ ∈ b → K ⊢ (implicit e₁ ∶ a in' e₂) ∈ b
  implicit' e₁ ∶ a in' e₂ = (ρ a e₂) with' e₁

  wt-¿ : ∀ {ν n} {r : Type ν} {K : Ktx ν n} → [] ⊢unamb r → (proj₂ K) ⊢ᵣ r → K ⊢ (¿ r) ∈ r
  wt-¿ r x = (ρ r (var zero)) ⟨ x ⟩

  -----------------------------------------------------------------------------
  -- utilities

  erase : ∀ {ν n} {K : Ktx ν n} {t a} → K ⊢ t ∈ a → Term ν n
  erase {t = t} _ = t

  -- Collections of typing derivations for well-typed terms.
  data _⊢ⁿ_∈_ {m n} (Γ : Ktx n m) : ∀ {k} → Vec (Term n m) k → Vec (Type n) k → Set where
    []  : Γ ⊢ⁿ [] ∈ []
    _∷_ : ∀ {t a k} {ts : Vec (Term n m) k} {as : Vec (Type n) k} →
        Γ ⊢ t ∈ a → Γ ⊢ⁿ ts ∈ as → Γ ⊢ⁿ t ∷ ts ∈ (a ∷ as)

  -- Lookup a well-typed term in a collection thereof.
  lookup-⊢ : ∀ {m n k} {Γ : Ktx n m} {ts : Vec (Term n m) k} {as : Vec (Type n) k} →
              (x : Fin k) → Γ ⊢ⁿ ts ∈ as → Γ ⊢ lookup x ts ∈ lookup x as
  lookup-⊢ zero  (⊢t ∷ ⊢ts) = ⊢t
  lookup-⊢ (suc x) (⊢t ∷ ⊢ts) = lookup-⊢ x ⊢ts


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

open import Categories.Category
open import Categories.Functor hiding (id)

-- Coimit of a Cocone over a Functor F : J → C
module Categories.Diagram.Colimit
  {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} (F : Functor J C) where

private
  module C = Category C
  module J = Category J
open C
open HomReasoning
open Functor F

open import Level
open import Data.Product using (proj₂)

open import Categories.Category.Construction.Cocones F renaming (Cocone⇒ to _⇨_)
open import Categories.Object.Initial as I hiding (up-to-iso; transport-by-iso)
open import Categories.Morphism.Reasoning C
open import Categories.Morphism C
open import Categories.Morphism Cocones as MC using () renaming (_≅_ to _⇔_)

private
  variable
    K K′  : Cocone
    A B   : J.Obj
    X Y Z : Obj
    q     : K ⇨ K′

-- A Colimit is an Initial object in the category of Cocones
--   (This could be unpacked...)
record Colimit : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  field
    initial : Initial Cocones

  module initial = Initial initial

  open initial using () renaming (⊥ to colimit) public
  open Cocone colimit hiding (coapex) renaming (N to coapex; ψ to proj; commute to colimit-commute) public

  rep-cocone : ∀ K → colimit ⇨ K
  rep-cocone K = initial.! {K}

  rep : ∀ K → coapex ⇒ Cocone.N K
  rep K = arr
    where open _⇨_ (rep-cocone K)

  unrep : coapex ⇒ X → Cocone
  unrep f = record {
    coapex        = record
      { ψ       = λ A → f ∘ proj A
      ; commute = λ g → pullʳ (colimit-commute g)
      }
    }

  coconify : (f : coapex ⇒ X) → colimit ⇨ unrep f
  coconify f = record
    { arr     = f
    ; commute = refl
    }

  commute : rep K ∘ proj A ≈ Cocone.ψ K A
  commute {K = K} = _⇨_.commute (rep-cocone K)

  unrep-cone : (colimit ⇨ K) → Cocone
  unrep-cone f = unrep (_⇨_.arr f)

  g-η : ∀ {f : coapex ⇒ X} → rep (unrep f) ≈ f
  g-η {f = f} = initial.!-unique (coconify f)

  η-cocone : Cocones [ rep-cocone colimit ≈ Category.id Cocones ]
  η-cocone = initial.⊥-id (rep-cocone colimit)

  η : rep colimit ≈ id
  η = η-cocone

  rep-cocone∘ : Cocones [ Cocones [ q ∘ rep-cocone K ] ≈ rep-cocone K′ ]
  rep-cocone∘ {K = K} {q = q} = Equiv.sym (initial.!-unique (Cocones [ q ∘ rep-cocone K ]))

  rep∘ : ∀ {q : K ⇨ K′} → _⇨_.arr q ∘ rep K ≈ rep K′
  rep∘ {q = q} = rep-cocone∘ {q = q}

  rep-cone-self-id : Cocones [ rep-cocone colimit ≈  Cocones.id  ]
  rep-cone-self-id = initial.!-unique ( Cocones.id )

  rep-self-id : rep colimit ≈ id
  rep-self-id = rep-cone-self-id

open Colimit

up-to-iso-cone : (L₁ L₂ : Colimit) → colimit L₁ ⇔ colimit L₂
up-to-iso-cone L₁ L₂ =  I.up-to-iso Cocones (initial L₁) (initial L₂)

up-to-iso : (L₁ L₂ : Colimit) → coapex L₁ ≅ coapex L₂
up-to-iso L₁ L₂ =  iso-cocone⇒iso-coapex (up-to-iso-cone L₁ L₂)

transport-by-iso-cocone : (C : Colimit) → colimit C ⇔ K → Colimit
transport-by-iso-cocone C C⇿K = record
  { initial =  I.transport-by-iso Cocones (initial C) C⇿K
  }

transport-by-iso : (C : Colimit) → coapex C ≅ X → Colimit
transport-by-iso C C≅X = transport-by-iso-cocone C (proj₂ p)
  where p = cocone-resp-iso (colimit C) C≅X

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
-- Moved from the successfull test-suite. See Issue 1481.

module tests.Nat where

data Nat : Set where
  Z : Nat
  S : Nat → Nat

{-# BUILTIN NATURAL Nat #-}

_+_ : Nat → Nat → Nat
Z   + m = m
S n + m = S (n + m)

{-# BUILTIN NATPLUS _+_ #-}

_*_ : Nat → Nat → Nat
Z   * m = Z
S n * m = m + (n * m)

{-# BUILTIN NATTIMES _*_ #-}

data Unit : Set where
  unit : Unit

postulate
  IO          : Set → Set
  String      : Set
  natToString : Nat → String
  putStr      : String → IO Unit

printNat : Nat → IO Unit
printNat n = putStr (natToString n)

{-# COMPILED_TYPE IO IO #-}

{-# COMPILED_EPIC natToString (n : Any) -> String = bigToStr(n) #-}

{-# COMPILED_EPIC putStr (a : String, u : Unit) ->
                  Unit = foreign Int "wputStr" (a : String); primUnit #-}

main : IO Unit
main = printNat (7 * 191)

-- should print 1337


text:
{-# OPTIONS --safe --warning=error #-}

open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Sets.FinSet.Definition
open import LogicalFormulae
open import Numbers.Naturals.WithK
open import Sets.FinSet.Lemmas

module Sets.FinSetWithK where

private
  sgEq : {l m : _} {L : Set l} → {pr : L → Set m} → {a b : Sg L pr} → (underlying a ≡ underlying b) → ({c : L} → (r s : pr c) → r ≡ s) → (a ≡ b)
  sgEq {l} {m} {L} {prop} {(a , b1)} {(.a , b)} refl pr2 with pr2 {a} b b1
  sgEq {l} {m} {L} {prop} {(a , b1)} {(.a , .b1)} refl pr2 | refl = refl

finNotEqualsRefl : {n : ℕ} {a b : FinSet (succ n)} → (p1 p2 : FinNotEquals a b) → p1 ≡ p2
finNotEqualsRefl {.1} {.fzero} {.(fsucc fzero)} (fne2 .fzero .(fsucc fzero) (inl (refl ,, refl))) (fne2 .fzero .(fsucc fzero) (inl (refl ,, refl))) = refl
finNotEqualsRefl {.1} {.fzero} {.(fsucc fzero)} (fne2 .fzero .(fsucc fzero) (inl (refl ,, refl))) (fne2 .fzero .(fsucc fzero) (inr (() ,, snd)))
finNotEqualsRefl {.1} {.(fsucc fzero)} {.fzero} (fne2 .(fsucc fzero) .fzero (inr (refl ,, refl))) (fne2 .(fsucc fzero) .fzero (inl (() ,, snd)))
finNotEqualsRefl {.1} {.(fsucc fzero)} {.fzero} (fne2 .(fsucc fzero) .fzero (inr (refl ,, refl))) (fne2 .(fsucc fzero) .fzero (inr (refl ,, refl))) = refl
finNotEqualsRefl {.(succ (succ _))} {.fzero} {.(fsucc a)} (fneN .fzero .(fsucc a) (inl (inl (refl ,, (a , refl))))) (fneN .fzero .(fsucc a) (inl (inl (refl ,, (.a , refl))))) = refl
finNotEqualsRefl {.(succ (succ _))} {.fzero} {.(fsucc a)} (fneN .fzero .(fsucc a) (inl (inl (refl ,, (a , refl))))) (fneN .fzero .(fsucc a) (inl (inr ((a₁ , ()) ,, snd))))
finNotEqualsRefl {.(succ (succ _))} {.fzero} {.(fsucc a)} (fneN .fzero .(fsucc a) (inl (inl (refl ,, (a , refl))))) (fneN .fzero .(fsucc a) (inr ((fst ,, snd) , b))) = exFalso q
  where
    p : fzero ≡ fsucc fst
    p = _&_&_.one b
    q : False
    q with p
    ... | ()
finNotEqualsRefl {.(succ (succ _))} {.(fsucc a)} {.fzero} (fneN .(fsucc a) .fzero (inl (inr ((a , refl) ,, refl)))) (fneN .(fsucc a) .fzero (inl (inl (() ,, snd))))
finNotEqualsRefl {.(succ (succ _))} {.(fsucc a)} {.fzero} (fneN .(fsucc a) .fzero (inl (inr ((a , refl) ,, refl)))) (fneN .(fsucc a) .fzero (inl (inr ((.a , refl) ,, refl)))) = refl
finNotEqualsRefl {.(succ (succ _))} {.(fsucc a)} {.fzero} (fneN .(fsucc a) .fzero (inl (inr ((a , refl) ,, refl)))) (fneN .(fsucc a) .fzero (inr ((fst ,, snd) , b))) = exFalso q
  where
    p : fzero ≡ fsucc snd
    p = _&_&_.two b
    q : False
    q with p
    ... | ()
finNotEqualsRefl {.(succ (succ _))} {a} {b} (fneN a b (inr (record { fst = fst ; snd = snd₁ } , snd))) (fneN .a .b (inl (inl (fst1 ,, snd₂)))) = exFalso q
  where
    p : fzero ≡ fsucc fst
    p = transitivity (equalityCommutative fst1) (_&_&_.one snd)
    q : False
    q with p
    ... | ()
finNotEqualsRefl {.(succ (succ _))} {a} {b} (fneN a b (inr (record { fst = fst ; snd = snd1 } , snd))) (fneN .a .b (inl (inr (fst₁ ,, snd2)))) = exFalso q
  where
    p : fzero ≡ fsucc snd1
    p = transitivity (equalityCommutative snd2) (_&_&_.two snd)
    q : False
    q with p
    ... | ()
finNotEqualsRefl {.(succ (succ _))} {.fzero} {b} (fneN fzero b (inr (record { fst = fst ; snd = snd₁ } , snd))) (fneN .fzero .b (inr ((fst1 ,, snd₂) , b1))) = exFalso q
  where
    p : fzero ≡ fsucc fst1
    p = _&_&_.one b1
    q : False
    q with p
    ... | ()
finNotEqualsRefl {.(succ (succ _))} {.(fsucc a)} {.fzero} (fneN (fsucc a) fzero (inr (record { fst = fst ; snd = snd₁ } , snd))) (fneN .(fsucc a) .fzero (inr ((fst₁ ,, snd2) , b1))) = exFalso q
  where
    p : fzero ≡ fsucc snd2
    p = _&_&_.two b1
    q : False
    q with p
    ... | ()
finNotEqualsRefl {.(succ (succ _))} {.(fsucc a)} {.(fsucc b)} (fneN (fsucc a) (fsucc b) (inr (record { fst = fst ; snd = snd1 } , snd))) (fneN .(fsucc a) .(fsucc b) (inr ((fst1 ,, snd2) , b1))) = ans
  where
    t : a ≡ fst1
    t = fsuccInjective (_&_&_.one b1)
    t' : a ≡ fst
    t' = fsuccInjective (_&_&_.one snd)
    u : b ≡ snd1
    u = fsuccInjective (_&_&_.two snd)
    u' : b ≡ snd2
    u' = fsuccInjective (_&_&_.two b1)
    equality : {c : FinSet (succ (succ _)) && FinSet (succ (succ _))} → (r1 s : (fsucc a ≡ fsucc (_&&_.fst c)) & (fsucc b ≡ fsucc (_&&_.snd c)) & FinNotEquals (_&&_.fst c) (_&&_.snd c)) → r1 ≡ s
    equality record { one = refl ; two = refl ; three = q } record { one = refl ; two = refl ; three = q' } = applyEquality (λ t → record { one = refl ; two = refl ; three = t }) (finNotEqualsRefl q q')
    r : (fst ,, snd1) ≡ (fst1 ,, snd2)
    r rewrite equalityCommutative t | equalityCommutative t' | equalityCommutative u | equalityCommutative u' = refl
    ans : fneN (fsucc a) (fsucc b) (inr ((fst ,, snd1) , snd)) ≡ fneN (fsucc a) (fsucc b) (inr ((fst1 ,, snd2) , b1))
    ans = applyEquality (λ t → fneN (fsucc a) (fsucc b) (inr t)) (sgEq r equality)


text:
------------------------------------------------------------------------------
-- Totality properties respect to ListN
------------------------------------------------------------------------------

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

module FOTC.Program.SortList.Properties.Totality.ListN-ATP where

open import FOTC.Base
open import FOTC.Data.Nat.List.Type
open import FOTC.Data.Nat.List.PropertiesATP
open import FOTC.Program.SortList.SortList

------------------------------------------------------------------------------
-- The function flatten generates a ListN.
flatten-ListN : ∀ {t} → Tree t → ListN (flatten t)
flatten-ListN tnil = prf
  where postulate prf : ListN (flatten nil)
        {-# ATP prove prf #-}
flatten-ListN (ttip {i} Ni) = prf
  where postulate prf : ListN (flatten (tip i))
        {-# ATP prove prf #-}

flatten-ListN (tnode {t₁} {i} {t₂} Tt₁ Ni Tt₂) =
  prf (flatten-ListN Tt₁) (flatten-ListN Tt₂)
  where postulate prf : ListN (flatten t₁) →
                        ListN (flatten t₂) →
                        ListN (flatten (node t₁ i t₂))


text:
module Day5 where

open import Prelude.String as String
open import Data.Maybe
open import Foreign.Haskell using (Unit)
open import Prelude.List as List
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Nat.Properties
import Data.Nat.Show as ℕs
open import Prelude.Char
open import Data.Vec as Vec renaming (_>>=_ to _VV=_ ; toList to VecToList)
open import Data.Product
open import Relation.Nullary
open import Data.Nat.Properties
open import Data.Bool.Base
open import AocIO
open import AocUtil
open import AocVec
open import Relation.Binary.PropositionalEquality
open import EvenOdd
open import Prelude.Int

unsafeParseInt : List Char → Int
unsafeParseInt ('-' ∷ ls) with (unsafeParseNat ls)
... | zero = pos zero
... | suc n = negsuc n
unsafeParseInt ls = pos (unsafeParseNat ls)

main : IO Unit
main = mainBuilder (readFileMain process-file)
  where
    process-file : String → IO Unit
    process-file file-content with lines (unpackString file-content)
    ... | file-lines with List.map unsafeParseInt file-lines
    ... | instructions with List.map (λ n → printString (primShowInteger n)) instructions
    ... | io-ops = void (sequence-io-prim io-ops)


text:
-- Andreas, 2016-01-21, issue 1791
-- With-clause stripping for copatterns with "polymorphic" field.

-- {-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.with.strip:60 #-}

postulate anything : ∀{A : Set} → A

record Wrap (A : Set) : Set where
  field unwrap : A

module VisibleWorks where

  -- monomorphic field

  record Pointed (M : Set → Set) : Set₁ where
    field point : ∀ A → M A

  test : Pointed Wrap
  Wrap.unwrap (Pointed.point test A) with Set₂
  ... | _ = anything

-- polymorphic field

record Pointed (M : Set → Set) : Set₁ where
  field point : ∀{A} → M A

module ExplicitWorks where

  test : Pointed Wrap
  Wrap.unwrap (Pointed.point test {A}) with Set₂
  ... | _ = anything

-- WAS: hidden fails

test : Pointed Wrap
Wrap.unwrap (Pointed.point test) with Set₂
... | _ = anything

-- should succeed


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.FinData.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat
open import Cubical.Relation.Nullary

data Fin : ℕ → Type₀ where
  zero : {n : ℕ} → Fin (suc n)
  suc  : {n : ℕ} (i : Fin n) → Fin (suc n)

toℕ : ∀ {n} → Fin n → ℕ
toℕ zero    = 0
toℕ (suc i) = suc (toℕ i)

fromℕ : (n : ℕ) → Fin (suc n)
fromℕ zero    = zero
fromℕ (suc n) = suc (fromℕ n)

¬Fin0 : ¬ Fin 0
¬Fin0 ()

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


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

open import bool
open import bool-thms2
open import eq
open import maybe
open import product
open import product-thms
open import bool-relations using (transitive ; total)

module z05-01-hc-sorted-list
  (A : Set)                    -- type of elements
  (_≤A_ : A → A → 𝔹)           -- ordering function
  (≤A-trans : transitive _≤A_) -- proof of transitivity of given ordering
  (≤A-total : total      _≤A_) -- proof of totality     of given ordering
  where

open import bool-relations _≤A_ hiding (transitive ; total)
open import minmax _≤A_ ≤A-trans ≤A-total

data slist : A → A → Set where
  snil  : ∀ {l u : A}
        → l ≤A u ≡ tt
        → slist l u
  scons : ∀ {l u : A}
        → (d : A)      -- value stored at head
        → slist l u    -- elements to the right ≥ stored value
        → d ≤A l ≡ tt
        → slist (min d l) (max d u)

slist-insert : ∀ {l u : A}
             → (d : A)                   -- insert 'd'
             → slist l u                 -- into this 'bst'
             → d ≤A l ≡ tt
             → slist (min d l) (max d u) -- type might change
slist-insert d (snil l≤Au) d≤Al≡tt = scons d (snil l≤Au) d≤Al≡tt

slist-insert d   (scons d' xs d'≤Al≡tt) d≤Al≡tt  with keep (d ≤A d')

slist-insert d L@(scons d' xs d'≤Al≡tt) d≤Al≡tt | tt , p = scons d L d≤Al≡tt

slist-insert d L@(scons d' xs d'≤Al≡tt) d≤Al≡tt | ff , p = {!!}

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Truncation where

open import Cubical.HITs.Truncation.Base public
open import Cubical.HITs.Truncation.Properties public

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical