text:
module TLP01 where

open import Data.Bool
open import Data.Nat
open import Data.String
open import Relation.Binary.PropositionalEquality
  as PropEq using (_≡_; refl; sym; cong; cong₂; trans)

_==ℕ_ : ℕ → ℕ → Bool
zero  ==ℕ zero  = true
suc n ==ℕ suc m = n ==ℕ m
_     ==ℕ _     = false

_<ℕ_ : ℕ → ℕ → Bool
_     <ℕ zero  = false
zero  <ℕ suc _ = true
suc n <ℕ suc m = n <ℕ m

-- ----- Star型の定義と同値性 -----
data Star : Set where
  NIL : Star
  TRU : Star
  N   : ℕ → Star
  S   : String → Star
  C   : Star → Star → Star

eqStar : Star → Star → Bool
eqStar NIL NIL = true
eqStar NIL _ = false
eqStar TRU TRU = true
eqStar TRU _ = false
eqStar (N x) (N y) = x ==ℕ y
eqStar (N _) _ = false
eqStar (S x) (S y) = x == y
eqStar (S _) _ = false
eqStar (C x x₁) (C y y₁) = eqStar x y ∧ eqStar x₁ y₁
eqStar (C _ _) _ = false

-- ----- 組込関数の定義 -----
CONS : Star → Star → Star
CONS = C

CAR : Star → Star
CAR (C x _) = x
CAR _ = NIL

CDR : Star → Star
CDR (C _ x₁) = x₁
CDR _ = NIL

ATOM : Star → Star
ATOM (C _ _) = NIL
ATOM _ = TRU

IF : Star → Star → Star → Star
IF TRU a _ = a
IF q a e = if eqStar q NIL then e else a

EQUAL : Star → Star → Star
EQUAL x y = if eqStar x y then TRU else NIL

s-size : Star → ℕ
s-size (C a b) = s-size a + s-size b + 1
s-size _ = 0
SIZE : Star → Star
SIZE x = N (s-size x)

s2n : Star → ℕ
s2n (N x) = x
s2n _ = 0
LT : Star → Star → Star
LT x y = if s2n x <ℕ s2n y then TRU else NIL

-- ----- Starから≡に -----
postulate
  ts : Star → Set
  ~ : Star → Star
  equal-eq : {x y : Star} → ts (EQUAL x y) →  x ≡ y
  ifAP : {q x y : Star} → ts (IF q (EQUAL x y) TRU) → (ts q → x ≡ y)
  ifEP : {q x y : Star} → ts (IF q TRU (EQUAL x y)) → (ts (~ q) → x ≡ y)
-- ----- 公理 -----
  equal-same : (x : Star) → ts (EQUAL x x)
  equal-swap : (x y : Star) → ts (EQUAL (EQUAL x y) (EQUAL y x))
  equal-if : (x y : Star) → ts (IF (EQUAL x y) (EQUAL x y) TRU)
  atom/cons : (x y : Star) → ts (EQUAL (ATOM (CONS x y)) NIL)
  car/cons : (x y : Star) → ts (EQUAL (CAR (CONS x y)) x)
  cdr/cons : (x y : Star) → ts (EQUAL (CDR (CONS x y)) y)
  cons/car+cdr : (x : Star)
    → ts (IF (ATOM x) TRU (EQUAL (CONS (CAR x) (CDR x)) x))
  if-true : (x y : Star) → ts (EQUAL (IF TRU x y) x)
  if-false : (x y : Star) → ts (EQUAL (IF NIL x y) y)
  if-same : (x y : Star) → ts (EQUAL (IF x y y) y)
  if-nest-A : (x y z : Star) → ts (IF x (EQUAL (IF x y z) y) TRU)
  if-nest-E : (x y z : Star) → ts (IF x TRU (EQUAL (IF x y z) z))
  size/car : (x : Star)
    → ts (IF (ATOM x) TRU (EQUAL (LT (SIZE (CAR x)) (SIZE x)) TRU))
  size/cdr : (x : Star)
    → ts (IF (ATOM x) TRU (EQUAL (LT (SIZE (CDR x)) (SIZE x)) TRU))

-- ----- 練習 -----
postulate
  -- a b : Star
  foo : ts (EQUAL TRU NIL)
hoge6 : (a b : Star)
  → (IF (EQUAL TRU NIL) TRU TRU) ≡ (IF (EQUAL TRU NIL) NIL TRU)
hoge6 a b = ifAP (equal-if TRU NIL) foo

hoge2 : (ATOM (CONS TRU TRU)) ≡ NIL
hoge2 = equal-eq (atom/cons TRU TRU)

-- hoge2' : (ATOM (CONS TRU TRU)) ≡ NIL
-- hoge2' rewrite (equal-eq (atom-cons TRU TRU)) = {!!}

hoge3 : (C TRU NIL) ≡ (C TRU NIL)
hoge3 = equal-eq (equal-same (C TRU NIL))

hoge4 : (EQUAL TRU TRU) ≡ TRU
hoge4 = begin
    (if eqStar TRU TRU then TRU else NIL)
  ≡⟨ refl ⟩
    TRU
  ∎
  where open PropEq.≡-Reasoning

hoge5 : (EQUAL NIL NIL) ≡ TRU
hoge5 = refl

postulate
  j : (x : Star) → ts (~ (ATOM x))
hoge7 : (x : ℕ)
  → (IF (ATOM (N x)) TRU (LT (SIZE (CDR (N x))) (SIZE (N x)))) ≡ (IF (ATOM (N x)) TRU TRU)
hoge7 x = ifEP (size/cdr (N x)) (j (N x))
-- -----

{-
-- ----- 停止性で引っかかる -----
memb?' : Star → Star
memb?' xs =
  (IF (ATOM xs)
       NIL
       (IF (EQUAL (CAR xs) (S "?"))
           TRU
           (memb?' (CDR xs))))
-}
-- ----- memb?の停止性 -----
-- ----- SIZEを使う時はℕを引数にとる
postulate
  premise : (xs : Star) → ts (~ (ATOM xs))
measure-memb? : (x : ℕ)
  → (IF (ATOM (N x))
        TRU
        (IF (EQUAL (CAR (N x)) (S "?"))
            TRU
            (LT (SIZE (CDR (N x))) (SIZE (N x)))))
    ≡ TRU
measure-memb? x = begin
    (IF (ATOM (N x))
        TRU
        (IF (EQUAL (CAR (N x)) (S "?"))
            TRU
            (LT (SIZE (CDR (N x))) (SIZE (N x)))))
  ≡⟨ ifEP (size/cdr (N x)) (premise (N x)) ⟩
    (IF (ATOM (N x))
        TRU
        (IF (EQUAL (CAR (N x)) (S "?"))
            TRU
            TRU))
  ≡⟨ equal-eq (if-same (EQUAL (CAR (N x)) (S "?")) TRU) ⟩
    (IF (ATOM (N x))
        TRU
        TRU)
  ≡⟨ equal-eq (if-same (ATOM (N x)) TRU) ⟩
    TRU
  ∎
  where open PropEq.≡-Reasoning

-- ----- memb?の定義 -----
postulate
  memb? : Star → Star
  def-memb? : (xs : Star) →
    memb? xs ≡
      (IF (ATOM xs)
          NIL
          (IF (EQUAL (CAR xs) (S "?"))
              TRU
              (memb? (CDR xs))))
-- ----- rembの定義 -----
postulate
  remb : Star → Star
  def-remb : (xs : Star) →
    remb xs ≡
      (IF (ATOM xs)
          (S "'()")
          (IF (EQUAL (CAR xs) (S "?"))
              (remb (CDR xs))
              (CONS (CAR xs)
                 (remb (CDR xs)))))
-- ----- 帰納的な証明(未完) -----
-- ----- ATOMを使う時はC x yを引数にとる
postulate
  premise2 : (xs : Star) → ts (ATOM xs)
atomt : (ATOM (S "'()")) ≡ TRU
atomt = refl
memb?/remb : (x y : Star)
  → (IF (ATOM (C x y))
        (EQUAL (memb? (remb (C x y))) NIL)
        (IF (EQUAL (memb? (remb (CDR (C x y)))) NIL)
            (EQUAL (memb? (remb (C x y))) NIL)
            TRU))
    ≡      (IF (ATOM (C x y))
        (EQUAL (IF TRU
                    NIL
                    (IF (EQUAL (CAR (S "'()")) (S "?"))
                        TRU
                        (memb? (CDR (S "'()")))))
                        NIL)
        (IF (EQUAL (memb? (remb (CDR (C x y)))) NIL)
            (EQUAL (memb? (remb (C x y))) NIL)
            TRU))
memb?/remb x y = begin
    (IF (ATOM (C x y))
        (EQUAL (memb? (remb (C x y))) NIL)
        (IF (EQUAL (memb? (remb (CDR (C x y)))) NIL)
            (EQUAL (memb? (remb (C x y))) NIL)
            TRU))
  ≡⟨ cong (λ t → ((IF (ATOM (C x y))
        (EQUAL (memb? t) NIL)
        (IF (EQUAL (memb? (remb (CDR (C x y)))) NIL)
            (EQUAL (memb? (remb (C x y))) NIL)
            TRU)))) (def-remb (C x y)) ⟩
    (IF (ATOM (C x y))
        (EQUAL (memb? (IF (ATOM (C x y))
          (S "'()")
          (IF (EQUAL (CAR (C x y)) (S "?"))
              (remb (CDR (C x y)))
              (CONS (CAR (C x y))
                 (remb (CDR (C x y)))))))
                        NIL)
        (IF (EQUAL (memb? (remb (CDR (C x y)))) NIL)
            (EQUAL (memb? (remb (C x y))) NIL)
            TRU))
  ≡⟨ ifAP (if-nest-A (ATOM (C x y)) (S "'()") ((IF (EQUAL (CAR (C x y)) (S "?"))
              (remb (CDR (C x y)))
              (CONS (CAR (C x y))
                 (remb (CDR (C x y))))))) (premise2 (C x y)) ⟩
    (IF (ATOM (C x y))
        (EQUAL (memb?
          (S "'()"))
                        NIL)
        (IF (EQUAL (memb? (remb (CDR (C x y)))) NIL)
            (EQUAL (memb? (remb (C x y))) NIL)
            TRU))
  ≡⟨ cong ((λ t → (IF (ATOM (C x y))
        (EQUAL t
                        NIL)
        (IF (EQUAL (memb? (remb (CDR (C x y)))) NIL)
            (EQUAL (memb? (remb (C x y))) NIL)
            TRU)))) (def-memb? ((S "'()"))) ⟩
    (IF (ATOM (C x y))
        (EQUAL (IF (ATOM (S "'()"))
                    NIL
                    (IF (EQUAL (CAR (S "'()")) (S "?"))
                        TRU
                        (memb? (CDR (S "'()")))))
                        NIL)
        (IF (EQUAL (memb? (remb (CDR (C x y)))) NIL)
            (EQUAL (memb? (remb (C x y))) NIL)
            TRU))
  ≡⟨ cong ((λ t →     (IF (ATOM (C x y))
        (EQUAL (IF t
                    NIL
                    (IF (EQUAL (CAR (S "'()")) (S "?"))
                        TRU
                        (memb? (CDR (S "'()")))))
                        NIL)
        (IF (EQUAL (memb? (remb (CDR (C x y)))) NIL)
            (EQUAL (memb? (remb (C x y))) NIL)
            TRU)))) atomt ⟩
    (IF (ATOM (C x y))
        (EQUAL (IF TRU
                    NIL
                    (IF (EQUAL (CAR (S "'()")) (S "?"))
                        TRU
                        (memb? (CDR (S "'()")))))
                        NIL)
        (IF (EQUAL (memb? (remb (CDR (C x y)))) NIL)
            (EQUAL (memb? (remb (C x y))) NIL)
            TRU))
  ∎
  where open PropEq.≡-Reasoning


text:
-- Andreas, 2012-05-09
module DontPrune where

open import Common.Equality
open import Common.Product

data Bool : Set where
  true false : Bool

test : (A : Set) →
  let IF : Bool → A → A → A
      IF = _
  in  (a b : A) →
      (IF true a b ≡ a) × (IF false a b ≡ b)
test A a b = refl , refl

-- Expected result: unsolved metas
--
-- (unless someone implemented unification that produces definitions by case).
--
-- The test case should prevent overzealous pruning:
-- If the first equation pruned away the b, then the second
-- would have an unbound rhs.

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------------
-- Testing various arguments in the ATP pragmas
------------------------------------------------------------------------------

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

module VariousArguments where

postulate
  D       : Set
  _≡_     : D → D → Set
  a b c d : D
  a≡b     : a ≡ b
  b≡c     : b ≡ c
  c≡d     : c ≡ d
{-# ATP axioms a≡b b≡c c≡d #-}

postulate a≡d : a ≡ d
{-# ATP prove a≡d #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Colimit where

open import Level

open import Categories.Category
open import Categories.Functor
open import Categories.NaturalTransformation
open import Categories.Functor.Constant
open import Categories.Cocones
open import Categories.Cocone
open import Categories.Object.Initial

-- Isomorphic to an terminal object, but worth keeping distinct in case we change its definition
record Colimit {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} (F : Functor J C) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  field
    initial : Initial (Cocones F)

  module I = Initial initial
  module Ic = Cocone I.⊥
  private module C = Category C

  ∃F : C.Obj
  ∃F = Ic.N

  ι : NaturalTransformation F (Constant ∃F)
  ι = record { η = Ic.ψ; commute = λ f → C.Equiv.trans (C.Equiv.sym (Ic.commute f)) (C.Equiv.sym C.identityˡ) }

  <_> : ∀ {Q} → NaturalTransformation F (Constant Q) → ∃F C.⇒ Q
  <_> {Q} η = CoconeMorphism.f (I.! {record
          { N = Q
          ; ψ = η.η
          ; commute = λ f → C.Equiv.trans (C.Equiv.sym C.identityˡ) (C.Equiv.sym (η.commute f)) }})
    where
      module η = NaturalTransformation η

record Cocomplete (o ℓ e : Level) {o′ ℓ′ e′} (C : Category o′ ℓ′ e′) : Set (suc o ⊔ suc ℓ ⊔ suc e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  field
    colimit : ∀ {J : Category o ℓ e} (F : Functor J C) → Colimit F

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Esterel.Variable.Sequential where

open import Data.Nat
  using (ℕ) renaming (_≟_ to _≟ℕ_)
open import Function
  using (_∘_)
open import Relation.Nullary
  using (Dec ; yes ; no ; ¬_)
open import Relation.Binary
  using (Decidable)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; cong ; trans ; sym)

data SeqVar : Set where
  _ᵥ : ℕ → SeqVar

unwrap : SeqVar → ℕ
unwrap (n ᵥ) = n

unwrap-inverse : ∀ {s} → (unwrap s) ᵥ ≡ s
unwrap-inverse {_ ᵥ} = refl

unwrap-injective : ∀ {s t} → unwrap s ≡ unwrap t → s ≡ t
unwrap-injective s'≡t' = trans (sym unwrap-inverse) (trans (cong _ᵥ s'≡t') unwrap-inverse)

-- for backward compatibility
unwrap-neq : ∀{k1 : SeqVar} → ∀{k2 : SeqVar} → ¬ k1 ≡ k2 → ¬ (unwrap k1) ≡ (unwrap k2)
unwrap-neq = (_∘ unwrap-injective)

wrap : ℕ → SeqVar
wrap = _ᵥ

bijective : ∀{x} → unwrap (wrap x) ≡ x
bijective = refl

_≟_ : Decidable {A = SeqVar} _≡_
(s ᵥ) ≟ (t ᵥ) with s ≟ℕ t
... | yes p = yes (cong _ᵥ p)
... | no ¬p = no (¬p ∘ cong unwrap)

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Functions
------------------------------------------------------------------------

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

module Function where

open import Function.Core public
open import Function.Base public
open import Function.Definitions public
open import Function.Structures public
open import Function.Bundles public


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

open import Base
open import Homotopy.Pushout
open import Homotopy.VanKampen.Guide

module Homotopy.VanKampen.Code.LemmaPackA {i} (d : pushout-diag i)
  (l : legend i (pushout-diag.C d)) where

  open import Homotopy.Truncation
  open import Homotopy.PathTruncation

  private
    module PackA1 (d : pushout-diag i)
      (l : legend i (pushout-diag.C d)) (n : legend.name l) where
      open pushout-diag d
      open legend l

      -- Code from A.
      open import Homotopy.VanKampen.SplitCode d l (f $ loc n)
      -- Code from B. F for `flipped'.
      import Homotopy.VanKampen.SplitCode (pushout-diag-flip d) l (g $ loc n) as F

      private
        ap⇒bp-split : (∀ {a₂} → code-a a₂ → F.code-b a₂)
                    × (∀ {b₂} → code-b b₂ → F.code-a b₂)
        ap⇒bp-split = code-rec-nondep
          F.code-b ⦃ λ _ → F.code-b-is-set _ ⦄
          F.code-a ⦃ λ _ → F.code-a-is-set _ ⦄
          (λ p → F.⟧a refl₀ F.a⟦ n ⟧b p)
          (λ n₁ pco p → pco F.a⟦ n₁ ⟧b p)
          (λ n₁ pco p → pco F.b⟦ n₁ ⟧a p)
          (λ n₁ pco → F.code-b-refl-refl n₁ pco)
          (λ n₁ pco → F.code-a-refl-refl n₁ pco)
          (λ n₁ pco n₂ r → F.code-ba-swap n₁ pco n₂ r)

      aa⇒ba : ∀ {a₂} → code-a a₂ → F.code-b a₂
      aa⇒ba = π₁ ap⇒bp-split
      ab⇒bb : ∀ {b₂} → code-b b₂ → F.code-a b₂
      ab⇒bb = π₂ ap⇒bp-split

  private
    module PackA2 (d : pushout-diag i)
      (l : legend i (pushout-diag.C d)) (n : legend.name l) where
      open pushout-diag d
      open legend l

      -- Code from A.
      open import Homotopy.VanKampen.SplitCode d l (f $ loc n)
      open PackA1 d l n public
      -- Code from B. F for `flipped'.
      private
        module F where
          open import Homotopy.VanKampen.SplitCode (pushout-diag-flip d) l (g $ loc n) public
          open PackA1 (pushout-diag-flip d) l n public

      private
        aba-glue-code-split : (∀ {a₂} (co : code-a a₂) → F.ab⇒bb (aa⇒ba co) ≡ co)
                            × (∀ {b₂} (co : code-b b₂) → F.aa⇒ba (ab⇒bb co) ≡ co)
      abstract
        aba-glue-code-split = code-rec
          (λ {a} co → F.ab⇒bb (aa⇒ba co) ≡ co)
          ⦃ λ _ → ≡-is-set $ code-a-is-set _ ⦄
          (λ {b} co → F.aa⇒ba (ab⇒bb co) ≡ co)
          ⦃ λ _ → ≡-is-set $ code-b-is-set _ ⦄
          (λ p →
            ⟧a refl₀ a⟦ n ⟧b refl₀ b⟦ n ⟧a p
                ≡⟨ code-a-merge n refl₀ p ⟩
            ⟧a refl₀ ∘₀ p
                ≡⟨ ap (λ x → ⟧a x) $ refl₀-left-unit p ⟩∎
            ⟧a p
                ∎)
          (λ n₁ {co} eq p → ap (λ x → x b⟦ n₁ ⟧a p) eq)
          (λ n₁ {co} eq p → ap (λ x → x a⟦ n₁ ⟧b p) eq)
          (λ _ _ → code-has-all-cells₂-a _ _)
          (λ _ _ → code-has-all-cells₂-b _ _)
          (λ _ _ _ _ → code-has-all-cells₂-a _ _)

      aba-glue-code-a : ∀ {a₂} (co : code-a a₂) → F.ab⇒bb (aa⇒ba co) ≡ co
      aba-glue-code-a = π₁ aba-glue-code-split
      aba-glue-code-b : ∀ {b₂} (co : code-b b₂) → F.aa⇒ba (ab⇒bb co) ≡ co
      aba-glue-code-b = π₂ aba-glue-code-split

  private
    module PackA3 (d : pushout-diag i)
      (l : legend i (pushout-diag.C d)) (n : legend.name l) where
      open pushout-diag d
      open legend l

      -- Code from A.
      open import Homotopy.VanKampen.SplitCode d l (f $ loc n)
      open PackA2 d l n public
      -- Code from B. F for `flipped'.
      private
        module F where
          open import Homotopy.VanKampen.SplitCode (pushout-diag-flip d) l (g $ loc n) public
          open PackA2 (pushout-diag-flip d) l n public

      flipped-code : P → Set i
      flipped-code = F.code ◯ pushout-flip

      private
        ap⇒bp-glue : ∀ c → transport (λ p → code p → flipped-code p) (glue c) aa⇒ba ≡ ab⇒bb
      abstract
        ap⇒bp-glue = loc-fiber-rec l
          (λ c → transport (λ p → code p → flipped-code p) (glue c) aa⇒ba ≡ ab⇒bb)
          ⦃ λ _ → Π-is-set (λ _ → F.code-a-is-set _) _ _ ⦄
          (λ n → funext λ co →
            transport (λ p → code p → flipped-code p) (glue $ loc n) aa⇒ba co
                ≡⟨ trans-→ code flipped-code (glue $ loc n) aa⇒ba co ⟩
            transport flipped-code (glue $ loc n)
              (aa⇒ba $ transport code (! $ glue $ loc n) co)
                ≡⟨ ap (λ x → transport flipped-code (glue $ loc n) $ aa⇒ba x)
                    $ trans-code-!glue-loc n co ⟩
            transport flipped-code (glue $ loc n) (aa⇒ba $ b⇒a n co)
                ≡⟨ refl ⟩
            transport flipped-code (glue $ loc n) (F.a⇒b n $ ab⇒bb co)
                ≡⟨ ! $ trans-ap F.code pushout-flip (glue $ loc n)
                     $ F.a⇒b n $ ab⇒bb co ⟩
            transport F.code (ap pushout-flip $ glue $ loc n) (F.a⇒b n $ ab⇒bb co)
                ≡⟨ ap (λ x → transport F.code x $ F.a⇒b n $ ab⇒bb co)
                      $ pushout-β-glue-nondep _ right left (! ◯ glue) $ loc n ⟩
            transport F.code (! $ glue $ loc n) (F.a⇒b n $ ab⇒bb co)
                ≡⟨ F.trans-code-!glue-loc n (F.a⇒b n $ ab⇒bb co) ⟩
            F.b⇒a n (F.a⇒b n $ ab⇒bb co)
                ≡⟨ F.code-a-refl-refl n $ ab⇒bb co ⟩∎
            ab⇒bb co
                ∎)

      ap⇒bp : ∀ {p} → code p → flipped-code p
      ap⇒bp {p} = pushout-rec
        (λ x → code x → flipped-code x)
        (λ _ → aa⇒ba)
        (λ _ → ab⇒bb)
        ap⇒bp-glue
        p

  open PackA3 d l public

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module Cats.Functor.Yoneda where

open import Data.Product using (_,_)
open import Relation.Binary using (Rel ; Setoid ; IsEquivalence)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)

open import Cats.Bifunctor using (transposeBifunctor₂)
open import Cats.Category
open import Cats.Category.Cat.Facts.Exponential using (Eval)
open import Cats.Category.Cat.Facts.Product using (First ; Swap)
open import Cats.Category.Fun using (Fun ; Trans ; ≈-intro ; ≈-elim)
open import Cats.Category.Fun.Facts using (NatIso→≅)
open import Cats.Category.Op using (_ᵒᵖ)
open import Cats.Category.Product.Binary using (_×_)
open import Cats.Category.Setoids using (Setoids ; ≈-intro ; ≈-elim ; ≈-elim′)
open import Cats.Functor using
  ( Functor ; _∘_ ; IsFull ; IsFaithful ; IsEmbedding ; Embedding→Full
  ; Embedding→Faithful )
open import Cats.Functor.Op using (Op)
open import Cats.Functor.Representable using (Hom[_])
open import Cats.Util.SetoidMorphism.Iso using (IsIso-resp)

import Cats.Util.SetoidReasoning as SetoidReasoning
import Cats.Category.Constructions.Iso

open Functor
open Trans
open Cats.Category.Setoids._⇒_
open Setoid using (Carrier)

-- We force C to be at l/l/l. Can we generalise to lo/la/l≈?
module _ {l} {C : Category l l l} where

  private
    Sets : Category _ _ _
    Sets = Setoids l l

    Presheaves : Category _ _ _
    Presheaves = Fun (C ᵒᵖ) Sets

    Funs : Category _ _ _
    Funs = Fun ((C ᵒᵖ) × Presheaves) Sets

    module C = Category C
    module Sets = Category Sets
    module Pre = Category Presheaves
    module Funs = Category Funs

  y : Functor C Presheaves
  y = transposeBifunctor₂ Hom[ C ]

  module _ (c : C.Obj) (F : Functor (C ᵒᵖ) (Sets)) where

    private
      module ycc≈ = Setoid (fobj (fobj y c) c)
      module Fc≈ = Setoid (fobj F c)

    forth : Pre.Hom (fobj y c) F Sets.⇒ fobj F c
    forth = record
        { arr = λ f → arr (component f c) C.id
        ; resp = λ f≈g → ≈-elim′ (≈-elim f≈g)
        }

    back-θ-component : Carrier (fobj F c) → (c′ : C.Obj) → C.Hom c′ c Sets.⇒ fobj F c′
    back-θ-component a c′ = record
        { arr = λ h → arr (fmap F h) a
        ; resp = λ f≈g → ≈-elim′ (fmap-resp F f≈g)
        }

    back-θ : Carrier (fobj F c) → fobj y c Pre.⇒ F
    back-θ a = record
        { component = back-θ-component a
        ; natural = λ {c′} {d′} {f} → ≈-intro λ {g} {g′} g≈g′ →
            let open Setoid (fobj F d′) using (sym) in
            begin⟨ fobj F d′ ⟩
              arr (back-θ-component a d′ Sets.∘ fmap (fobj y c) f) g
            ≡⟨⟩
              arr (fmap F (C.id C.∘ g C.∘ f)) a
            ≈⟨ ≈-elim′ (fmap-resp F (C.≈.trans C.id-l (C.∘-resp-l g≈g′))) ⟩
              arr (fmap F (g′ C.∘ f)) a
            ≈⟨ sym (≈-elim′ (fmap-∘ F)) ⟩
              arr (fmap F f Sets.∘ fmap F g′) a
            ≡⟨⟩
              arr (fmap F f Sets.∘ back-θ-component a c′) g′
            ∎
        }
      where
        open SetoidReasoning

    back : fobj F c Sets.⇒ Pre.Hom (fobj y c) F
    back = record
        { arr = back-θ
        ; resp = λ f≈g → ≈-intro (≈-intro λ x≈y → ≈-elim (fmap-resp F x≈y) f≈g)
        }

    back-forth : back Sets.∘ forth Sets.≈ Sets.id
    back-forth = ≈-intro λ {θ} {θ′} θ≈θ′ → ≈-intro λ {c′} → ≈-intro λ {f} {g} f≈g →
        begin⟨ fobj F c′ ⟩
          arr (component (arr (back Sets.∘ forth) θ) c′) f
        ≡⟨⟩
          arr (fmap F f Sets.∘ component θ c) C.id
        ≈⟨ ≈-elim′ (Sets.≈.sym (natural θ)) ⟩
          arr (component θ c′ Sets.∘ fmap (fobj y c) f) C.id
        ≡⟨⟩
          arr (component θ c′) (C.id C.∘ C.id C.∘ f)
        ≈⟨ resp (component θ c′) (C.≈.trans C.id-l C.id-l) ⟩
          arr (component θ c′) f
        ≈⟨ ≈-elim (≈-elim θ≈θ′) f≈g ⟩
          arr (component θ′ c′) g
        ∎
      where
        open SetoidReasoning

    forth-back : forth Sets.∘ back Sets.≈ Sets.id
    forth-back = ≈-intro λ x≈y → ≈-elim (fmap-id F) x≈y

    iso : fobj Hom[ Presheaves ] (fobj y c , F) Sets.≅ fobj F c
    iso = record
        { forth = forth
        ; back = back
        ; back-forth = back-forth
        ; forth-back = forth-back
        }

  yoneda : (Hom[ Presheaves ] ∘ First (Op y)) Funs.≅ (Eval ∘ Swap)
  yoneda = NatIso→≅ record
      { iso = λ { {c , F} → iso c F }
      ; forth-natural = λ where
          {c , F} {c′ , F′} {f , θ} → ≈-intro λ {ι} {τ} ι≈τ →
            let module S = Setoid (fobj F′ c′) in
            triangle (fobj F′ c′) (arr (component (θ Pre.∘ ι) c′) f)
              ( begin⟨ fobj F′ c′ ⟩
                  arr (forth c′ F′ Sets.∘ fmap Hom[ Presheaves ]
                         (fmap (First {D = Presheaves ᵒᵖ} (Op y)) (f , θ)))
                      ι
                ≡⟨⟩
                  arr (component (Pre.id Pre.∘ θ Pre.∘ ι) c′) (f C.∘ C.id C.∘ C.id)
                ≈⟨ ≈-elim (≈-elim (Pre.id-l {f = θ Pre.∘ ι}))
                    (C.≈.trans (C.∘-resp-r C.id-r) C.id-r) ⟩
                  arr (component (θ Pre.∘ ι) c′) f
                ∎
              )

              ( begin⟨ fobj F′ c′ ⟩
                  arr (fmap F′ f Sets.∘ component θ c Sets.∘ forth c F) τ
                ≡⟨⟩
                  arr (fmap F′ f Sets.∘ component (θ Pre.∘ τ) c) C.id
                ≈⟨ S.sym (≈-elim′ (natural (θ Pre.∘ τ))) ⟩
                  arr (component (θ Pre.∘ τ) c′ Sets.∘ fmap (fobj y c) f) C.id
                ≡⟨⟩
                  arr (component (θ Pre.∘ τ) c′) (C.id C.∘ C.id C.∘ f)
                ≈⟨ ≈-elim (≈-elim (Pre.∘-resp-r {f = θ} (Pre.≈.sym {i = ι} {τ} ι≈τ)))
                    (C.≈.trans C.id-l C.id-l) ⟩
                  arr (component (θ Pre.∘ ι) c′) f
                ∎
              )
      }
    where
      open SetoidReasoning

  back≈sfmap : ∀ {a b} → back a (fobj y b) Sets.≈ sfmap y
  back≈sfmap {a} {b} = ≈-intro λ {f} {g} f≈g → ≈-intro (≈-intro λ {x} {y} x≈y →
      begin
        C.id C.∘ f C.∘ x
      ≈⟨ C.id-l ⟩
        f C.∘ x
      ≈⟨ C.∘-resp f≈g x≈y ⟩
        g C.∘ y
      ≈⟨ C.≈.sym C.id-r ⟩
        (g C.∘ y) C.∘ C.id
      ≈⟨ C.assoc ⟩
        g C.∘ y C.∘ C.id
      ∎)
    where
      open C.≈-Reasoning

  y-Embedding : IsEmbedding y
  y-Embedding {a} {b} = IsIso-resp back≈sfmap record
      { back = forth a (fobj y b)
      ; forth-back = back-forth a (fobj y b)
      ; back-forth = forth-back a (fobj y b)
      }

  y-Full : IsFull y
  y-Full = Embedding→Full y y-Embedding

  y-Faithful : IsFaithful y
  y-Faithful = Embedding→Faithful y y-Embedding

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
module Automata.Composition.Union (Σ : Set) where

-- Standard libraries imports ----------------------------------------
open import Data.Empty using (⊥ ; ⊥-elim)
open import Data.Nat using (ℕ)
open import Data.Sum using (_⊎_ ; inj₁ ; inj₂)
open import Data.Product using (_,_)
open import Data.Vec using (Vec ; [] ; _∷_)

open import Relation.Nullary using (¬_)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl)
----------------------------------------------------------------------

-- Thesis imports ----------------------------------------------------
open import Automata.Nondeterministic
----------------------------------------------------------------------

_∪_ : (M : NDA Σ) → (N : NDA Σ) → NDA Σ
⟨ Q₁ , S₁ , F₁ , Δ₁ ⟩ ∪ ⟨ Q₂ , S₂ , F₂ , Δ₂ ⟩ = ⟨ Q , S , F , Δ ⟩
  where
    Q : Set _
    Q = Q₁ ⊎ Q₂

    S : Q → Set _
    S (inj₁ q) = S₁ q
    S (inj₂ q) = S₂ q

    F : Q → Set
    F (inj₁ q) = F₁ q
    F (inj₂ q) = F₂ q

    Δ : Q → Σ → Q → Set
    Δ (inj₁ q) c (inj₁ q′) = Δ₁ q c q′
    Δ (inj₂ q) c (inj₂ q′) = Δ₂ q c q′
    {-# CATCHALL #-}
    Δ _ _ _ = ⊥ -- No connections between the machines

M-Δ*⇒M∪N-Δ* : {M N : NDA Σ}
             → let Q₁ = NDA.Q M
                   Δ₁* = NDA.Δ* M
                   Δ* = NDA.Δ* (M ∪ N) in
               (q : Q₁) → {n : ℕ} → (xs : Vec Σ n) → (q′ : Q₁)
             → Δ₁* q xs q′
             → Δ* (inj₁ q) xs (inj₁ q′)
M-Δ*⇒M∪N-Δ* q [] .q refl = refl
M-Δ*⇒M∪N-Δ* q (x ∷ xs) q′ (q₀ , Δ₁-q-x-q₀ , Δ₁*-q₀-xs-q′) =
  inj₁ q₀ , Δ₁-q-x-q₀ , M-Δ*⇒M∪N-Δ* q₀ xs q′ Δ₁*-q₀-xs-q′

N-Δ*⇒M∪N-Δ* : {M N : NDA Σ}
             → let Q₂ = NDA.Q N
                   Δ₂* = NDA.Δ* N
                   Δ* = NDA.Δ* (M ∪ N) in
               (q : Q₂) → {n : ℕ} → (xs : Vec Σ n) → (q′ : Q₂)
             → Δ₂* q xs q′
             → Δ* (inj₂ q) xs (inj₂ q′)
N-Δ*⇒M∪N-Δ* q [] .q refl = refl
N-Δ*⇒M∪N-Δ* q (x ∷ xs) q′ (q₀ , Δ₂-q-x-q₀ , Δ₂*-q₀-xs-q′) =
  inj₂ q₀ , Δ₂-q-x-q₀ , N-Δ*⇒M∪N-Δ* q₀ xs q′ Δ₂*-q₀-xs-q′

M∪N-Δ*⇒M-Δ* : {M N : NDA Σ}
             → let Q₁ = NDA.Q M
                   Δ₁* = NDA.Δ* M
                   Δ* = NDA.Δ* (M ∪ N) in
               (q : Q₁) → {n : ℕ} → (xs : Vec Σ n) → (q′ : Q₁)
             → Δ* (inj₁ q) xs (inj₁ q′)
             → Δ₁* q xs q′
M∪N-Δ*⇒M-Δ* q [] .q refl = refl
M∪N-Δ*⇒M-Δ* q (x ∷ xs) q′ (inj₁ q₀ , Δ-q-x-q₀ , Δ*-q₀-xs-q′) =
  q₀ , Δ-q-x-q₀ , M∪N-Δ*⇒M-Δ* q₀ xs q′ Δ*-q₀-xs-q′

M∪N-Δ*⇒N-Δ* : {M N : NDA Σ}
             → let Q₂ = NDA.Q N
                   Δ₂* = NDA.Δ* N
                   Δ* = NDA.Δ* (M ∪ N) in
               (q : Q₂) → {n : ℕ} → (xs : Vec Σ n) → (q′ : Q₂)
             → Δ* (inj₂ q) xs (inj₂ q′)
             → Δ₂* q xs q′
M∪N-Δ*⇒N-Δ* q [] .q refl = refl
M∪N-Δ*⇒N-Δ* q (x ∷ xs) q′ (inj₂ q₀ , Δ-q-x-q₀ , Δ*-q₀-xs-q′) =
  q₀ , Δ-q-x-q₀ , M∪N-Δ*⇒N-Δ* q₀ xs q′ Δ*-q₀-xs-q′

M∪N-Δ*-disconnectedˡ : {M N : NDA Σ}
                     → let Q₁ = NDA.Q M
                           Q₂ = NDA.Q N
                           Δ* = NDA.Δ* (M ∪ N) in
                       (q : Q₁) → {n : ℕ} → (xs : Vec Σ n) → (q′ : Q₂)
                     → ¬ (Δ* (inj₁ q) xs (inj₂ q′))
M∪N-Δ*-disconnectedˡ q (x ∷ xs) q′ (inj₁ q₀ , _ , Δ*-q₀-xs-q′) =
  M∪N-Δ*-disconnectedˡ q₀ xs q′ Δ*-q₀-xs-q′

M∪N-Δ*-disconnectedʳ : {M N : NDA Σ}
                     → let Q₁ = NDA.Q M
                           Q₂ = NDA.Q N
                           Δ* = NDA.Δ* (M ∪ N) in
                       (q : Q₂) → {n : ℕ} → (xs : Vec Σ n) → (q′ : Q₁)
                     → ¬ (Δ* (inj₂ q) xs (inj₁ q′))
M∪N-Δ*-disconnectedʳ q (x ∷ xs) q′ (inj₂ q₀ , _ , Δ*-q₀-xs-q′) =
  M∪N-Δ*-disconnectedʳ q₀ xs q′ Δ*-q₀-xs-q′

M-Accepts⇒M∪N-Accepts : {M N : NDA Σ}
                      → {n : ℕ} → (xs : Vec Σ n)
                      → NDA.Accepts M xs
                      → NDA.Accepts (M ∪ N) xs
M-Accepts⇒M∪N-Accepts [] (q , S-q , .q , F-q , refl) =
  inj₁ q , S-q , inj₁ q , F-q , refl
M-Accepts⇒M∪N-Accepts (x ∷ xs)
  ( q  , S-q         -- The beginning state
  , q′ , F-q′       -- The ending state
  , q₀ , Δ₁-q-x-q₀   -- The first step
  , Δ₁*-q₀-xs-q′) =  -- The remaining steps
  -- Translate to the union:
    (inj₁ q , S-q        -- The beginning state
    , inj₁ q′ , F-q′     -- The ending state
    , inj₁ q₀ , Δ₁-q-x-q₀  -- The first step
    , M-Δ*⇒M∪N-Δ* q₀ xs q′ Δ₁*-q₀-xs-q′)   -- The remaining steps (applying I.H.)

N-Accepts⇒M∪N-Accepts : {M N : NDA Σ}
                      → {n : ℕ} → (xs : Vec Σ n)
                      → NDA.Accepts N xs
                      → NDA.Accepts (M ∪ N) xs
N-Accepts⇒M∪N-Accepts [] (q , S-q , .q , F-q , refl) =
  inj₂ q , S-q , inj₂ q , F-q , refl
N-Accepts⇒M∪N-Accepts (x ∷ xs)
  ( q , S-q
  , q′ , F-q′
  , q₀ , Δ-q-x-q₀
  , Δ*-q₀-xs-q′) =
    ( inj₂ q , S-q
    , inj₂ q′ , F-q′
    , inj₂ q₀ , Δ-q-x-q₀
    , N-Δ*⇒M∪N-Δ* q₀ xs q′ Δ*-q₀-xs-q′ )

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

M∪N-Accepts⇒M-Accepts∨N-Accepts : {M N : NDA Σ}
                                → {n : ℕ} → (xs : Vec Σ n)
                                → NDA.Accepts (M ∪ N) xs
                                → NDA.Accepts M xs  ⊎  NDA.Accepts N xs

-- Base cases.

M∪N-Accepts⇒M-Accepts∨N-Accepts []
  (inj₁ q , S-q , .(inj₁ q) , F-q , refl) =
    inj₁ (q , S-q , q , F-q , refl)
M∪N-Accepts⇒M-Accepts∨N-Accepts []
  (inj₂ q , S-q , .(inj₂ q) , F-q , refl) =
    inj₂ (q , S-q , q , F-q , refl)

-- Induction step 1: both the start and final state are in M.

M∪N-Accepts⇒M-Accepts∨N-Accepts (x ∷ xs)
  ( inj₁ q  , S-q
  , inj₁ q′ , F-q′
  , inj₁ q₀ , Δ-q-x-q₀
  , Δ*-q₀-xs-q′) =
    inj₁ ( q , S-q
         , q′ , F-q′
         , q₀ , Δ-q-x-q₀
         , M∪N-Δ*⇒M-Δ* q₀ xs q′ Δ*-q₀-xs-q′)

-- Induction step 2: both the start and final state are in N.

M∪N-Accepts⇒M-Accepts∨N-Accepts (x ∷ xs)
  ( inj₂ q  , S-q
  , inj₂ q′ , F-q′
  , inj₂ q₀ , Δ-q-x-q₀
  , Δ*-q₀-xs-q′) =
    inj₂ ( q  , S-q
         , q′ , F-q′
         , q₀ , Δ-q-x-q₀
         , M∪N-Δ*⇒N-Δ* q₀ xs q′ Δ*-q₀-xs-q′)

-- Unreachable cases: the proof of “Accepts (M ∪ N) xs”
-- asserts M and N are connected.

M∪N-Accepts⇒M-Accepts∨N-Accepts (x ∷ xs)
  (inj₁ q , _ , inj₂ q′ , _ , inj₁ q₀ , _ , Δ*-q₀-xs-q′) =
    ⊥-elim (M∪N-Δ*-disconnectedˡ q₀ xs q′ Δ*-q₀-xs-q′)
M∪N-Accepts⇒M-Accepts∨N-Accepts (x ∷ xs)
  (inj₂ q , _ , inj₁ q′ , _ , inj₂ q₀ , _ , Δ*-q₀-xs-q′) =
    ⊥-elim (M∪N-Δ*-disconnectedʳ q₀ xs q′ Δ*-q₀-xs-q′)

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

max_stars_repo_name: armkeh/agda-computability

max_issues_repo_name: armkeh/agda-computability

max_forks_repo_name: armkeh/agda-computability


text:
{-

This file contains the classic isomorphism theorems for groups (so far
only the first theorem)

-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.IsomorphismTheorems where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Powerset
open import Cubical.Foundations.Function
open import Cubical.Data.Sigma
open import Cubical.HITs.SetQuotients renaming (_/_ to _/s_ ; rec to recS ; elim to elimS)
open import Cubical.HITs.PropositionalTruncation

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Subgroup
open import Cubical.Algebra.Group.QuotientGroup
open import Cubical.Algebra.Group.GroupPath

private
  variable
    ℓ : Level

-- The first isomorphism theorem: im ϕ ≃ G / ker ϕ
module _ {G H : Group ℓ} (ϕ : GroupHom G H) where

  open isSubgroup
  open Iso
  open GroupTheory

  kerNormalSubgroup : NormalSubgroup G
  kerNormalSubgroup = kerSubgroup ϕ , isNormalKer ϕ

  private
    imϕ : Group ℓ
    imϕ = imGroup ϕ

  -- for completeness:
  imNormalSubgroup : ((x y : ⟨ H ⟩)
    → GroupStr._·_ (snd H) x y ≡ GroupStr._·_ (snd H) y x)
    → NormalSubgroup H
  imNormalSubgroup comm = imSubgroup ϕ , isNormalIm ϕ comm

  private
    module G = GroupStr (snd G)
    module H = GroupStr (snd H)
    module imG = GroupStr (snd imϕ)
    module kerG = GroupStr (snd (G / kerNormalSubgroup))
    module ϕ = IsGroupHom (ϕ .snd)

  f1 : ⟨ imϕ ⟩ → ⟨ G / kerNormalSubgroup ⟩
  f1 (x , Hx) = rec→Set ( squash/)
                         (λ { (y , hy) → [ y ]})
                         (λ { (y , hy) (z , hz) → eq/ y z (rem y z hy hz) })
                         Hx
    where
    rem : (y z : ⟨ G ⟩) → ϕ .fst y ≡ x → ϕ .fst z ≡ x → ϕ .fst (y G.· G.inv z) ≡ H.1g
    rem y z hy hz =
      ϕ .fst (y G.· G.inv z)        ≡⟨ ϕ.pres· _ _ ⟩
      ϕ .fst y H.· ϕ .fst (G.inv z) ≡⟨ cong (ϕ .fst y H.·_) (ϕ.presinv _) ⟩
      ϕ .fst y H.· H.inv (ϕ .fst z) ≡⟨ (λ i → hy i H.· H.inv (hz i)) ⟩
      x H.· H.inv x                 ≡⟨ H.·InvR x ⟩
      H.1g                          ∎

  f2 : ⟨ G / kerNormalSubgroup ⟩ → ⟨ imϕ ⟩
  f2 = recS imG.is-set (λ y → ϕ .fst y , ∣ y , refl ∣₁)
                       (λ x y r → Σ≡Prop (λ _ → squash₁)
                       (rem x y r))
    where
    rem : (x y : ⟨ G ⟩) → ϕ .fst (x G.· G.inv y) ≡ H.1g → ϕ .fst x ≡ ϕ .fst y
    rem x y r =
      ϕ .fst x                                      ≡⟨ sym (H.·IdR _) ⟩
      ϕ .fst x H.· H.1g                             ≡⟨ cong (ϕ .fst x H.·_) (sym (H.·InvL _)) ⟩
      ϕ .fst x H.· H.inv (ϕ .fst y) H.· ϕ .fst y    ≡⟨ (λ i → ϕ .fst x H.· ϕ.presinv y (~ i) H.· ϕ .fst y) ⟩
      ϕ .fst x H.· ϕ .fst (G.inv y) H.· ϕ .fst y    ≡⟨ H.·Assoc _ _ _ ⟩
      (ϕ .fst x H.· ϕ .fst (G.inv y)) H.· ϕ .fst y  ≡⟨ cong (H._· _) (sym (ϕ.pres· _ _)) ⟩
      ϕ .fst (x G.· G.inv y) H.· ϕ .fst y           ≡⟨ cong (H._· ϕ .fst y) r ⟩
      H.1g H.· ϕ .fst y                             ≡⟨ H.·IdL _ ⟩
      ϕ .fst y ∎

  f12 : (x : ⟨ G / kerNormalSubgroup ⟩) → f1 (f2 x) ≡ x
  f12 = elimProp (λ _ → squash/ _ _) (λ _ → refl)

  f21 : (x : ⟨ imϕ ⟩) → f2 (f1 x) ≡ x
  f21 (x , hx) = elim {P = λ hx → f2 (f1 (x , hx)) ≡ (x , hx)}
                      (λ _ → imG.is-set _ _)
                      (λ {(x , hx) → Σ≡Prop (λ _ → squash₁) hx})
                      hx

  f1-isHom : (x y : ⟨ imϕ ⟩) → f1 (x imG.· y) ≡ f1 x kerG.· f1 y
  f1-isHom (x , hx) (y , hy) =
    elim2 {P = λ hx hy → f1 ((x , hx) imG.· (y , hy)) ≡ f1 (x , hx) kerG.· f1 (y , hy)}
          (λ _ _ → kerG.is-set _ _) (λ _ _ → refl) hx hy

  -- The first isomorphism theorem for groups
  isoThm1 : GroupIso imϕ (G / kerNormalSubgroup)
  fun (fst isoThm1) = f1
  inv (fst isoThm1) = f2
  rightInv (fst isoThm1) = f12
  leftInv (fst isoThm1) = f21
  snd isoThm1 = makeIsGroupHom f1-isHom

  -- The SIP lets us turn the isomorphism theorem into a path
  pathThm1 : imϕ ≡ G / kerNormalSubgroup
  pathThm1 = uaGroup (GroupIso→GroupEquiv isoThm1)

  surjImIso : isSurjective ϕ → GroupIso imϕ H
  surjImIso surj =
    BijectionIso→GroupIso
      (bijIso indHom
              (uncurry
                (λ h → elim (λ _ → isPropΠ (λ _ → imG.is-set _ _))
                  (uncurry λ g y
                    → λ inker → Σ≡Prop (λ _ → squash₁) inker)))
              λ b → map (λ x → (b , ∣ x ∣₁) , refl) (surj b))
    where
    indHom : GroupHom imϕ H
    fst indHom = fst
    snd indHom = makeIsGroupHom λ _ _ → refl

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Bicategory where

open import Level
-- open import Data.Product using (curry; _,_)
-- open import Function using () renaming (_∘_ to _·_)

open import Categories.Support.PropositionalEquality

open import Categories.Category
open import Categories.Categories
open import Categories.Object.Terminal
open import Categories.Terminal
open import Categories.Functor using (Functor) renaming (_∘_ to _∘F_; _≡_ to _≡F_; id to idF)
open import Categories.Functor.Constant using (Constant)
open import Categories.Bifunctor using (Bifunctor; reduce-×)
open import Categories.Product using (assocʳ; πˡ; πʳ)
open import Categories.NaturalIsomorphism
open import Categories.Bicategory.Helpers using (module BicategoryHelperFunctors)

record Bicategory (o ℓ t e : Level) : Set (suc (o ⊔ ℓ ⊔ t ⊔ e)) where
  open Terminal (One {ℓ} {t} {e})
  field
    Obj : Set o
    _⇒_ : (A B : Obj) → Category ℓ t e
    id : {A : Obj} → Functor ⊤ (A ⇒ A)
    —∘— : {A B C : Obj} → Bifunctor (B ⇒ C) (A ⇒ B) (A ⇒ C)

  _∘_ : {A B C : Obj} {L R : Category ℓ t e} → Functor L (B ⇒ C) → Functor R (A ⇒ B) → Bifunctor L R (A ⇒ C)
  _∘_ {A} {B} {C} F G = reduce-× {D₁ = B ⇒ C} {D₂ = A ⇒ B} —∘— F G

  field
    λᵤ : {A B : Obj} → NaturalIsomorphism (id ∘ idF {C = A ⇒ B}) (πʳ {C = ⊤} {A ⇒ B})
    ρᵤ : {A B : Obj} → NaturalIsomorphism (idF {C = A ⇒ B} ∘ id) (πˡ {C = A ⇒ B} {⊤})
    α : {A B C D : Obj} → NaturalIsomorphism (idF ∘ —∘—) (((—∘— ∘ idF) ∘F assocʳ (C ⇒ D) (B ⇒ C) (A ⇒ B)))

  private module BHF = BicategoryHelperFunctors(Obj)(_⇒_)(—∘—)(id)
  private module EQ = BHF.Coherence(λᵤ)(ρᵤ)(α)

  private module _⇒_ (A B : Obj) = Category (A ⇒ B)
  open _⇒_ public using () renaming (Obj to _⇒₁_)

  field
    .triangle : {A B C : Obj} (f : A ⇒₁ B) (g : B ⇒₁ C) → EQ.Triangle f g
    .pentagon : {A B C D E : Obj} (f : A ⇒₁ B) (g : B ⇒₁ C) (h : C ⇒₁ D) (i : D ⇒₁ E)
        → EQ.Pentagon f g h i

  -- do note that most of the "convenience" definitions in the Helpers module should really
  -- be here (but usable in both places).  Clean that up later.

max_issues_repo_name: copumpkin/categories

max_forks_repo_name: copumpkin/categories


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

module Definition.Typed.Consequences.PiNorm where

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening
open import Definition.Typed.EqRelInstance
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Fundamental.Reducibility
open import Definition.Typed.Consequences.Inversion
open import Definition.Typed.Consequences.Injectivity
open import Definition.Typed.Consequences.Syntactic
open import Definition.Conversion.Stability

open import Tools.Product
open import Tools.Empty
import Tools.PropositionalEquality as PE

-- reduction including in the codomain of Pis
-- useful to get unicity of relevance

-- there are 2 kinds of fat arrows!!!
-- the constructor for transitivity closure is closed on the left ⇨
-- the ones in types aren't ⇒

data ΠNorm : Term → Set where
  Uₙ : ∀ {r l} → ΠNorm (Univ r l)
  Πₙ : ∀ {F rF lF G lG lΠ} → ΠNorm G → ΠNorm (Π F ^ rF ° lF ▹ G ° lG ° lΠ)
  ∃ₙ : ∀ {F G} → ΠNorm F → ΠNorm (∃ F ▹ G)
  ℕₙ : ΠNorm ℕ
  Emptyₙ : ∀ {lEmpty} → ΠNorm (Empty lEmpty)
  ne   : ∀ {n} → Neutral n → ΠNorm n

ΠNorm-Π : ∀ {F rF lF G lG lΠ} → ΠNorm (Π F ^ rF ° lF ▹ G ° lG ° lΠ) → ΠNorm G
ΠNorm-Π (Πₙ x) = x
ΠNorm-Π (ne ())

data _⊢_⇒Π_∷_^_ (Γ : Con Term) : Term → Term → Term → TypeLevel → Set where
  regular : ∀ {t u A l} → Γ ⊢ t ⇒ u ∷ A ^ l → Γ ⊢ t ⇒Π u ∷ A ^ l
  deepΠ : ∀ {F rF lF G G′ lG rG lΠ}
       → Γ ∙ F ^ [ rF , ι lF ] ⊢ G ⇒Π G′ ∷ Univ rG lG ^ next lG
       → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° lΠ ⇒Π Π F ^ rF ° lF ▹ G′ ° lG ° lΠ ∷ Univ rG lΠ ^ next lΠ
  deep∃ : ∀ {F G F′ l∃}
       → Γ ⊢ F ⇒Π F′ ∷ Univ % l∃ ^ next l∃
       → Γ ⊢ ∃ F ▹ G ⇒Π ∃ F′ ▹ G ∷ Univ % l∃ ^ next l∃

data _⊢_⇒Π_^_ (Γ : Con Term) : Term → Term → TypeInfo → Set where
  univ : ∀ {A B r l}
       → Γ ⊢ A ⇒Π B ∷ (Univ r l) ^ next l
       → Γ ⊢ A ⇒Π B ^ [ r , ι l ]

data _⊢_⇒*Π_∷_^_ (Γ : Con Term) : Term → Term → Term → TypeLevel → Set where
  id : ∀ {t T l} → Γ ⊢ t ⇒*Π t ∷ T ^ l
  _⇨_ : ∀ {t t' u T l}
      → Γ ⊢ t  ⇒Π t' ∷ T ^ l
      → Γ ⊢ t' ⇒*Π u ∷ T ^ l
      → Γ ⊢ t  ⇒*Π u ∷ T ^ l

data _⊢_⇒*Π_^_ (Γ : Con Term) : Term → Term → TypeInfo → Set where
  id : ∀ {A r} → Γ ⊢ A ⇒*Π A ^ r
  _⇨_ : ∀ {t t' u r}
      → Γ ⊢ t  ⇒Π t' ^ r
      → Γ ⊢ t' ⇒*Π u ^ r
      → Γ ⊢ t  ⇒*Π u ^ r

_⇨*_ : ∀ {Γ A B C r} → Γ ⊢ A ⇒*Π B ^ r → Γ ⊢ B ⇒*Π C ^ r → Γ ⊢ A ⇒*Π C ^ r
id ⇨* y = y
(x ⇨ x₁) ⇨* y = x ⇨ (x₁ ⇨* y)

regular* : ∀ {Γ t u r} → Γ ⊢ t ⇒* u ^ r → Γ ⊢ t ⇒*Π u ^ r
regular* (id _) = id
regular* (univ x ⇨ x₁) = univ (regular x) ⇨ regular* x₁

deep* : ∀ {Γ F rF lF G G′ lG rG lΠ}
      → Γ ∙ F ^ [ rF , ι lF ] ⊢ G ⇒*Π G′ ^ [ rG , ι lG ]
      → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° lΠ ⇒*Π Π F ^ rF ° lF ▹ G′ ° lG ° lΠ ^ [ rG , ι lΠ ]
deep* id = id
deep* (univ (regular x) ⇨ x₁) = univ (deepΠ (regular x)) ⇨ deep* x₁
deep* (univ (deepΠ x) ⇨ x₁) = univ (deepΠ (deepΠ x)) ⇨ deep* x₁
deep* (univ (deep∃ x) ⇨ x₁) = univ (deepΠ (deep∃ x)) ⇨ deep* x₁

deep∃* : ∀ {Γ F G F′ l∃}
      → Γ ⊢ F ⇒*Π F′ ^ [ % , ι l∃ ]
      → Γ ⊢ ∃ F ▹ G ⇒*Π ∃ F′ ▹ G ^ [ % , ι l∃ ]
deep∃* id = id
deep∃* (univ (regular x) ⇨ x₁) = univ (deep∃ (regular x)) ⇨ deep∃* x₁
deep∃* (univ (deepΠ x) ⇨ x₁) = univ (deep∃ (deepΠ x)) ⇨ deep∃* x₁
deep∃* (univ (deep∃ x) ⇨ x₁) = univ (deep∃ (deep∃ x)) ⇨ deep∃* x₁

deep-correct-term : ∀ {Γ t u T l} → Γ ⊢ t ∷ T ^ [ ! , l ] → Γ ⊢ t ⇒Π u ∷ T ^ l → Γ ⊢ u ∷ T ^ [ ! , l ] × Γ ⊢ t ≡ u ∷ T ^ [ ! , l ]
deep-correct-term ⊢t (regular x) =
  let t≡u = subsetTerm x
      _ , _ , ⊢u = syntacticEqTerm t≡u
  in ⊢u , t≡u
deep-correct-term ⊢t (deepΠ X) =
  let _ , l< , l<' , ⊢F , ⊢G , e , _ = inversion-Π ⊢t
      erG , _ = Uinjectivity e
      ⊢G' , G≡G' = deep-correct-term (PE.subst (λ rr → _ ⊢ _ ∷ Univ rr _ ^ _ ) (PE.sym erG) ⊢G) X
  in Πⱼ l< ▹ l<' ▹ ⊢F ▹ ⊢G' , Π-cong l< l<' (univ ⊢F) (refl ⊢F) G≡G'
deep-correct-term ⊢t (deep∃ X) =
  let l , ⊢F , ⊢G , e , _ = inversion-∃ ⊢t
      _ , el = Uinjectivity e
      ⊢Fl = PE.subst (λ ll → _ ⊢ _ ∷ SProp ll ^ [ ! , next ll ] ) (PE.sym el) ⊢F
      ⊢F' , F≡F' = deep-correct-term ⊢Fl X
      ⊢Gl = PE.subst (λ ll → _ ∙ _ ^ [ % , ι ll ] ⊢ _ ∷ SProp ll ^ [ ! , next ll ] ) (PE.sym el) ⊢G
  in ∃ⱼ ⊢F' ▹ stabilityTerm (reflConEq (wfTerm ⊢F) ∙ (univ F≡F')) ⊢Gl , ∃-cong (univ ⊢Fl) F≡F' (refl ⊢Gl)

deep-correct : ∀ {Γ A B r} → Γ ⊢ A ^ r → Γ ⊢ A ⇒Π B ^ r → Γ ⊢ B ^ r × Γ ⊢ A ≡ B ^ r
deep-correct ⊢A (univ x) =
  let ⊢B , A≡B = deep-correct-term (un-univ ⊢A) x
  in univ ⊢B , univ A≡B

deep*-correct-term : ∀ {Γ t u T l} → Γ ⊢ t ∷ T ^ [ ! , l ] → Γ ⊢ t ⇒*Π u ∷ T ^ l → Γ ⊢ t ≡ u ∷ T ^ [ ! , l ]
deep*-correct-term ⊢t id = refl ⊢t
deep*-correct-term ⊢t (x ⇨ X) =
  let ⊢u , t≡u = deep-correct-term ⊢t x
  in trans t≡u (deep*-correct-term ⊢u X)

deep*-correct : ∀ {Γ A B r} → Γ ⊢ A ^ r → Γ ⊢ A ⇒*Π B ^ r → Γ ⊢ A ≡ B ^ r
deep*-correct ⊢A id = refl ⊢A
deep*-correct ⊢A (x ⇨ X) =
  let ⊢B , A≡B = deep-correct ⊢A x
  in trans A≡B (deep*-correct ⊢B X)

doΠNorm′ : ∀ {A rA Γ l} ([A] : Γ ⊩⟨ l ⟩ A ^ rA)
         → ∃ λ B → ΠNorm B × Γ ⊢ B ^ rA × Γ ⊢ A ⇒*Π B ^ rA
doΠNorm′ (Uᵣ (Uᵣ r l′ l< PE.refl [[ A , U , d ]])) = Univ r l′ , Uₙ , Ugenⱼ (wf A) , regular* d
doΠNorm′ (ℕᵣ [[ ⊢A , ⊢B , D ]]) = ℕ , ℕₙ , ⊢B , regular* D
doΠNorm′ (Emptyᵣ {l = l} [[ ⊢A , ⊢B , D ]]) = Empty l , Emptyₙ , ⊢B , regular* D
doΠNorm′ (ne′ K [[ ⊢A , ⊢B , D ]] neK K≡K) = K , ne neK , ⊢B , regular* D
doΠNorm′ (Πᵣ′ rF lF lG lF≤ lG≤ F G [[ ⊢A , ⊢B , D ]] ⊢F ⊢G A≡A [F] [G] G-ext) =
  let redF₀ , red₀ = reducibleTerm (var (wf ⊢G) here)
      [F]′ = irrelevanceTerm redF₀ ([F] (step id) (wf ⊢G)) red₀
      G′ , nG′ , ⊢G′ , D′ = PE.subst (λ G′ → ∃ λ B → ΠNorm B × _ ⊢ B ^ _ × _ ⊢ G′ ⇒*Π B ^ _)
                              (wkSingleSubstId _)
                              (doΠNorm′ ([G] (step id) (wf ⊢G) [F]′))
  in Π F ^ rF ° lF ▹ G′ ° lG ° _ , Πₙ nG′ , univ (Πⱼ lF≤ ▹ lG≤ ▹ (un-univ ⊢F) ▹ (un-univ ⊢G′)) , regular* D ⇨* deep* D′
doΠNorm′ (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) =
  let F′ , nF′ ,  ⊢F′ , D′ = doΠNorm′ ([F] id (wf ⊢F))
      DD = (PE.subst (λ FF → _ ⊢ FF ⇒*Π F′ ^ _ ) (wk-id _) D′)
      F≡F′ = deep*-correct ⊢F DD
  in ∃ F′ ▹ G , ∃ₙ nF′ , univ (∃ⱼ un-univ ⊢F′ ▹ un-univ (stability (reflConEq (wf ⊢F) ∙ F≡F′) ⊢G)) ,
     regular* (red D) ⇨* deep∃* DD
doΠNorm′ (emb emb< [A]) = doΠNorm′ [A]
doΠNorm′ (emb ∞< [A]) = doΠNorm′ [A]

doΠNorm : ∀ {A rA Γ} → Γ ⊢ A ^ rA
        → ∃ λ B → ΠNorm B × Γ ⊢ B ^ rA × Γ ⊢ A ⇒*Π B ^ rA
doΠNorm ⊢A = doΠNorm′ (reducible ⊢A)

ΠNorm-whnf : ∀ {A} → ΠNorm A → Whnf A
ΠNorm-whnf Uₙ = Uₙ
ΠNorm-whnf (Πₙ _) = Πₙ
ΠNorm-whnf (∃ₙ _) = ∃ₙ
ΠNorm-whnf ℕₙ = ℕₙ
ΠNorm-whnf Emptyₙ = Emptyₙ
ΠNorm-whnf (ne x) = ne x

ΠNorm-noredTerm : ∀ {Γ A B T r} → Γ ⊢ A ⇒Π B ∷ T ^ r  → ΠNorm A → ⊥
ΠNorm-noredTerm (regular x) w = whnfRedTerm x (ΠNorm-whnf w)
ΠNorm-noredTerm (deepΠ x) (Πₙ w) = ΠNorm-noredTerm x w
ΠNorm-noredTerm (deepΠ x) (ne ())
ΠNorm-noredTerm (deep∃ x) (∃ₙ w) = ΠNorm-noredTerm x w
ΠNorm-noredTerm (deep∃ x) (ne ())

ΠNorm-nored : ∀ {Γ A B r} → Γ ⊢ A ⇒Π B ^ r → ΠNorm A → ⊥
ΠNorm-nored (univ x) w = ΠNorm-noredTerm x w

detΠRedTerm : ∀ {Γ A B B′ T T′ r r'} → Γ ⊢ A ⇒Π B ∷ T ^ r  → Γ ⊢ A ⇒Π B′ ∷ T′ ^ r' → B PE.≡ B′
detΠRedTerm (regular x) (regular x₁) = whrDetTerm x x₁
detΠRedTerm (regular x) (deepΠ y) = ⊥-elim (whnfRedTerm x Πₙ)
detΠRedTerm (deepΠ x) (regular x₁) = ⊥-elim (whnfRedTerm x₁ Πₙ)
detΠRedTerm (deepΠ x) (deepΠ y) = PE.cong _ (detΠRedTerm x y)
detΠRedTerm (regular x) (deep∃ y) = ⊥-elim (whnfRedTerm x ∃ₙ)
detΠRedTerm (deep∃ x) (regular x₁) = ⊥-elim (whnfRedTerm x₁ ∃ₙ)
detΠRedTerm (deep∃ x) (deep∃ y) = PE.cong _ (detΠRedTerm x y)

detΠRed : ∀ {Γ A B B′ r r′} → Γ ⊢ A ⇒Π B ^ r → Γ ⊢ A ⇒Π B′ ^ r′ → B PE.≡ B′
detΠRed (univ x) (univ y) = detΠRedTerm x y

detΠNorm* : ∀ {Γ A B B′ r r′} → ΠNorm B → ΠNorm B′ → Γ ⊢ A ⇒*Π B ^ r → Γ ⊢ A ⇒*Π B′ ^ r′ → B PE.≡ B′
detΠNorm* w w′ id id = PE.refl
detΠNorm* w w′ id (x ⇨ b) = ⊥-elim (ΠNorm-nored x w)
detΠNorm* w w′ (x ⇨ a) id = ⊥-elim (ΠNorm-nored x w′)
detΠNorm* w w′ (x ⇨ a) (x₁ ⇨ b) =
  detΠNorm* w w′ a (PE.subst (λ t → _ ⊢ t ⇒*Π _ ^ _) (detΠRed x₁ x) b)

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Grothendieck where

open import Relation.Binary using (Rel)
open import Data.Product using (Σ; _,_; proj₁; proj₂; _×_)

open import Categories.Support.Experimental
open import Categories.Support.PropositionalEquality
open import Categories.Support.IProduct
import Categories.Category as CCat
open CCat hiding (module Heterogeneous)
open import Categories.Functor using (Functor; module Functor; ≡⇒≣)
open import Categories.Agda
open import Categories.Categories
open import Categories.Congruence

-- TODO: don't use sigmas
-- Break into modules Strict and Weak using Sets and Setoids?
Elements : ∀ {o ℓ e o′} {C : Category o ℓ e} → Functor C (Sets o′) → Category _ _ _
Elements {o′ = o′} {C = C} F = record
  { Obj = Obj′
  ; _⇒_ = Hom′
  ; _≡_ = _≡′_
  ; _∘_ = _∘′_
  ; id = id , identity
  ; assoc = assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; equiv = record
    { refl = refl
    ; sym = sym
    ; trans = trans
    }
  ; ∘-resp-≡ = ∘-resp-≡
  }
  where
  open Category C
  open Equiv
  open Functor F

  Obj′ = Σ Obj F₀

  Hom′ : Rel Obj′ _
  Hom′ (c₁ , x₁) (c₂ , x₂) = Σ′ (c₁ ⇒ c₂) (λ f → F₁ f x₁ ≣ x₂)

  _≡′_ : ∀ {X Y} → Rel (Hom′ X Y) _
  (f , pf₁) ≡′ (g , pf₂) = f ≡ g

  _∘′_ : ∀ {X Y Z} → Hom′ Y Z → Hom′ X Y → Hom′ X Z
  _∘′_ {X} {Y} {Z} (f , pf₁) (g , pf₂) = (f ∘ g) , pf
    where
    -- This could be a lot prettier...
    .pf : F₁ (f ∘ g) (proj₂ X) ≣ proj₂ Z
    pf = ≣-trans homomorphism (≣-sym (≣-trans (≣-sym pf₁) (≣-cong (F₁ f) (≣-sym pf₂))))

Dom : ∀ {o ℓ e o′} {C : Category o ℓ e} → (F : Functor C (Sets o′)) -> Functor (Elements F) C
Dom {C = C} F = record {
                  F₀ = proj₁;
                  F₁ = proj₁′;
                  identity = Equiv.refl;
                  homomorphism = Equiv.refl;
                  F-resp-≡ = λ x → x }
  where
   open Category C

-- because we want the following function to reduce all the time, define it globally
private
  module _ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} (F : Functor C (Categories o′ ℓ′ e′)) where
    private
      module C = Category C
      module F = Functor F
      module Cat = Category (Categories o′ ℓ′ e′)

    ∘-eq : ∀ {cx xx cy cz} -> (f : cy C.⇒ cz) (g : cx C.⇒ cy) -> Functor.F₀ (F.F₁ f Cat.∘ F.F₁ g) xx ≣ Functor.F₀ (F.F₁ (f C.∘ g)) xx
    ∘-eq {cx} {xx} {cy} {cz} f g = ≣-relevant (≣-sym (≡⇒≣ (F.F₁ (f C.∘ g)) (F.F₁ f Cat.∘ F.F₁ g) (F.homomorphism {f = g} {g = f}) xx))

Grothendieck : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} → Functor C (Categories o′ ℓ′ e′) → Category _ _ _
Grothendieck {o′ = o′} {ℓ′} {e′} {C = C} F = record
  { Obj = Obj′
  ; _⇒_ = Hom′
  ; _≡_ = _≡′_
  ; _∘_ = _∘′_
  ; id = id′
  ; assoc = assoc′
  ; identityˡ = identityˡ′
  ; identityʳ = identityʳ′
  ; equiv = record {
     refl = refl , Het.refl;
     sym  = λ { (eq₁ , eq₂) → sym eq₁ , Het.sym eq₂};
     trans = λ { (xeq₁ , xeq₂) (yeq₁ , yeq₂) → trans xeq₁ yeq₁ , Het.trans xeq₂ yeq₂} }
  ; ∘-resp-≡ = ∘-resp-≡′
  }
  module Groth where
  open Functor F
  module Fc {c} where
    open Category (F₀ c) public
    open Equiv public
  open Category C
  open Equiv
  module Cat = Category (Categories o′ ℓ′ e′)
  module Cong {c} where
   open Congruence (TrivialCongruence (F₀ c)) public
  open Cong public using () renaming (coerce to coe)
  module Het {c} = Heterogeneous (TrivialCongruence (F₀ c))
  open Het using (▹_)
  module OHet {c} where
   open CCat.Heterogeneous (F₀ c) public
   ohet⇒het : ∀ {A B} {f : A Fc.⇒ B} -> ∀ {X Y} → {g : X Fc.⇒ Y} → f ∼ g -> f Het.∼ g
   ohet⇒het (≡⇒∼ x) = Het.≡⇒∼ ≣-refl ≣-refl x

  Obj′ = Σ Obj (\ c -> Category.Obj (F₀ c))

  Hom′ : Rel Obj′ _
  Hom′ (c₁ , x₁) (c₂ , x₂) = Σ (c₁ ⇒ c₂) (λ f → Functor.F₀ (F₁ f) x₁ Fc.⇒ x₂)

  _≡′_ : ∀ {X Y} → Rel (Hom′ X Y) _
  _≡′_ {c₁ , x₁} {c₂ , x₂} (f , α) (g , β) = f ≡ g × α Het.∼ β

  _∘′_ : ∀ {X Y Z} → Hom′ Y Z → Hom′ X Y → Hom′ X Z
  _∘′_ {cx , xx} {Y} {cz , xz} (f , α) (g , β) = (f ∘ g) , α Fc.∘ Cong.coerce (∘-eq F f g) ≣-refl (Functor.F₁ (F₁ f) β)

  id-eq : ∀ {c x} -> Functor.F₀ (Cat.id {F₀ c}) x ≣ Functor.F₀ (F₁ id) x
  id-eq {c} {x} = ≣-relevant (≣-sym (≡⇒≣ (F₁ id) Cat.id (identity {c}) x))

  id′ : {A : Obj′} → Hom′ A A
  id′ {c , x} = id , Cong.coerce id-eq ≣-refl Fc.id

  F-resp-∼ : ∀ {b c} -> (H : Functor (F₀ b) (F₀ c)) -> {A B A' B' : Category.Obj (F₀ b)} {α : A Fc.⇒ B }{β : A' Fc.⇒ B'} →
             (α Het.∼ β) → (Functor.F₁ H α Het.∼ Functor.F₁ H β)
  F-resp-∼ H (Heterogeneous.≡⇒∼ ≣-refl ≣-refl x) = Heterogeneous.≡⇒∼ ≣-refl ≣-refl (Functor.F-resp-≡ H x)

  .identityˡ′ : {A B : Obj′} {f : Hom′ A B} → (id′ ∘′ f) ≡′ f
  identityˡ′ {ca , xa} {cb , xb} {f , α} = identityˡ , (begin
    ▹ coe id-eq ≣-refl Fc.id Fc.∘ coe (∘-eq F id f) ≣-refl (Functor.F₁ (F₁ id) α)
      ↓⟨ Het.∘-resp-∼ (Het.sym (Het.coerce-resp-∼ id-eq ≣-refl)) F₁id[α]~α ⟩
    ▹ Fc.id Fc.∘ α
      ↓⟨ Het.≡⇒∼ ≣-refl ≣-refl Fc.identityˡ ⟩
    ▹ α
      ∎)
   where
    open Het.HetReasoning
    F₁id[α]~α : coe (∘-eq F id f) ≣-refl (Functor.F₁ (F₁ id) α) Het.∼ α
    F₁id[α]~α = begin
      ▹ coe (∘-eq F id f) ≣-refl (Functor.F₁ (F₁ id) α)
        ↑⟨ Het.coerce-resp-∼ (∘-eq F id f) ≣-refl ⟩
      ▹ Functor.F₁ (F₁ id) α
        ↓⟨ OHet.ohet⇒het (identity α) ⟩
      ▹ α
        ∎

  .identityʳ′ : {A B : Obj′} {f : Hom′ A B} → (f ∘′ id′) ≡′ f
  identityʳ′ {ca , xa} {cb , xb} {f , α} = identityʳ , (begin
    ▹ α Fc.∘ coe (∘-eq F f id) ≣-refl (Functor.F₁ (F₁ f) (coe id-eq ≣-refl Fc.id))
       ↓⟨ Het.∘-resp-∼ʳ F₁f[id]~id ⟩
    ▹ α Fc.∘ Fc.id
       ↓⟨ Het.≡⇒∼ ≣-refl ≣-refl Fc.identityʳ ⟩
    ▹ α
       ∎)
   where
    open Het.HetReasoning
    F₁f[id]~id : coe (∘-eq F f id) ≣-refl (Functor.F₁ (F₁ f) (coe id-eq ≣-refl Fc.id)) Het.∼ Fc.id
    F₁f[id]~id = begin
      ▹ coe (∘-eq F f id) ≣-refl (Functor.F₁ (F₁ f) (coe id-eq ≣-refl Fc.id))
        ↑⟨ Het.coerce-resp-∼ (∘-eq F f id) ≣-refl ⟩
      ▹ Functor.F₁ (F₁ f) (coe id-eq ≣-refl Fc.id)
        ↓⟨ F-resp-∼ (F₁ f) (Het.sym (Het.coerce-resp-∼ id-eq ≣-refl)) ⟩
      ▹ Functor.F₁ (F₁ f) (Category.id (F₀ ca))
        ↓⟨ Het.≡⇒∼ ≣-refl ≣-refl (Functor.identity (F₁ f)) ⟩
      ▹ Fc.id
        ∎

  .assoc′ : {A B C₁ D : Obj′} {f : Hom′ A B} {g : Hom′ B C₁} {h : Hom′ C₁ D} →
                 ((h ∘′ g) ∘′ f) ≡′ (h ∘′ (g ∘′ f))
  assoc′ {ca , xa} {cb , xb} {cc , xc} {cd , xd} {f , α} {g , β} {h , γ}
    = assoc , Het.trans (Het.≡⇒∼ ≣-refl ≣-refl Fc.assoc) (Het.∘-resp-∼ʳ F₁h[β]∘F₁h∘g[α]~F₁h[β∘F₁g[α]])
   where
    open Het.HetReasoning
    eq : Functor.F₀ (F₁ ((h ∘ g) ∘ f)) xa ≣ Functor.F₀ (F₁ (h ∘ g ∘ f)) xa
    eq = ≡⇒≣ (F₁ ((h ∘ g) ∘ f)) (F₁ (h ∘ g ∘ f)) (F-resp-≡ (assoc {f = f})) xa

    F₁h[β]∘F₁h∘g[α]~F₁h[β∘F₁g[α]] : (coe (∘-eq F h g) ≣-refl (Functor.F₁ (F₁ h) β) Fc.∘ coe (∘-eq F (h ∘ g) f) ≣-refl (Functor.F₁ (F₁ (h ∘ g)) α))
                                     Het.∼ (coe (∘-eq F h (g ∘ f)) ≣-refl (Functor.F₁ (F₁ h) (proj₂ ((g , β) ∘′ (f , α)))))
    F₁h[β]∘F₁h∘g[α]~F₁h[β∘F₁g[α]] = Het.sym (begin
      ▹ coe (∘-eq F h (g ∘ f)) ≣-refl (Functor.F₁ (F₁ h) (β Fc.∘ coe(∘-eq F g f) ≣-refl (Functor.F₁ (F₁ g) α)))
        ↑⟨ Het.coerce-resp-∼ (∘-eq F h (g ∘ f)) ≣-refl ⟩
      ▹ Functor.F₁ (F₁ h) (β Fc.∘ coe (∘-eq F g f) ≣-refl (Functor.F₁ (F₁ g) α))
        ↓⟨ Het.≡⇒∼ ≣-refl ≣-refl (Functor.homomorphism (F₁ h)) ⟩
      ▹ Functor.F₁ (F₁ h) β Fc.∘ (Functor.F₁ (F₁ h) (coe (∘-eq F g f) ≣-refl (Functor.F₁ (F₁ g) α)))
        ↓⟨ Het.∘-resp-∼ (Het.coerce-resp-∼ (∘-eq F h g) ≣-refl) F₁h[β]~F₁h∘g[α] ⟩
      ▹ coe (∘-eq F h g) ≣-refl (Functor.F₁ (F₁ h) β) Fc.∘ coe (∘-eq F (h ∘ g) f) ≣-refl (Functor.F₁ (F₁ (h ∘ g)) α)
        ∎)
     where
      F₁h[β]~F₁h∘g[α] : (Functor.F₁ (F₁ h) (coe (∘-eq F g f) ≣-refl (Functor.F₁ (F₁ g) α))) Het.∼ coe (∘-eq F (h ∘ g) f) ≣-refl (Functor.F₁ (F₁ (h ∘ g)) α)
      F₁h[β]~F₁h∘g[α] = begin
        ▹ Functor.F₁ (F₁ h) (coe (∘-eq F g f) ≣-refl (Functor.F₁ (F₁ g) α))
          ↓⟨ F-resp-∼ (F₁ h) (Het.sym (Het.coerce-resp-∼ (∘-eq F g f) ≣-refl)) ⟩
        ▹ Functor.F₁ (F₁ h) (Functor.F₁ (F₁ g) α)
          ↑⟨ OHet.ohet⇒het (homomorphism α) ⟩
        ▹ Functor.F₁ (F₁ (h ∘ g)) α
          ↓⟨ Het.coerce-resp-∼ (∘-eq F (h ∘ g) f) ≣-refl ⟩
        ▹ coe (∘-eq F (h ∘ g) f) ≣-refl (Functor.F₁ (F₁ (h ∘ g)) α)
          ∎

  .∘-resp-≡′ : {A B C₁ : Obj′} {f h : Hom′ B C₁} {g i : Hom′ A B} →
                     f ≡′ h → g ≡′ i → (f ∘′ g) ≡′ (h ∘′ i)
  ∘-resp-≡′ {a , ax} {b , bx} {c , cx} {f = f , α} {h , η} {g , γ} {i , ι} (f≡h , α~η) (g≡i , γ~ι) = ∘-resp-≡ f≡h g≡i , Het.∘-resp-∼ α~η
    (begin
     ▹ coe (∘-eq F f g) ≣-refl (Functor.F₁ (F₁ f) γ) ↑⟨ Het.coerce-resp-∼ (∘-eq F f g) ≣-refl ⟩
     ▹ Functor.F₁ (F₁ f) γ                           ↓⟨ OHet.ohet⇒het (F-resp-≡ f≡h γ) ⟩
     ▹ Functor.F₁ (F₁ h) γ                           ↓⟨ F-resp-∼ (F₁ h) γ~ι ⟩
     ▹ Functor.F₁ (F₁ h) ι                           ↓⟨ Het.coerce-resp-∼ (∘-eq F h i) ≣-refl ⟩
     ▹ coe (∘-eq F h i) ≣-refl (Functor.F₁ (F₁ h) ι) ∎)
   where
    open Het.HetReasoning

Gr = Grothendieck

DomGr : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} → (F : Functor C (Categories o′ ℓ′ e′)) → Functor (Grothendieck F) C
DomGr {C = C} F = record {
                    F₀ = proj₁;
                    F₁ = proj₁;
                    identity = C.Equiv.refl;
                    homomorphism = C.Equiv.refl;
                    F-resp-≡ = proj₁ }
  where
    module C = Category C

inGr : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} (F : Functor C (Categories o′ ℓ′ e′)) → ∀ c -> Functor (Functor.F₀ F c) (Gr F)
inGr {C = C} F c = record {
                     F₀ = _,_ c;
                     F₁ = λ f → C.id , GrF.coe GrF.id-eq ≣-refl f;
                     identity = Category.Equiv.refl (Grothendieck F);
                     homomorphism = C.Equiv.sym C.identityʳ , Het.trans (Het.sym (Het.coerce-resp-∼ GrF.id-eq ≣-refl))
                                                                (Het.∘-resp-∼ (Het.coerce-resp-∼ GrF.id-eq ≣-refl)
                                                                 (Het.trans
                                                                  (Het.trans (Het.coerce-resp-∼ GrF.id-eq ≣-refl)
                                                                   (Het.sym (GrF.OHet.ohet⇒het (F.identity _))))
                                                                  (Het.coerce-resp-∼ (∘-eq F C.id C.id) ≣-refl)));
                     F-resp-≡ = λ x → C.Equiv.refl , (Het.trans (Het.trans (Het.sym (Het.coerce-resp-∼ GrF.id-eq ≣-refl))
                              (Heterogeneous.≡⇒∼ ≣-refl ≣-refl x)) (Het.coerce-resp-∼ GrF.id-eq ≣-refl)) }
  where
    module C = Category C
    module F = Functor F
    module GrF = Groth F
    open GrF using (module Het; module Cong)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A bunch of properties
------------------------------------------------------------------------

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

module Data.Bool.Properties where

open import Algebra
open import Data.Bool.Base
open import Data.Empty
open import Data.Product
open import Data.Sum
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence
  using (_⇔_; equivalence; module Equivalence)
open import Level using (0ℓ)
open import Relation.Binary.Core using (Decidable)
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable using (True)
open import Relation.Unary as U using (Irrelevant)

open import Algebra.FunctionProperties (_≡_ {A = Bool})
open import Algebra.Structures (_≡_ {A = Bool})
open ≡-Reasoning

------------------------------------------------------------------------
-- Queries

infix 4 _≟_

_≟_ : Decidable {A = Bool} _≡_
true  ≟ true  = yes refl
false ≟ false = yes refl
true  ≟ false = no λ()
false ≟ true  = no λ()

------------------------------------------------------------------------
-- Properties of _∨_

∨-assoc : Associative _∨_
∨-assoc true  y z = refl
∨-assoc false y z = refl

∨-comm : Commutative _∨_
∨-comm true  true  = refl
∨-comm true  false = refl
∨-comm false true  = refl
∨-comm false false = refl

∨-identityˡ : LeftIdentity false _∨_
∨-identityˡ _ = refl

∨-identityʳ : RightIdentity false _∨_
∨-identityʳ false = refl
∨-identityʳ true  = refl

∨-identity : Identity false _∨_
∨-identity = ∨-identityˡ , ∨-identityʳ

∨-zeroˡ : LeftZero true _∨_
∨-zeroˡ _ = refl

∨-zeroʳ : RightZero true _∨_
∨-zeroʳ false = refl
∨-zeroʳ true  = refl

∨-zero : Zero true _∨_
∨-zero = ∨-zeroˡ , ∨-zeroʳ

∨-inverseˡ : LeftInverse true not _∨_
∨-inverseˡ false = refl
∨-inverseˡ true  = refl

∨-inverseʳ : RightInverse true not _∨_
∨-inverseʳ x = ∨-comm x (not x) ⟨ trans ⟩ ∨-inverseˡ x

∨-inverse : Inverse true not _∨_
∨-inverse = ∨-inverseˡ , ∨-inverseʳ

∨-idem : Idempotent _∨_
∨-idem false = refl
∨-idem true  = refl

∨-sel : Selective _∨_
∨-sel false y = inj₂ refl
∨-sel true y  = inj₁ refl

∨-isMagma : IsMagma _∨_
∨-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = cong₂ _∨_
  }

∨-magma : Magma 0ℓ 0ℓ
∨-magma = record
  { isMagma = ∨-isMagma
  }

∨-isSemigroup : IsSemigroup _∨_
∨-isSemigroup = record
  { isMagma = ∨-isMagma
  ; assoc   = ∨-assoc
  }

∨-semigroup : Semigroup 0ℓ 0ℓ
∨-semigroup = record
  { isSemigroup = ∨-isSemigroup
  }

∨-isBand : IsBand _∨_
∨-isBand = record
  { isSemigroup = ∨-isSemigroup
  ; idem        = ∨-idem
  }

∨-band : Band 0ℓ 0ℓ
∨-band = record
  { isBand = ∨-isBand
  }

∨-isSemilattice : IsSemilattice _∨_
∨-isSemilattice = record
  { isBand = ∨-isBand
  ; comm   = ∨-comm
  }

∨-semilattice : Semilattice 0ℓ 0ℓ
∨-semilattice = record
  { isSemilattice = ∨-isSemilattice
  }

∨-isCommutativeMonoid : IsCommutativeMonoid _∨_ false
∨-isCommutativeMonoid = record
  { isSemigroup = ∨-isSemigroup
  ; identityˡ   = ∨-identityˡ
  ; comm        = ∨-comm
  }

∨-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
∨-commutativeMonoid = record
  { isCommutativeMonoid = ∨-isCommutativeMonoid
  }

∨-isIdempotentCommutativeMonoid :
  IsIdempotentCommutativeMonoid _∨_ false
∨-isIdempotentCommutativeMonoid = record
    { isCommutativeMonoid = ∨-isCommutativeMonoid
   ; idem = ∨-idem
   }

∨-idempotentCommutativeMonoid : IdempotentCommutativeMonoid 0ℓ 0ℓ
∨-idempotentCommutativeMonoid = record
  { isIdempotentCommutativeMonoid = ∨-isIdempotentCommutativeMonoid
  }

------------------------------------------------------------------------
-- Properties of _∧_

∧-assoc : Associative _∧_
∧-assoc true  y z = refl
∧-assoc false y z = refl

∧-comm : Commutative _∧_
∧-comm true  true  = refl
∧-comm true  false = refl
∧-comm false true  = refl
∧-comm false false = refl

∧-identityˡ : LeftIdentity true _∧_
∧-identityˡ _ = refl

∧-identityʳ : RightIdentity true _∧_
∧-identityʳ false = refl
∧-identityʳ true  = refl

∧-identity : Identity true _∧_
∧-identity = ∧-identityˡ , ∧-identityʳ

∧-zeroˡ : LeftZero false _∧_
∧-zeroˡ _ = refl

∧-zeroʳ : RightZero false _∧_
∧-zeroʳ false = refl
∧-zeroʳ true  = refl

∧-zero : Zero false _∧_
∧-zero = ∧-zeroˡ , ∧-zeroʳ

∧-inverseˡ : LeftInverse false not _∧_
∧-inverseˡ false = refl
∧-inverseˡ true = refl

∧-inverseʳ : RightInverse false not _∧_
∧-inverseʳ x = ∧-comm x (not x) ⟨ trans ⟩ ∧-inverseˡ x

∧-inverse : Inverse false not _∧_
∧-inverse = ∧-inverseˡ , ∧-inverseʳ

∧-idem : Idempotent _∧_
∧-idem false = refl
∧-idem true  = refl

∧-sel : Selective _∧_
∧-sel false y = inj₁ refl
∧-sel true y  = inj₂ refl

∧-distribˡ-∨ : _∧_ DistributesOverˡ _∨_
∧-distribˡ-∨ true  y z = refl
∧-distribˡ-∨ false y z = refl

∧-distribʳ-∨ : _∧_ DistributesOverʳ _∨_
∧-distribʳ-∨ x y z = begin
  (y ∨ z) ∧ x     ≡⟨ ∧-comm (y ∨ z) x ⟩
  x ∧ (y ∨ z)     ≡⟨ ∧-distribˡ-∨ x y z ⟩
  x ∧ y ∨ x ∧ z  ≡⟨ cong₂ _∨_ (∧-comm x y) (∧-comm x z) ⟩
  y ∧ x ∨ z ∧ x  ∎

∧-distrib-∨ : _∧_ DistributesOver _∨_
∧-distrib-∨ = ∧-distribˡ-∨ , ∧-distribʳ-∨

∨-distribˡ-∧ : _∨_ DistributesOverˡ _∧_
∨-distribˡ-∧ true  y z = refl
∨-distribˡ-∧ false y z = refl

∨-distribʳ-∧ : _∨_ DistributesOverʳ _∧_
∨-distribʳ-∧ x y z = begin
  (y ∧ z) ∨ x        ≡⟨ ∨-comm (y ∧ z) x ⟩
  x ∨ (y ∧ z)        ≡⟨ ∨-distribˡ-∧ x y z ⟩
  (x ∨ y) ∧ (x ∨ z)  ≡⟨ cong₂ _∧_ (∨-comm x y) (∨-comm x z) ⟩
  (y ∨ x) ∧ (z ∨ x)  ∎

∨-distrib-∧ : _∨_ DistributesOver _∧_
∨-distrib-∧ = ∨-distribˡ-∧ , ∨-distribʳ-∧

∧-abs-∨ : _∧_ Absorbs _∨_
∧-abs-∨ true  y = refl
∧-abs-∨ false y = refl

∨-abs-∧ : _∨_ Absorbs _∧_
∨-abs-∧ true  y = refl
∨-abs-∧ false y = refl

∨-∧-absorptive : Absorptive _∨_ _∧_
∨-∧-absorptive = ∨-abs-∧ , ∧-abs-∨

∧-isMagma : IsMagma _∧_
∧-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = cong₂ _∧_
  }

∧-magma : Magma 0ℓ 0ℓ
∧-magma = record
  { isMagma = ∧-isMagma
  }

∧-isSemigroup : IsSemigroup _∧_
∧-isSemigroup = record
  { isMagma = ∧-isMagma
  ; assoc   = ∧-assoc
  }

∧-semigroup : Semigroup 0ℓ 0ℓ
∧-semigroup = record
  { isSemigroup = ∧-isSemigroup
  }

∧-isBand : IsBand _∧_
∧-isBand = record
  { isSemigroup = ∧-isSemigroup
  ; idem        = ∧-idem
  }

∧-band : Band 0ℓ 0ℓ
∧-band = record
  { isBand = ∧-isBand
  }

∧-isSemilattice : IsSemilattice _∧_
∧-isSemilattice = record
  { isBand = ∧-isBand
  ; comm   = ∧-comm
  }

∧-semilattice : Semilattice 0ℓ 0ℓ
∧-semilattice = record
  { isSemilattice = ∧-isSemilattice
  }

∧-isCommutativeMonoid : IsCommutativeMonoid _∧_ true
∧-isCommutativeMonoid = record
  { isSemigroup = ∧-isSemigroup
  ; identityˡ   = ∧-identityˡ
  ; comm        = ∧-comm
  }

∧-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
∧-commutativeMonoid = record
  { isCommutativeMonoid = ∧-isCommutativeMonoid
  }

∧-isIdempotentCommutativeMonoid :
  IsIdempotentCommutativeMonoid _∧_ true
∧-isIdempotentCommutativeMonoid = record
  { isCommutativeMonoid = ∧-isCommutativeMonoid
  ; idem = ∧-idem
  }

∧-idempotentCommutativeMonoid : IdempotentCommutativeMonoid 0ℓ 0ℓ
∧-idempotentCommutativeMonoid = record
  { isIdempotentCommutativeMonoid = ∧-isIdempotentCommutativeMonoid
  }

∨-∧-isCommutativeSemiring
  : IsCommutativeSemiring _∨_ _∧_ false true
∨-∧-isCommutativeSemiring = record
  { +-isCommutativeMonoid = ∨-isCommutativeMonoid
  ; *-isCommutativeMonoid = ∧-isCommutativeMonoid
  ; distribʳ = ∧-distribʳ-∨
  ; zeroˡ    = ∧-zeroˡ
  }

∨-∧-commutativeSemiring : CommutativeSemiring 0ℓ 0ℓ
∨-∧-commutativeSemiring = record
  { _+_                   = _∨_
  ; _*_                   = _∧_
  ; 0#                    = false
  ; 1#                    = true
  ; isCommutativeSemiring = ∨-∧-isCommutativeSemiring
  }

∧-∨-isCommutativeSemiring
  : IsCommutativeSemiring _∧_ _∨_ true false
∧-∨-isCommutativeSemiring = record
  { +-isCommutativeMonoid = ∧-isCommutativeMonoid
  ; *-isCommutativeMonoid = ∨-isCommutativeMonoid
  ; distribʳ = ∨-distribʳ-∧
  ; zeroˡ    = ∨-zeroˡ
  }

∧-∨-commutativeSemiring : CommutativeSemiring 0ℓ 0ℓ
∧-∨-commutativeSemiring = record
  { _+_                   = _∧_
  ; _*_                   = _∨_
  ; 0#                    = true
  ; 1#                    = false
  ; isCommutativeSemiring = ∧-∨-isCommutativeSemiring
  }

∨-∧-isLattice : IsLattice _∨_ _∧_
∨-∧-isLattice = record
  { isEquivalence = isEquivalence
  ; ∨-comm        = ∨-comm
  ; ∨-assoc       = ∨-assoc
  ; ∨-cong        = cong₂ _∨_
  ; ∧-comm        = ∧-comm
  ; ∧-assoc       = ∧-assoc
  ; ∧-cong        = cong₂ _∧_
  ; absorptive    = ∨-∧-absorptive
  }

∨-∧-lattice : Lattice 0ℓ 0ℓ
∨-∧-lattice = record
  { isLattice = ∨-∧-isLattice
  }

∨-∧-isDistributiveLattice : IsDistributiveLattice _∨_ _∧_
∨-∧-isDistributiveLattice = record
  { isLattice     = ∨-∧-isLattice
  ; ∨-∧-distribʳ = ∨-distribʳ-∧
  }

∨-∧-distributiveLattice : DistributiveLattice 0ℓ 0ℓ
∨-∧-distributiveLattice = record
  { isDistributiveLattice = ∨-∧-isDistributiveLattice
  }

∨-∧-isBooleanAlgebra : IsBooleanAlgebra _∨_ _∧_ not true false
∨-∧-isBooleanAlgebra = record
  { isDistributiveLattice = ∨-∧-isDistributiveLattice
  ; ∨-complementʳ = ∨-inverseʳ
  ; ∧-complementʳ = ∧-inverseʳ
  ; ¬-cong        = cong not
  }

∨-∧-booleanAlgebra : BooleanAlgebra 0ℓ 0ℓ
∨-∧-booleanAlgebra = record
  { isBooleanAlgebra = ∨-∧-isBooleanAlgebra
  }

------------------------------------------------------------------------
-- Properties of _xor_

xor-is-ok : ∀ x y → x xor y ≡ (x ∨ y) ∧ not (x ∧ y)
xor-is-ok true  y = refl
xor-is-ok false y = sym (∧-identityʳ _)

xor-∧-commutativeRing : CommutativeRing 0ℓ 0ℓ
xor-∧-commutativeRing = commutativeRing
  where
  import Algebra.Properties.BooleanAlgebra as BA
  open BA ∨-∧-booleanAlgebra
  open XorRing _xor_ xor-is-ok

------------------------------------------------------------------------
-- Miscellaneous other properties

not-involutive : Involutive not
not-involutive true  = refl
not-involutive false = refl

not-¬ : ∀ {x y} → x ≡ y → x ≢ not y
not-¬ {true}  refl ()
not-¬ {false} refl ()

¬-not : ∀ {x y} → x ≢ y → x ≡ not y
¬-not {true}  {true}  x≢y = ⊥-elim (x≢y refl)
¬-not {true}  {false} _   = refl
¬-not {false} {true}  _   = refl
¬-not {false} {false} x≢y = ⊥-elim (x≢y refl)

⇔→≡ : {b₁ b₂ b : Bool} → b₁ ≡ b ⇔ b₂ ≡ b → b₁ ≡ b₂
⇔→≡ {true } {true }         hyp = refl
⇔→≡ {true } {false} {true } hyp = sym (Equivalence.to hyp ⟨$⟩ refl)
⇔→≡ {true } {false} {false} hyp = Equivalence.from hyp ⟨$⟩ refl
⇔→≡ {false} {true } {true } hyp = Equivalence.from hyp ⟨$⟩ refl
⇔→≡ {false} {true } {false} hyp = sym (Equivalence.to hyp ⟨$⟩ refl)
⇔→≡ {false} {false}         hyp = refl

T-≡ : ∀ {b} → T b ⇔ b ≡ true
T-≡ {false} = equivalence (λ ())       (λ ())
T-≡ {true}  = equivalence (const refl) (const _)

T-not-≡ : ∀ {b} → T (not b) ⇔ b ≡ false
T-not-≡ {false} = equivalence (const refl) (const _)
T-not-≡ {true}  = equivalence (λ ())       (λ ())

T-∧ : ∀ {b₁ b₂} → T (b₁ ∧ b₂) ⇔ (T b₁ × T b₂)
T-∧ {true}  {true}  = equivalence (const (_ , _)) (const _)
T-∧ {true}  {false} = equivalence (λ ())          proj₂
T-∧ {false} {_}     = equivalence (λ ())          proj₁

T-∨ : ∀ {b₁ b₂} → T (b₁ ∨ b₂) ⇔ (T b₁ ⊎ T b₂)
T-∨ {true}  {b₂}    = equivalence inj₁ (const _)
T-∨ {false} {true}  = equivalence inj₂ (const _)
T-∨ {false} {false} = equivalence inj₁ [ id , id ]

T-irrelevant : Irrelevant T
T-irrelevant {true}  _  _  = refl
T-irrelevant {false} () ()

T? : U.Decidable T
T? true  = yes _
T? false = no (λ ())

T?-diag : ∀ b → T b → True (T? b)
T?-diag true  _ = _
T?-diag false ()

push-function-into-if :
  ∀ {a b} {A : Set a} {B : Set b} (f : A → B) x {y z} →
  f (if x then y else z) ≡ (if x then f y else f z)
push-function-into-if _ true  = refl
push-function-into-if _ false = refl

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

-- Version 0.15

∧-∨-distˡ   = ∧-distribˡ-∨
{-# WARNING_ON_USAGE ∧-∨-distˡ
"Warning: ∧-∨-distˡ was deprecated in v0.15.
Please use ∧-distribˡ-∨ instead."
#-}
∧-∨-distʳ   = ∧-distribʳ-∨
{-# WARNING_ON_USAGE ∧-∨-distʳ
"Warning: ∧-∨-distʳ was deprecated in v0.15.
Please use ∧-distribʳ-∨ instead."
#-}
distrib-∧-∨ = ∧-distrib-∨
{-# WARNING_ON_USAGE distrib-∧-∨
"Warning: distrib-∧-∨ was deprecated in v0.15.
Please use ∧-distrib-∨ instead."
#-}
∨-∧-distˡ   = ∨-distribˡ-∧
{-# WARNING_ON_USAGE ∨-∧-distˡ
"Warning: ∨-∧-distˡ was deprecated in v0.15.
Please use ∨-distribˡ-∧ instead."
#-}
∨-∧-distʳ   = ∨-distribʳ-∧
{-# WARNING_ON_USAGE ∨-∧-distʳ
"Warning: ∨-∧-distʳ was deprecated in v0.15.
Please use ∨-distribʳ-∧ instead."
#-}
∨-∧-distrib = ∨-distrib-∧
{-# WARNING_ON_USAGE ∨-∧-distrib
"Warning: ∨-∧-distrib was deprecated in v0.15.
Please use ∨-distrib-∧ instead."
#-}
∨-∧-abs    = ∨-abs-∧
{-# WARNING_ON_USAGE ∨-∧-abs
"Warning: ∨-∧-abs was deprecated in v0.15.
Please use ∨-abs-∧ instead."
#-}
∧-∨-abs    = ∧-abs-∨
{-# WARNING_ON_USAGE ∧-∨-abs
"Warning: ∧-∨-abs was deprecated in v0.15.
Please use ∧-abs-∨ instead."
#-}
not-∧-inverseˡ = ∧-inverseˡ
{-# WARNING_ON_USAGE not-∧-inverseˡ
"Warning: not-∧-inverseˡ was deprecated in v0.15.
Please use ∧-inverseˡ instead."
#-}
not-∧-inverseʳ = ∧-inverseʳ
{-# WARNING_ON_USAGE not-∧-inverseʳ
"Warning: not-∧-inverseʳ was deprecated in v0.15.
Please use ∧-inverseʳ instead."
#-}
not-∧-inverse = ∧-inverse
{-# WARNING_ON_USAGE not-∧-inverse
"Warning: not-∧-inverse was deprecated in v0.15.
Please use ∧-inverse instead."
#-}
not-∨-inverseˡ = ∨-inverseˡ
{-# WARNING_ON_USAGE not-∨-inverseˡ
"Warning: not-∨-inverseˡ was deprecated in v0.15.
Please use ∨-inverseˡ instead."
#-}
not-∨-inverseʳ = ∨-inverseʳ
{-# WARNING_ON_USAGE not-∨-inverseʳ
"Warning: not-∨-inverseʳ was deprecated in v0.15.
Please use ∨-inverseʳ instead."
#-}
not-∨-inverse = ∨-inverse
{-# WARNING_ON_USAGE not-∨-inverse
"Warning: not-∨-inverse was deprecated in v0.15.
Please use ∨-inverse instead."
#-}
isCommutativeSemiring-∨-∧ = ∨-∧-isCommutativeSemiring
{-# WARNING_ON_USAGE isCommutativeSemiring-∨-∧
"Warning: isCommutativeSemiring-∨-∧ was deprecated in v0.15.
Please use ∨-∧-isCommutativeSemiring instead."
#-}
commutativeSemiring-∨-∧   =  ∨-∧-commutativeSemiring
{-# WARNING_ON_USAGE commutativeSemiring-∨-∧
"Warning: commutativeSemiring-∨-∧ was deprecated in v0.15.
Please use ∨-∧-commutativeSemiring instead."
#-}
isCommutativeSemiring-∧-∨ = ∧-∨-isCommutativeSemiring
{-# WARNING_ON_USAGE isCommutativeSemiring-∧-∨
"Warning: isCommutativeSemiring-∧-∨ was deprecated in v0.15.
Please use ∧-∨-isCommutativeSemiring instead."
#-}
commutativeSemiring-∧-∨   = ∧-∨-commutativeSemiring
{-# WARNING_ON_USAGE commutativeSemiring-∧-∨
"Warning: commutativeSemiring-∧-∨ was deprecated in v0.15.
Please use ∧-∨-commutativeSemiring instead."
#-}
isBooleanAlgebra          = ∨-∧-isBooleanAlgebra
{-# WARNING_ON_USAGE isBooleanAlgebra
"Warning: isBooleanAlgebra was deprecated in v0.15.
Please use ∨-∧-isBooleanAlgebra instead."
#-}
booleanAlgebra            = ∨-∧-booleanAlgebra
{-# WARNING_ON_USAGE booleanAlgebra
"Warning: booleanAlgebra was deprecated in v0.15.
Please use ∨-∧-booleanAlgebra instead."
#-}
commutativeRing-xor-∧     = xor-∧-commutativeRing
{-# WARNING_ON_USAGE commutativeRing-xor-∧
"Warning: commutativeRing-xor-∧ was deprecated in v0.15.
Please use xor-∧-commutativeRing instead."
#-}
proof-irrelevance = T-irrelevant
{-# WARNING_ON_USAGE proof-irrelevance
"Warning: proof-irrelevance was deprecated in v0.15.
Please use T-irrelevant instead."
#-}

-- Version 1.0

T-irrelevance = T-irrelevant
{-# WARNING_ON_USAGE T-irrelevance
"Warning: T-irrelevance was deprecated in v1.0.
Please use T-irrelevant instead."
#-}


text:
module STLCSF.Examples where

open import Data.Fin hiding (_+_)
open import Data.Product
open import Data.List
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.All
open import Data.Maybe
open import Data.Integer hiding (suc)

-- This file contains a few example programs for the definitional
-- interpreter for STLC using scopes and frames in Section 4.

open import Agda.Builtin.Nat hiding (_+_)
open import Relation.Binary.PropositionalEquality hiding ([_])

-- The identity function: λ x . x
module Id where

  open import STLCSF.Semantics 2
  open import ScopesFrames.ScopesFrames 2 Ty

  -- Whereas Agda can infer the structure of ordinary type contexts,
  -- the scope graph library represents scope graphs as "lookup
  -- tables".  Agda cannot straightforwardly infer the structure of a
  -- lookup table.  We spell it out.

  g : Graph
  g zero    = [] , [] -- root scope
  g (suc n) = [ unit ] , [ zero ] -- lexical scope for lambda

  -- Had we used the structural representation discussed in Section
  -- 4.2 ("A Note on Scope Representation"), Agda could infer the
  -- structure of scope graphs for STLC for us.  As summarized in that
  -- discussion, such a representation has other shortcomings, e.g.,
  -- when it comes to dealing with scope graphs that has actual graph
  -- structure (i.e. cyclic paths).
  --
  -- We assume that programs have been analyzed using the scope graph
  -- resolution calculus to construct scope graphs and replace named
  -- references with paths in programs.  In future work, we will
  -- explore how to automate this.  For now, we construct scope graphs
  -- manually.

  -- We load the syntax definition, specialized to our scope graph:
  open Syntax g
  open UsesGraph g

  idexpr : Expr zero (unit ⇒ unit)
  idexpr = ƛ {s' = suc zero} (var (path ([]) (here refl)))

  open UsesVal Val val-weaken

  -- Initial heap with an empty frame that is typed by the root scope:
  init-h : Heap [ zero ]
  init-h = ([] , []) ∷ []

  -- id () = ()
  test-idexpr : eval 2 (idexpr · unit) (here refl) init-h ≡ just (_ , _ , unit , _)
  test-idexpr = refl

module Curry where

  open import STLCSF.Semantics 3
  open import ScopesFrames.ScopesFrames 3 Ty

  -- Whereas Agda can infer the structure of ordinary type contexts,
  -- the scope graph library represents scope graphs as "lookup
  -- tables".  Agda cannot straightforwardly infer the structure of a
  -- lookup table.  We spell it out.

  g : Graph
  g zero          = [] , [] -- root scope
  g (suc (suc n)) = [ int ] , [ suc zero ] -- lexical scope for inner lambda
  g (suc n)       = [ int ] , [ zero ] -- lexical scope for outer

  -- Had we used the structural representation discussed in Section
  -- 4.2 ("A Note on Scope Representation"), Agda could infer the
  -- structure of scope graphs for STLC for us.  As summarized in that
  -- discussion, such a representation has other shortcomings, e.g.,
  -- when it comes to dealing with scope graphs that has actual graph
  -- structure (i.e. cyclic paths).
  --
  -- We assume that programs have been analyzed using the scope graph
  -- resolution calculus to construct scope graphs and replace named
  -- references with paths in programs.  In future work, we will
  -- explore how to automate this.  For now, we construct scope graphs
  -- manually.

  -- We load the syntax definition, specialized to our scope graph:
  open Syntax g
  open UsesGraph g

  -- curried addition: λ x . λ y . y + x
  curry+ : Expr zero (int ⇒ (int ⇒ int))
  curry+ = ƛ {s' = suc zero}
             (ƛ {s' = suc (suc zero)}
                (iop _+_
                     (var (path [] (here refl)))
                     (var (path ((here refl) ∷ []) (here refl)))))

  open UsesVal Val val-weaken

  -- Initial heap with an empty frame that is typed by the root scope:
  init-h : Heap [ zero ]
  init-h = ([] , []) ∷ []

  -- 1 + 1 = 2
  test-curry+ : eval 3 ((curry+ · (num (+ 1))) · (num (+ 1))) (here refl) init-h
                ≡ just (_ , _ , num (+ 2) , _)
  test-curry+ = refl


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

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Impl.OBM.Rust.RustTypes

module LibraBFT.Impl.OBM.Rust.Duration where

record Duration : Set where
  constructor Duration∙new

postulate -- TODO-1 : fromMillis, asMillis
  fromMillis : U64 → Duration
  asMillis   : Duration → U128


text:
module Category.Diagram where

open import Level renaming (suc to lsuc)

open import Equality.Eq
open import Setoid.Total
open import Category.Category
open import Category.Funct
open import Category.Preorder

-- Diagrams are functors from an index category J to a category ℂ.  We
-- think of J as the scheme of the diagram in ℂ.
record Diagram {l₁ l₂ : Level} (J : Cat {l₁}) (ℂ : Cat {l₂}) : Set (l₁ ⊔ l₂) where
  field
    diag : Functor J ℂ

-- A commutative diagram is a diagram from a preorder to a category ℂ.
-- The preorder axiom garauntees that any diagram must commute because
-- there is only one composition.  Mixing this with the fact that
-- functors preserve composition implies that there can only be one
-- composition in ℂ.  This definition goes against the references --
-- nLab and Awedoy's book -- that comm. diagrams must be functors from
-- posets.  In fact we can prove that a PO is enough.  See the next
-- module.
record Comm-Diagram {l₁ l₂ : Level} (J : PO {l₁}) (ℂ : Cat {l₂}) : Set (l₁ ⊔ l₂) where
  field
    diag : Diagram (po-cat J) ℂ

open Comm-Diagram

-- The underlying functor of a diagram.
UFunc : {l l' : Level}{J : PO {l}}{ℂ : Cat {l'}} → Comm-Diagram J ℂ → Functor (po-cat J) ℂ
UFunc D = Diagram.diag (diag D)

-- This module shows that comm. squares can be modeled by POs.
module Commutative-Squares where
  open 4PO

  record Comm-Square'
         {l : Level}
         (ℂ : Cat {l})
         (om : 4Obj → Obj ℂ)
         (g : el (Hom ℂ (om i₁) (om i₂)))
         (h : el (Hom ℂ (om i₂) (om i₄)))
         (j : el (Hom ℂ (om i₁) (om i₃)))
         (k : el (Hom ℂ (om i₃) (om i₄))) : Set l where
     field
       Sq : {a b : 4Obj {l}} → SetoidFun (4Hom a b) (Hom ℂ (om a) (om b))

       sq-max₁ : ⟨ Hom ℂ (om i₁) (om i₂) ⟩[ appT Sq f₁ ≡ g ]
       sq-max₂ : ⟨ Hom ℂ (om i₁) (om i₃) ⟩[ appT Sq f₂ ≡ j ]
       sq-max₃ : ⟨ Hom ℂ (om i₂) (om i₄) ⟩[ appT Sq f₃ ≡ h ]
       sq-max₄ : ⟨ Hom ℂ (om i₃) (om i₄) ⟩[ appT Sq f₄ ≡ k ]

       sq-funct-id : {i : 4Obj} → ⟨ Hom ℂ (om i) (om i) ⟩[ appT Sq (4Id {_}{i}) ≡ id ℂ ]

       sq-funct-comp : ∀{i j k : 4Obj {l}}{a : el (4Hom i j)}{b : el (4Hom j k)}
         → ⟨ Hom ℂ (om i) (om k) ⟩[ appT Sq (a ○[ 4Comp {l}{i}{j}{k} ] b) ≡ (appT Sq a) ○[ comp ℂ ] (appT Sq b) ]

  open Comm-Square'

  -- A default function from the objects of the 4PO to the objects of
  -- a square in ℂ.
  sq-default-om : {l : Level}{ℂ : Cat {l}}
    → Obj ℂ
    → Obj ℂ
    → Obj ℂ
    → Obj ℂ
    → (4Obj {l} → Obj ℂ)
  sq-default-om A B D C i₁ = A
  sq-default-om A B D C i₂ = B
  sq-default-om A B D C i₃ = D
  sq-default-om A B D C i₄ = C

  -- Commutative squares in ℂ.
  Comm-Square : {l : Level}{ℂ : Cat {l}}
    → (A B D C : Obj ℂ)
    → (g : el (Hom ℂ A B))
    → (h : el (Hom ℂ B C))
    → (j : el (Hom ℂ A D))
    → (k : el (Hom ℂ D C))
    → Set l
  Comm-Square {_} {ℂ} A B D C g h j k = Comm-Square' ℂ (sq-default-om {_} {ℂ} A B D C) g h j k

  -- Commutative squares are functors.
  Comm-Square-is-Functor : ∀{l}{ℂ : Cat {l}}{A B D C}
    → {g : el (Hom ℂ A B)}
    → {h : el (Hom ℂ B C)}
    → {j : el (Hom ℂ A D)}
    → {k : el (Hom ℂ D C)}
    → Comm-Square {_} {ℂ} A B D C g h j k
    → Functor {l} 4cat ℂ
  Comm-Square-is-Functor {_} {ℂ} {A} {B} {D} {C} {g} {h} {j} {k} sq =
    record { omap = sq-default-om {_}{ℂ} A B D C;
             fmap = λ {A₁} {B₁} → Sq sq {A₁} {B₁};
             idPF = sq-funct-id sq;
           compPF = λ {A₁} {B₁} {C₁} {f} {g₁} → sq-funct-comp sq {A₁}{B₁}{C₁}{f}{g₁} }

  -- The former now implies that we have a commutative diagram.
  Comm-Square-is-Comm-Diagram : ∀{l}{ℂ : Cat {l}}{A B D C}
    → {g : el (Hom ℂ A B)}
    → {h : el (Hom ℂ B C)}
    → {j : el (Hom ℂ A D)}
    → {k : el (Hom ℂ D C)}
    → Comm-Square {_} {ℂ} A B D C g h j k
    → Comm-Diagram {l}{l} 4po ℂ
  Comm-Square-is-Comm-Diagram {l}{ℂ}{g}{h}{j}{k} sq =
    record { diag = record { diag = Comm-Square-is-Functor sq } }

  -- If we have a commutative square, then it commutes in ℂ.
  Comm-Square-Commutes : ∀{l}{ℂ : Cat {l}}{A B D C}
    → {g : el (Hom ℂ A B)}
    → {h : el (Hom ℂ B C)}
    → {j : el (Hom ℂ A D)}
    → {k : el (Hom ℂ D C)}
    → Comm-Square {_} {ℂ} A B D C g h j k
    → ⟨ Hom ℂ A C ⟩[ g ○[ comp ℂ ] h ≡ j ○[ comp ℂ ] k ]
  Comm-Square-Commutes {l}{ℂ}{A}{B}{D}{C}{g}{h}{j}{k} sq with sq-funct-comp sq {i₁}{i₂}{i₄}{f₁}{f₃} | sq-funct-comp sq {i₁}{i₃}{i₄}{f₂}{f₄}
  ... | sq-eq₁ | sq-eq₂ with transPf (parEqPf (eqRpf (Hom ℂ A C))) (symPf (parEqPf (eqRpf (Hom ℂ A C))) sq-eq₁) sq-eq₂
  ... | sq-eq₃ with eq-comp-all {_}{ℂ}{A}{B}{C}{g}
                                {appT {_}{_}{4Hom i₁ i₂} {Hom ℂ A B} (Sq sq {i₁}{i₂}) f₁}
                                {h}
                                {appT (Sq sq {i₂}{i₄}) f₃}
                                (symPf (parEqPf (eqRpf (Hom ℂ A B))) (sq-max₁ sq))
                                (symPf (parEqPf (eqRpf (Hom ℂ B C))) (sq-max₃ sq))
  ... | sq-eq₄ with eq-comp-all {_}{ℂ}{A}{D}{C}
                                {appT {_}{_}{4Hom i₁ i₃} {Hom ℂ A D} (Sq sq {i₁}{i₃}) f₂}
                                {j}
                                {appT (Sq sq {i₃}{i₄}) f₄}
                                {k}
                                (sq-max₂ sq)
                                (sq-max₄ sq)
  ... | sq-eq₅ with transPf (parEqPf (eqRpf (Hom ℂ A C))) sq-eq₄ sq-eq₃
  ... | sq-eq₆ = transPf (parEqPf (eqRpf (Hom ℂ A C))) sq-eq₆ sq-eq₅

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


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

open import Cubical.Algebra.Ring.Base public
open import Cubical.Algebra.Ring.Properties public
open import Cubical.Algebra.Ring.Ideal public
open import Cubical.Algebra.Ring.Kernel public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{-# OPTIONS --cubical-compatible #-}
module Common.Product where

open import Common.Level

infixr 4 _,_ _,′_
infixr 2 _×_

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

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ public

syntax Σ A (λ x → B) = Σ[ x ∶ A ] B

∃ : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
∃ = Σ _

_×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b)
A × B = Σ[ x ∶ A ] B

_,′_ : ∀ {a b} {A : Set a} {B : Set b} → A → B → A × B
_,′_ = _,_


text:
-- Andreas, 2011-10-02
module NotApplyingInDontCareTriggersInternalError where
import Common.Irrelevance

postulate
  Val : Set
  App : Val -> Val -> Val -> Set

Rel = Val -> Val -> Set

Transitive : Rel → Set
Transitive R = ∀ {t1 t2 t3} → R t1 t2 → R t2 t3 → R t1 t3

postulate
  LeftReflexive : Rel → Set
  RightReflexive : Rel → Set

record PP (R : Rel) : Set where
  constructor pp
  field
    .leftRefl  : LeftReflexive R
    .rightRefl : RightReflexive R
    .trans     : Transitive R
open PP public

record Those (P : Val → Set)(R : Rel)(P' : Val → Set) : Set where
  constructor those
  field
    B    : Val
    B'   : Val
    PB   : P B
    PB'  : P' B'
    RBB' : R B B'

Fam : Rel → Set1
Fam AA = ∀ {a a'} → .(AA a a') → Rel

FamTrans : {AA : Rel}.(TA : Transitive AA)(FF : Fam AA) → Set
FamTrans {AA = AA} TA FF = ∀ {a1 a2 a3}(a12 : AA a1 a2)(a23 : AA a2 a3) →
  ∀ {b1 b2 b3}(b12 : FF a12 b1 b2)(b23 : FF a23 b2 b3) →
  FF (TA a12 a23) b1 b3

Π : (AA : Rel) → Fam AA → Rel
Π AA FF g g' = ∀ {a a'} → .(a≼a' : AA a a') →
  Those (App g a) (FF a≼a') (App g' a')

ΠTrans : {AA : Rel}(PA : PP AA){FF : Fam AA}(TF : FamTrans {AA = AA} (trans PA) FF) →
  Transitive (Π AA FF)
ΠTrans (pp leftRefl rightRefl trans) TF f12 f23 a≼a' with (leftRefl a≼a')
... | a≼a with f12 a≼a | f23 a≼a'
ΠTrans (pp leftRefl rightRefl trans) TF f12 f23 a≼a' | a≼a | those b1 b2 app1 app2 b1≼b2 | those b2' b3 app2' app3 b2'≼b3 = those b1 b3 app1 app3 ?

-- This should not give the internal error:
--
--   An internal error has occurred. Please report this as a bug.
--   Location of the error: src/full/Agda/TypeChecking/Substitute.hs:50
--
-- Instead it should complain that
--
--   Variable leftRefl is declared irrelevant, so it cannot be used here
--   when checking that the expression leftRefl a≼a' has type
--   _141 leftRefl rightRefl trans TF f12 f23 a≼a'


text:
{- Proof of the Universal Property of Our Fold -}

module FoldUniv where

open import Function using (id)
open import Data.Unit using (⊤ ; tt) public
open import Data.Empty using (⊥) public
open import Data.Sum using (_⊎_; [_,_]; inj₁ ; inj₂) public
open import Data.Product
open import Data.Nat using (ℕ)
open import Data.Bool using (Bool)
open import Data.List
open import Data.List.Any as Any
open import Data.Product
open Any.Membership-≡ hiding (_⊆_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)

data PolyF : Set where
  Id    : PolyF
  K1    : PolyF
  Kℕ    : PolyF
  KB    : PolyF
  _∔_   : (F : PolyF) → (G : PolyF) → PolyF
  _⋆_   : (F : PolyF) → (G : PolyF) → PolyF

infixr 30 _⋆_
infixr 20 _∔_

⟦_⟧ : PolyF → Set → Set
⟦_⟧ Id A      = A
⟦_⟧ K1 A     = ⊤
⟦_⟧ Kℕ A     = ℕ
⟦_⟧ KB A     = Bool
⟦_⟧ (F ∔ G) A = ⟦ F ⟧ A ⊎ ⟦ G ⟧ A
⟦_⟧ (F ⋆ G) A = ⟦ F ⟧ A × ⟦ G ⟧ A

fmap : ∀ {A B} F → (A → B) → ⟦ F ⟧ A → ⟦ F ⟧ B
fmap Id f = f
fmap K1 f = id
fmap Kℕ f = id
fmap KB f = id
fmap (F ∔ G) f =
  Data.Sum.map (fmap F f) (fmap G f)
fmap (F ⋆ G) f =
  Data.Product.map (fmap F f) (fmap G f)

Algebras : List PolyF → Set → Set
Algebras []       A = ⊤
Algebras (F ∷ Fs) A = (⟦ F ⟧ A → A) × Algebras Fs A

extract : {F : PolyF} {Fs : List PolyF} {A : Set}
          → F ∈ Fs → Algebras Fs A → (⟦ F ⟧ A → A)
extract (here refl) (f , _ ) = f
extract (there f∈ ) (f , fs) = extract f∈ fs

data μ (Fs : List PolyF) : Set where
  In : ∀ {F} → F ∈ Fs → ⟦ F ⟧ (μ Fs) → μ Fs

mutual
  fold : ∀ Fs {A} → Algebras Fs A → μ Fs → A
  fold Fs fs (In {F} F∈ x) = extract F∈ fs (mapFold Fs fs F x)

  mapFold : (Fs : List PolyF) {A : Set}
          → Algebras Fs A → (G : PolyF) → ⟦ G ⟧ (μ Fs) → ⟦ G ⟧ A
  mapFold Fs fs Id       x          = fold Fs fs x
  mapFold Fs fs K1       b          = b
  mapFold Fs fs Kℕ       b          = b
  mapFold Fs fs KB       b          = b
  mapFold Fs fs (G ∔ G') (inj₁ xs)  = inj₁ (mapFold Fs fs G xs)
  mapFold Fs fs (G ∔ G') (inj₂ xs)  = inj₂ (mapFold Fs fs G' xs)
  mapFold Fs fs (G ⋆ G') (xs , xs') = mapFold Fs fs G xs , mapFold Fs fs G' xs'

mutual

 fold-universal : (Fs : List PolyF) → {A : Set}
                → (h : μ Fs → A) → (fs : Algebras Fs A)
                → (∀ F → (F∈ : F ∈ Fs) →
                   ∀ xs → h (In F∈ xs) ≡ extract F∈ fs (fmap F h xs))
                → (∀ xs → h xs ≡ fold Fs fs xs)
 fold-universal Fs h fs hom (In {F} F∈ xs)
   rewrite hom F F∈ xs = cong (extract F∈ fs) (mapFold-univ Fs F h fs hom xs)

 mapFold-univ : (Fs : List PolyF) (G : PolyF)
              → ∀ {A : Set}
              → (h : μ Fs → A) → (fs : Algebras Fs A)
              → (∀ F → (F∈ : F ∈ Fs) →
                   ∀ xs → h (In F∈ xs) ≡ extract F∈ fs (fmap F h xs))
              → (Gxs : ⟦ G ⟧ (μ Fs))
              → fmap G h Gxs ≡ mapFold Fs fs G Gxs
 mapFold-univ Fs Id h fs hom xs = fold-universal Fs h fs hom xs
 mapFold-univ Fs K1 h fs hom tt = refl
 mapFold-univ Fs Kℕ h fs hom n = refl
 mapFold-univ Fs KB h fs hom b = refl
 mapFold-univ Fs (G₁ ∔ G₂) h fs hom (inj₁ x) = cong inj₁ (mapFold-univ Fs G₁ h fs hom x)
 mapFold-univ Fs (G₁ ∔ G₂) h fs hom (inj₂ y) = cong inj₂ (mapFold-univ Fs G₂ h fs hom y)
 mapFold-univ Fs (G₁ ⋆ G₂) h fs hom (x , y)
     rewrite mapFold-univ Fs G₁ h fs hom x | mapFold-univ Fs G₂ h fs hom y = refl


text:
module Structures where

open import Category.Functor using (RawFunctor ; module RawFunctor)
open import Category.Monad using (module RawMonad)
open import Data.Maybe using (Maybe) renaming (monad to MaybeMonad)
open import Data.Nat using (ℕ)
open import Data.Vec as V using (Vec)
import Data.Vec.Properties as VP
open import Function using (_∘_ ; flip ; id)
open import Function.Equality using (_⟶_ ; _⇨_ ; _⟨$⟩_)
open import Relation.Binary using (_Preserves_⟶_)
open import Relation.Binary.PropositionalEquality as P using (_≗_ ; _≡_ ; refl ; module ≡-Reasoning)

open import Generic using (sequenceV)

record IsFunctor (F : Set → Set) (f : {α β : Set} → (α →  β) → F α → F β) : Set₁ where
  field
    cong : {α β : Set} → f {α} {β} Preserves _≗_ ⟶ _≗_
    identity : {α : Set} → f {α} id ≗ id
    composition : {α β γ : Set} → (g : β → γ) → (h : α → β) →
                  f (g ∘ h) ≗ f g ∘ f h

  isCongruence : {α β : Set} → (P.setoid α ⇨ P.setoid β) ⟶ P.setoid (F α) ⇨ P.setoid (F β)
  isCongruence {α} {β} = record
    { _⟨$⟩_ = λ g → record
      { _⟨$⟩_ = f (_⟨$⟩_ g)
      ; cong = P.cong (f (_⟨$⟩_ g))
      }
    ; cong = λ {g} {h} g≗h {x} x≡y → P.subst (λ z → f (_⟨$⟩_ g) x ≡ f (_⟨$⟩_ h) z) x≡y (cong (λ _ → g≗h refl) x)
    }

record Functor (f : Set → Set) : Set₁ where
  field
    rawfunctor : RawFunctor f
    isFunctor : IsFunctor f (RawFunctor._<$>_ rawfunctor)

  open RawFunctor rawfunctor public
  open IsFunctor isFunctor public

record IsShaped (S : Set)
                (C : Set → S → Set)
                (arity : S → ℕ)
                (content : {α : Set} {s : S} → C α s → Vec α (arity s))
                (fill : {α : Set} → (s : S) → Vec α (arity s) → C α s)
                : Set₁ where
  field
    content-fill : {α : Set} {s : S} → (c : C α s) → fill s (content c) ≡ c
    fill-content : {α : Set} → (s : S) → (v : Vec α (arity s)) → content (fill s v) ≡ v

  fmap : {α β : Set} → (f : α → β) → {s : S} → C α s → C β s
  fmap f {s} c = fill s (V.map f (content c))

  isFunctor : (s : S) → IsFunctor (flip C s) (λ f → fmap f)
  isFunctor s = record
    { cong = λ g≗h c → P.cong (fill s) (VP.map-cong g≗h (content c))
    ; identity = λ c → begin
        fill s (V.map id (content c))
          ≡⟨ P.cong (fill s) (VP.map-id (content c)) ⟩
        fill s (content c)
          ≡⟨ content-fill c ⟩
        c ∎
    ; composition = λ g h c → P.cong (fill s) (begin
        V.map (g ∘ h) (content c)
          ≡⟨ VP.map-∘ g h (content c) ⟩
        V.map g (V.map h (content c))
          ≡⟨ P.cong (V.map g) (P.sym (fill-content s (V.map h (content c)))) ⟩
        V.map g (content (fill s (V.map h (content c)))) ∎)
    } where open ≡-Reasoning

  fmap-content : {α β : Set} → (f : α → β) → {s : S} → content {β} {s} ∘ fmap f ≗ V.map f ∘ content
  fmap-content f c = fill-content _ (V.map f (content c))
  fill-fmap : {α β : Set} → (f : α → β) → (s : S) → fmap f ∘ fill s ≗ fill s ∘ V.map f
  fill-fmap f s v = P.cong (fill s ∘ V.map f) (fill-content s v)

  sequence : {α : Set} {s : S} → C (Maybe α) s → Maybe (C α s)
  sequence {s = s} c = fill s <$> sequenceV (content c)
    where open RawMonad MaybeMonad

record Shaped (S : Set) (C : Set → S → Set) : Set₁ where
  field
    arity : S → ℕ
    content : {α : Set} {s : S} → C α s → Vec α (arity s)
    fill : {α : Set} → (s : S) → Vec α (arity s) → C α s

    isShaped : IsShaped S C arity content fill

  open IsShaped isShaped public

max_stars_repo_name: jvoigtlaender/bidiragda

max_issues_repo_name: jvoigtlaender/bidiragda

max_forks_repo_name: jvoigtlaender/bidiragda


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

module Control.Monad.Levels where

open import Control.Monad.Levels.Definition public

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.FromNat
open import Agda.Builtin.Unit

instance
  NumberNat : Number Nat
  Number.Constraint NumberNat _ = ⊤
  fromNat {{NumberNat}} n = n

open import Issue2641.Import


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

open import LogicalFormulae
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Rings.Definition

module Rings.Units.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where

open import Rings.Units.Definition R
open import Rings.Ideals.Definition R

open Ring R
open Setoid S
open Equivalence eq

unitImpliesGeneratedIdealEverything : {x : A} → Unit x → {y : A} → generatedIdealPred x y
unitImpliesGeneratedIdealEverything {x} (a , xa=1) {y} = (a * y) , transitive *Associative (transitive (*WellDefined xa=1 reflexive) identIsIdent)


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

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

open import Cubical.Data.Vec
open import Cubical.Data.Nat

private
  variable
    ℓ ℓ₁ ℓ₂ ℓ₃ : Level

-- Function extensionality is an equivalence
module _ {A : Type ℓ} {B : A → I → Type ℓ₁}
  {f : (x : A) → B x i0} {g : (x : A) → B x i1} where

  private
    fib : (p : PathP (λ i → ∀ x → B x i) f g) → fiber funExt p
    fib p = (funExt⁻ p , refl)

    funExt-fiber-isContr : ∀ p → (fi : fiber funExt p) → fib p ≡ fi
    funExt-fiber-isContr p (h , eq) i = (funExt⁻ (eq (~ i)) , λ j → eq (~ i ∨ j))

  funExt-isEquiv : isEquiv funExt
  equiv-proof funExt-isEquiv p = (fib p , funExt-fiber-isContr p)

  funExtEquiv : (∀ x → PathP (B x) (f x) (g x)) ≃ PathP (λ i → ∀ x → B x i) f g
  funExtEquiv = (funExt , funExt-isEquiv)

  funExtPath : (∀ x → PathP (B x) (f x) (g x)) ≡ PathP (λ i → ∀ x → B x i) f g
  funExtPath = ua funExtEquiv

  funExtIso : Iso (∀ x → PathP (B x) (f x) (g x)) (PathP (λ i → ∀ x → B x i) f g)
  funExtIso = iso funExt funExt⁻ (λ x → refl {x = x}) (λ x → refl {x = x})

-- Function extensionality for binary functions
funExt₂ : {A : Type ℓ} {B : A → Type ℓ₁} {C : (x : A) → B x → I → Type ℓ₂}
          {f : (x : A) → (y : B x) → C x y i0}
          {g : (x : A) → (y : B x) → C x y i1}
          → ((x : A) (y : B x) → PathP (C x y) (f x y) (g x y))
          → PathP (λ i → ∀ x y → C x y i) f g
funExt₂ p i x y = p x y i

-- Function extensionality for binary functions is an equivalence
module _ {A : Type ℓ} {B : A → Type ℓ₁} {C : (x : A) → B x → I → Type ℓ₂}
         {f : (x : A) → (y : B x) → C x y i0}
         {g : (x : A) → (y : B x) → C x y i1} where
  private
    appl₂ : PathP (λ i → ∀ x y → C x y i) f g → ∀ x y → PathP (C x y) (f x y) (g x y)
    appl₂ eq x y i = eq i x y

    fib : (p : PathP (λ i → ∀ x y → C x y i) f g) → fiber funExt₂ p
    fib p = (appl₂ p , refl)

    funExt₂-fiber-isContr : ∀ p → (fi : fiber funExt₂ p) → fib p ≡ fi
    funExt₂-fiber-isContr p (h , eq) i = (appl₂ (eq (~ i)) , λ j → eq (~ i ∨ j))

  funExt₂-isEquiv : isEquiv funExt₂
  equiv-proof funExt₂-isEquiv p = (fib p , funExt₂-fiber-isContr p)

  funExt₂Equiv : (∀ x y → PathP (C x y) (f x y) (g x y)) ≃ (PathP (λ i → ∀ x y → C x y i) f g)
  funExt₂Equiv = (funExt₂ , funExt₂-isEquiv)

  funExt₂Path : (∀ x y → PathP (C x y) (f x y) (g x y)) ≡ (PathP (λ i → ∀ x y → C x y i) f g)
  funExt₂Path = ua funExt₂Equiv

-- Function extensionality for ternary functions
funExt₃ : {A : Type ℓ} {B : A → Type ℓ₁} {C : (x : A) → B x → Type ℓ₂}
          {D : (x : A) → (y : B x) → C x y → I → Type ℓ₃}
          {f : (x : A) → (y : B x) → (z : C x y) → D x y z i0}
          {g : (x : A) → (y : B x) → (z : C x y) → D x y z i1}
        → ((x : A) (y : B x) (z : C x y) → PathP (D x y z) (f x y z) (g x y z))
        → PathP (λ i → ∀ x y z → D x y z i) f g
funExt₃ p i x y z = p x y z i

-- Function extensionality for ternary functions is an equivalence
module _ {A : Type ℓ} {B : A → Type ℓ₁} {C : (x : A) → B x → Type ℓ₂}
         {D : (x : A) → (y : B x) → C x y → I → Type ℓ₃}
         {f : (x : A) → (y : B x) → (z : C x y) → D x y z i0}
         {g : (x : A) → (y : B x) → (z : C x y) → D x y z i1} where
  private
    appl₃ : PathP (λ i → ∀ x y z → D x y z i) f g → ∀ x y z → PathP (D x y z) (f x y z) (g x y z)
    appl₃ eq x y z i = eq i x y z

    fib : (p : PathP (λ i → ∀ x y z → D x y z i) f g) → fiber funExt₃ p
    fib p = (appl₃ p , refl)

    funExt₃-fiber-isContr : ∀ p → (fi : fiber funExt₃ p) → fib p ≡ fi
    funExt₃-fiber-isContr p (h , eq) i = (appl₃ (eq (~ i)) , λ j → eq (~ i ∨ j))

  funExt₃-isEquiv : isEquiv funExt₃
  equiv-proof funExt₃-isEquiv p = (fib p , funExt₃-fiber-isContr p)

  funExt₃Equiv : (∀ x y z → PathP (D x y z) (f x y z) (g x y z)) ≃ (PathP (λ i → ∀ x y z → D x y z i) f g)
  funExt₃Equiv = (funExt₃ , funExt₃-isEquiv)

  funExt₃Path : (∀ x y z → PathP (D x y z) (f x y z) (g x y z)) ≡ (PathP (λ i → ∀ x y z → D x y z i) f g)
  funExt₃Path = ua funExt₃Equiv

-- n-ary non-dependent funext
nAryFunExt : (n : ℕ) {X : Type ℓ} {Y : I → Type ℓ₁} (fX : nAryOp n X (Y i0)) (fY : nAryOp n X (Y i1))
           → ((xs : Vec X n) → PathP Y (fX $ⁿ xs) (fY $ⁿ map (λ x → x) xs))
           → PathP (λ i → nAryOp n X (Y i)) fX fY
nAryFunExt zero fX fY p        = p []
nAryFunExt (suc n) fX fY p i x = nAryFunExt n (fX x) (fY x) (λ xs → p (x ∷ xs)) i

-- n-ary funext⁻
nAryFunExt⁻ : (n : ℕ) {X : Type ℓ} {Y : I → Type ℓ₁} (fX : nAryOp n X (Y i0)) (fY : nAryOp n X (Y i1))
           → PathP (λ i → nAryOp n X (Y i)) fX fY
           → ((xs : Vec X n) → PathP Y (fX $ⁿ xs) (fY $ⁿ map (λ x → x) xs))
nAryFunExt⁻ zero fX fY p [] = p
nAryFunExt⁻ (suc n) fX fY p (x ∷ xs) = nAryFunExt⁻ n (fX x) (fY x) (λ i → p i x) xs

nAryFunExtEquiv : (n : ℕ) {X : Type ℓ} {Y : I → Type ℓ₁} (fX : nAryOp n X (Y i0)) (fY : nAryOp n X (Y i1))
  → ((xs : Vec X n) → PathP Y (fX $ⁿ xs) (fY $ⁿ map (λ x → x) xs)) ≃ PathP (λ i → nAryOp n X (Y i)) fX fY
nAryFunExtEquiv n {X} {Y} fX fY = isoToEquiv (iso (nAryFunExt n fX fY) (nAryFunExt⁻ n fX fY)
                                              (linv n fX fY) (rinv n fX fY))
  where
  linv : (n : ℕ) (fX : nAryOp n X (Y i0)) (fY : nAryOp n X (Y i1))
    (p : PathP (λ i → nAryOp n X (Y i)) fX fY)
    → nAryFunExt n fX fY (nAryFunExt⁻ n fX fY p) ≡ p
  linv zero fX fY p          = refl
  linv (suc n) fX fY p i j x = linv n (fX x) (fY x) (λ k → p k x) i j

  rinv : (n : ℕ) (fX : nAryOp n X (Y i0)) (fY : nAryOp n X (Y i1))
         (p : (xs : Vec X n) → PathP Y (fX $ⁿ xs) (fY $ⁿ map (λ x → x) xs))
       → nAryFunExt⁻ n fX fY (nAryFunExt n fX fY p) ≡ p
  rinv zero fX fY p i []          = p []
  rinv (suc n) fX fY p i (x ∷ xs) = rinv n (fX x) (fY x) (λ ys i → p (x ∷ ys) i) i xs

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical