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

open import Setoids.Setoids
open import Groups.Definition
open import Groups.Lemmas
open import Groups.Homomorphisms.Definition
open import Groups.QuotientGroup.Definition
open import Groups.Homomorphisms.Lemmas
open import Groups.Actions.Definition
open import Sets.EquivalenceRelations

module Groups.SymmetricGroups.Lemmas where

trivialAction : {m n o p : _} {A : Set m} {S : Setoid {m} {o} A} {_·_ : A → A → A} {B : Set n} (G : Group S _·_) (X : Setoid {n} {p} B) → GroupAction G X
trivialAction G X = record { action = λ _ x → x ; actionWellDefined1 = λ _ → reflexive ; actionWellDefined2 = λ wd1 → wd1 ; identityAction = reflexive ; associativeAction = reflexive }
  where
    open Setoid X renaming (eq to setoidEq)
    open Equivalence (Setoid.eq X)

leftRegularAction : {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_·_ : A → A → A} (G : Group S _·_) → GroupAction G S
GroupAction.action (leftRegularAction {_·_ = _·_} G) g h = g · h
  where
    open Group G
GroupAction.actionWellDefined1 (leftRegularAction {S = S} G) eq1 = +WellDefined eq1 reflexive
  where
    open Group G
    open Setoid S renaming (eq to setoidEq)
    open Equivalence setoidEq
GroupAction.actionWellDefined2 (leftRegularAction {S = S} G) {g} {x} {y} eq1 = +WellDefined reflexive eq1
  where
    open Group G
    open Setoid S
    open Equivalence eq
GroupAction.identityAction (leftRegularAction G) = identLeft
  where
    open Group G
GroupAction.associativeAction (leftRegularAction {S = S} G) = symmetric +Associative
  where
    open Group G
    open Setoid S
    open Equivalence eq

conjugationAction : {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_·_ : A → A → A} → (G : Group S _·_) → GroupAction G S
conjugationAction {S = S} {_·_ = _·_} G = record { action = λ g h → (g · h) · (inverse g) ; actionWellDefined1 = λ gh → +WellDefined (+WellDefined gh reflexive) (inverseWellDefined G gh) ; actionWellDefined2 = λ x~y → +WellDefined (+WellDefined reflexive x~y) reflexive ; identityAction = transitive (+WellDefined reflexive (invIdent G)) (transitive identRight identLeft)  ; associativeAction = λ {x} {g} {h} → transitive (+WellDefined reflexive (invContravariant G)) (transitive +Associative (+WellDefined (transitive (symmetric +Associative) (transitive (symmetric (+Associative)) (+WellDefined reflexive +Associative))) reflexive)) }
  where
    open Group G
    open Setoid S
    open Equivalence eq

conjugationNormalSubgroupAction : {m n o p : _} {A : Set m} {B : Set o} {S : Setoid {m} {n} A} {T : Setoid {o} {p} B} {_·A_ : A → A → A} {_·B_ : B → B → B} → (G : Group S _·A_) → (H : Group T _·B_) → {underF : A → B} (f : GroupHom G H underF) → GroupAction G (quotientGroupSetoid G f)
GroupAction.action (conjugationNormalSubgroupAction {_·A_ = _·A_} G H {f} fHom) a b = a ·A (b ·A (Group.inverse G a))
GroupAction.actionWellDefined1 (conjugationNormalSubgroupAction {S = S} {T = T} {_·A_ = _·A_} G H {f} fHom) {g} {h} {x} g~h = ans
  where
    open Group G
    open Setoid T
    open Equivalence eq
    ans : f ((g ·A (x ·A (inverse g))) ·A inverse (h ·A (x ·A inverse h))) ∼ Group.0G H
    ans = transitive (GroupHom.wellDefined fHom (transferToRight'' G (Group.+WellDefined G g~h (Group.+WellDefined G (Equivalence.reflexive (Setoid.eq S)) (inverseWellDefined G g~h))))) (imageOfIdentityIsIdentity fHom)
GroupAction.actionWellDefined2 (conjugationNormalSubgroupAction {S = S} {T = T} {_·A_ = _·A_} {_·B_ = _·B_} G H {f} fHom) {g} {x} {y} x~y = ans
  where
    open Group G
    open Setoid T
    open Equivalence (Setoid.eq S)
    open Equivalence (Setoid.eq T) renaming (transitive to transitiveH ; symmetric to symmetricH ; reflexive to reflexiveH)
    input : f (x ·A inverse y) ∼ Group.0G H
    input = x~y
    p1 : Setoid._∼_ S ((g ·A (x ·A inverse g)) ·A inverse (g ·A (y ·A inverse g))) ((g ·A (x ·A inverse g)) ·A (inverse (y ·A (inverse g)) ·A inverse g))
    p1 = Group.+WellDefined G reflexive (invContravariant G)
    p2 : Setoid._∼_ S ((g ·A (x ·A inverse g)) ·A (inverse (y ·A (inverse g)) ·A inverse g)) ((g ·A (x ·A inverse g)) ·A ((inverse (inverse g) ·A inverse y) ·A inverse g))
    p2 = Group.+WellDefined G reflexive (Group.+WellDefined G (invContravariant G) reflexive)
    p3 : Setoid._∼_ S ((g ·A (x ·A inverse g)) ·A ((inverse (inverse g) ·A inverse y) ·A inverse g)) (g ·A (((x ·A inverse g) ·A (inverse (inverse g) ·A inverse y)) ·A inverse g))
    p3 = symmetric (transitive (+WellDefined reflexive (symmetric +Associative)) +Associative)
    p4 : Setoid._∼_ S (g ·A (((x ·A inverse g) ·A (inverse (inverse g) ·A inverse y)) ·A inverse g)) (g ·A ((x ·A ((inverse g ·A inverse (inverse g)) ·A inverse y)) ·A inverse g))
    p4 = Group.+WellDefined G reflexive (Group.+WellDefined G (symmetric (transitive (+WellDefined reflexive (symmetric +Associative)) +Associative)) reflexive)
    p5 : Setoid._∼_ S (g ·A ((x ·A ((inverse g ·A inverse (inverse g)) ·A inverse y)) ·A inverse g)) (g ·A ((x ·A (0G ·A inverse y)) ·A inverse g))
    p5 = Group.+WellDefined G reflexive (Group.+WellDefined G (Group.+WellDefined G reflexive (Group.+WellDefined G invRight reflexive)) reflexive)
    p6 : Setoid._∼_ S  (g ·A ((x ·A (0G ·A inverse y)) ·A inverse g)) (g ·A ((x ·A inverse y) ·A inverse g))
    p6 = Group.+WellDefined G reflexive (Group.+WellDefined G (Group.+WellDefined G reflexive identLeft) reflexive)
    intermediate : Setoid._∼_ S ((g ·A (x ·A inverse g)) ·A inverse (g ·A (y ·A inverse g))) (g ·A ((x ·A inverse y) ·A inverse g))
    intermediate = transitive p1 (transitive p2 (transitive p3 (transitive p4 (transitive p5 p6))))
    p7 : f ((g ·A (x ·A inverse g)) ·A inverse (g ·A (y ·A inverse g))) ∼ f (g ·A ((x ·A inverse y) ·A inverse g))
    p7 = GroupHom.wellDefined fHom intermediate
    p8 : f (g ·A ((x ·A inverse y) ·A inverse g)) ∼ (f g) ·B (f ((x ·A inverse y) ·A inverse g))
    p8 = GroupHom.groupHom fHom
    p9 : (f g) ·B (f ((x ·A inverse y) ·A inverse g)) ∼ (f g) ·B (f (x ·A inverse y) ·B f (inverse g))
    p9 = Group.+WellDefined H reflexiveH (GroupHom.groupHom fHom)
    p10 : (f g) ·B (f (x ·A inverse y) ·B f (inverse g)) ∼ (f g) ·B (Group.0G H ·B f (inverse g))
    p10 = Group.+WellDefined H reflexiveH (Group.+WellDefined H input reflexiveH)
    p11 : (f g) ·B (Group.0G H ·B f (inverse g)) ∼ (f g) ·B (f (inverse g))
    p11 = Group.+WellDefined H reflexiveH (Group.identLeft H)
    p12 : (f g) ·B (f (inverse g)) ∼ f (g ·A (inverse g))
    p12 = symmetricH (GroupHom.groupHom fHom)
    intermediate2 : f ((g ·A (x ·A inverse g)) ·A inverse (g ·A (y ·A inverse g))) ∼ (f (g ·A (inverse g)))
    intermediate2 = transitiveH p7 (transitiveH p8 (transitiveH p9 (transitiveH p10 (transitiveH p11 p12))))
    ans : f ((g ·A (x ·A inverse g)) ·A inverse (g ·A (y ·A inverse g))) ∼ Group.0G H
    ans = transitiveH intermediate2 (transitiveH (GroupHom.wellDefined fHom invRight) (imageOfIdentityIsIdentity fHom))
GroupAction.identityAction (conjugationNormalSubgroupAction {S = S} {T = T} {_·A_ = _·A_} G H {f} fHom) {x} = ans
  where
    open Group G
    open Setoid S
    open Setoid T renaming (_∼_ to _∼T_)
    open Equivalence (Setoid.eq T)
    i : Setoid._∼_ S (x ·A inverse 0G) x
    i = Equivalence.transitive (Setoid.eq S) (+WellDefined (Equivalence.reflexive (Setoid.eq S)) (invIdent G)) identRight
    h : 0G ·A (x ·A inverse 0G) ∼ x
    h = Equivalence.transitive (Setoid.eq S) identLeft i
    g : ((0G ·A (x ·A inverse 0G)) ·A inverse x) ∼ 0G
    g = transferToRight'' G h
    ans : f ((0G ·A (x ·A inverse 0G)) ·A Group.inverse G x) ∼T Group.0G H
    ans = transitive (GroupHom.wellDefined fHom g) (imageOfIdentityIsIdentity fHom)
GroupAction.associativeAction (conjugationNormalSubgroupAction {S = S} {T = T} {_·A_ = _·A_} G H {f} fHom) {x} {g} {h} = ans
  where
    open Group G
    open Setoid T renaming (_∼_ to _∼T_)
    open Setoid S renaming (_∼_ to _∼S_)
    open Equivalence (Setoid.eq T) renaming (transitive to transitiveH)
    open Equivalence (Setoid.eq S) renaming (transitive to transitiveG ; symmetric to symmetricG ; reflexive to reflexiveG)
    ans : f (((g ·A h) ·A (x ·A inverse (g ·A h))) ·A inverse ((g ·A ((h ·A (x ·A inverse h)) ·A inverse g)))) ∼T Group.0G H
    ans = transitiveH (GroupHom.wellDefined fHom (transferToRight'' G (transitiveG (symmetricG +Associative) (Group.+WellDefined G reflexiveG (transitiveG (+WellDefined reflexiveG (transitiveG (+WellDefined reflexiveG (invContravariant G)) +Associative)) +Associative))))) (imageOfIdentityIsIdentity fHom)


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

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

open Σ

data ⊤ : Set where
  tt : ⊤

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

infix 10 _≡_

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

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

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

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

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

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

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

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

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

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

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

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

{-
record Functor (C D : Cat) : Set where
  field Fun : Obj C → Obj D
        map : ∀ {X Y} → (Hom C X Y) → Hom D (Fun X) (Fun Y)
        mapid : ∀ {X} → map (id C X) ≡ id D (Fun X)
        map○ : ∀ {X Y Z}{f : Hom C X Y}{g : Hom C Y Z} →
               map (_○_ C g f) ≡ _○_ D (map g) (map f)

open Functor

idF : ∀ C → Functor C C
idF C = record {Fun = \x → x; map = \x → x; mapid = refl; map○ = refl}

_•_ : ∀ {C D E} → Functor D E → Functor C D → Functor C E
F • G = record {Fun = \X → Fun F (Fun G X);
                 map = \f → map F (map G f);
                 mapid = trans (resp (\x → map F x) (mapid G)) (mapid F);
                 map○ = trans (resp (\x → map F x) (map○ G)) (map○ F)}

record Nat {C D : Cat} (F G : Functor C D) : Set where
  field η : (X : Obj C) → Hom D (Fun F X) (Fun G X)
        law : {X Y : Obj C}{f : Hom C X Y} →
              _○_ D (η Y) (map F f) ≡ _○_ D (map G f) (η X)

open Nat

_▪_ : ∀ {C D : Cat}{F G H : Functor C D} → Nat G H → Nat F G → Nat F H
_▪_ {D = D} A B =
  record {
    η = \X → _○_ D (η A X) (η B X);
    law = \{X}{Y} →
      trans (assoc D)
            (trans (resp (\f → _○_ D (η A Y) f) (law B))
                   (trans (sym (assoc D))
                          (trans (resp (\g → _○_ D g (η B X)) (law A))
                                 (assoc D))))
  }

-}

ext: agda

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text: module Categories.Equalizer where

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
open import Data.List
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product
open import Data.Bool
open import Function using (id; _∘_)
open import Algebra
open import Level using (Level; _⊔_)

module test where

    variable
      a b c ℓ c₂ ℓ₂ : Level
      A : Set a
      B : Set b
      C : Set c
      m n o p : ℕ

-- Vector representation

    module Vector where
        -- Inductive definition of a vector
        data Vector (A : Set a) : (n : ℕ) → Set a where
          [] : Vector A zero
          _::_ :  A → Vector A n → Vector A (suc n)

        infixr 5 _::_

        vecLength : Vector A n → ℕ
        vecLength {n = n} v = n

        headV : Vector A (suc n) → A
        headV (x :: _) = x

        tailV : Vector A (suc n) → Vector A n
        tailV (_ :: xs) = xs

        -- Matrices are defined as vector of vectors
        Matrix : (A : Set a) → (m n : ℕ) → Set a
        Matrix A m n = Vector (Vector A m) n

        matLength : Matrix A m n → ℕ × ℕ
        matLength {m = m} {n = n} mat  = m , n

        -- Some examples
        v1 : Vector ℕ 4
        v1 = 1 :: 3 :: 4 :: 5 :: []

        m1 : Matrix ℕ 2 2
        m1 =  (1 :: 2 :: []) :: (3 :: 4 :: []) :: []

        -- Some standard functions for working with vectors
        zipV : (A → B → C) → (Vector A n → Vector B n → Vector C n)
        zipV f [] [] = []
        zipV f (x :: xs) (y :: ys) = f x y :: zipV f xs ys

        mapV : (A → B) → Vector A n → Vector B n
        mapV f [] = []
        mapV f (x :: v) = f x :: mapV f v

        replicateV : A → Vector A n
        replicateV {n = zero} x = []
        replicateV {n = suc n} x = x :: replicateV x

        transpose : Matrix A m n → Matrix A n m
        transpose [] = replicateV []
        transpose (x :: xs) = ((zipV _::_) x) (transpose xs)

        -- Pointwise equality on vectors (lifting _∼_ from elements to vectors)
        data EqV {A : Set a} (_∼_ : A → A → Set c) :
                       ∀ {m n} (xs : Vector A m) (ys : Vector A n) → Set (a ⊔ c)
                       where
          eq-[]  : EqV _∼_ [] []
          eq-::  : ∀ {m n x y} {xs : Vector A m} {ys : Vector A n}
                  (x∼y : x ∼ y) (xs∼ys : EqV _∼_ xs ys) →
                  EqV _∼_ (x :: xs) (y :: ys)

-- Operations

    module Operations (R : Ring c ℓ) where
        open Ring R
        open Vector

        infixr 6 _+v_
        infixr 7 _◁_ _◁ₘ_ _x_ _⊗_ _*m_

        sumV : Vector Carrier n → Carrier
        sumV {n = zero} v = 0#
        sumV {n = suc n} (x :: xs) = x + sumV {n} xs

        0v : Vector Carrier n
        0v = replicateV 0#

        0m : Matrix Carrier m n
        0m = replicateV 0v

        -- Vector addition
        _+v_ : Vector Carrier n → Vector Carrier n  → Vector Carrier n
        _+v_ = zipV _+_

        -- Scale vector
        _◁_ : Carrier → Vector Carrier n → Vector Carrier n
        c ◁ v = mapV (c *_) v

        -- Dot product
        _•_ : Vector Carrier n → Vector Carrier n → Carrier
        u • v = sumV (zipV _*_ u v)

        -- Cross
        _x_ : Vector Carrier 3 → Vector Carrier 3 → Vector Carrier 3
        (v1 :: v2 :: v3 :: []) x (u1 :: u2 :: u3 :: []) = (v2 * u3 + -(v3 * u2) ::
                                                           v3 * u1 + -(v1 * u3) ::
                                                           v1 * u2 + -(v2 * u1) :: [])

        -- Outer product
        _⊗_ : Vector Carrier m → Vector Carrier n → Matrix Carrier n m
        _⊗_ [] ys = []
        _⊗_ (x :: xs) ys = mapV (x *_) ys :: xs ⊗ ys

        -- Scale matrix
        _◁ₘ_ : Carrier → Matrix Carrier m n → Matrix Carrier m n
        c ◁ₘ m = mapV (c ◁_) m

        -- Add matrix/matrix
        _+m_ : Matrix Carrier m n → Matrix Carrier m n → Matrix Carrier m n
        _+m_ = zipV _+v_

        -- Mul matrix/vector
        _*mv_ : Matrix Carrier n m → Vector Carrier n → Vector Carrier m
        [] *mv m = 0v
        m *mv v = mapV (_• v) m

        -- Mul matrix/matrix
        _*m_ : {m n o : ℕ} → Matrix Carrier m n → Matrix Carrier m o → Matrix Carrier n o
        _ *m [] = 0m
        m1 *m m2 = mapV (m1 *mv_) m2

        Sign = Carrier
        altSumVHelp : Sign → Vector Carrier n → Carrier
        altSumVHelp s [] = 0#
        altSumVHelp s (x :: xs) = s * x + altSumVHelp (- s) xs

        altSumV : Vector Carrier n → Carrier
        altSumV = altSumVHelp 1# -- alternating sum: multiply every second term by minus one

        -- submatricesStep : Matrix Carrier m (suc (suc n)) → Vector (Matrix Carrier m (suc n)) (suc (suc n))
        submatricesStep : Matrix Carrier (suc (suc m)) n → Vector (Matrix Carrier (suc m) n) (suc (suc m))

        -- submatrices : Matrix Carrier m (suc n) → Vector (Matrix Carrier m n) (suc n)
        submatrices : Matrix Carrier (suc m) n → Vector (Matrix Carrier m n) (suc m)
        submatrices {ℕ.zero} {n} ma = replicateV [] :: []
        submatrices {suc m} {n}  ma = submatricesStep ma

        submatricesStep ma with mapV headV ma | mapV tailV ma
        submatricesStep ma | heads | tails with submatrices tails
        submatricesStep ma | heads | tails | rec = tails :: mapV (zipV _::_ heads) rec

        -- Determinant
        det : Matrix Carrier m m → Carrier
        det [] = 1#
        det (v :: m) = altSumV (zipV _*_ v (mapV det (submatrices m)))

        module Property (a11 a12 a21 a22 : Carrier) where

         m22 : Matrix Carrier 2 2
         m22 = (a11 :: a12 :: []) :: (a21 :: a22 :: []) :: []
         test : Carrier
         test = det m22

        -- Equality on our vectors is a lifted version of the
        -- underlying equality of the ring of components.
        _=v_ : Vector Carrier n → Vector Carrier m → Set (c ⊔ ℓ)
        _=v_ = EqV _≈_
        -- The equality type is basically just a vector of equality
        -- proofs between pairs of corresponding elements.

        -- Left and right proof of identity with vector addition
        vectorAddIdentityˡ : ∀ {n} (v1 : Vector Carrier n) → (0v +v v1) =v v1
        vectorAddIdentityˡ [] = eq-[]
        vectorAddIdentityˡ (x1 :: v1) = eq-::(+-identityˡ x1) (vectorAddIdentityˡ v1)

        vectorAddIdentityʳ : ∀ {n} (v1 : Vector Carrier n) → (v1 +v 0v) =v v1
        vectorAddIdentityʳ [] = eq-[]
        vectorAddIdentityʳ (x1 :: v1) = eq-::(+-identityʳ x1) (vectorAddIdentityʳ v1)

        -- Vector addition is commutative (statement, and inductive proof)
        vectorAddComm : ∀ {n} (v1 v2 : Vector Carrier n) →
                        (v1 +v v2) =v (v2 +v v1)
        vectorAddComm [] [] = eq-[]
        vectorAddComm (x1 :: v1) (x2 :: v2) =
            eq-:: (+-comm x1 x2) (vectorAddComm v1 v2)

        -- Vector addition is associative (statement, and inductive proof)
        vectorAddAssoc : ∀ {n} (v1 v2 v3 : Vector Carrier n) →
                         ((v1 +v v2) +v v3) =v (v1 +v (v2 +v v3))
        vectorAddAssoc [] [] [] = eq-[]
        vectorAddAssoc (x1 :: v1) (x2 :: v2) (x3 :: v3) =
            eq-:: (+-assoc x1 x2 x3) (vectorAddAssoc v1 v2 v3)

        dotComm : ∀ {n} (v1 v2 : Vector Carrier n) → (v1 • v2) ≈ (v2 • v1)
        dotComm [] v2 = refl
        dotComm (v1 :: vs) v2 = {!!} --hmmm

        module Morphism (G : Group c ℓ) (H : Group c₂ ℓ₂) where
          open Group G renaming (_∙_ to _*m_; ε to 0m)
          open Group H renaming (_∙_ to _*_; ε to 0#)

         -- show the determinant is a homomorphism


text:
module slots.imports where

open import Data.Nat public using (ℕ ; zero ; suc ; _+_ ; _*_)
open import Data.Fin public using (Fin ; zero ; suc ; #_)
open import Data.List public using (List ; [] ; _∷_)
open import Data.Vec public using (Vec ; [] ; _∷_)
open import Data.Product public using (_×_ ; _,_ ; proj₁ ; proj₂)
open import Function public using (const ; _∘_ ; _$_ ; case_of_)
open import Relation.Nullary public using (Dec ; yes ; no)
open import Relation.Binary.PropositionalEquality public using (_≡_ ; refl)

module N = Data.Nat
module F = Data.Fin
module L = Data.List
module V = Data.Vec
module P = Data.Product

max_stars_repo_name: semenov-vladyslav/slots-agda

max_issues_repo_name: semenov-vladyslav/slots-agda

max_forks_repo_name: semenov-vladyslav/slots-agda


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

open import Agda.Primitive
open import Prelude
import GSeTT.Rules
import GSeTT.Typed-Syntax
import Globular-TT.Syntax
import Globular-TT.Rules

{- Decidability of type cheking for the type theory for globular sets -}
module Globular-TT.Dec-Type-Checking {l} (index : Set l) (rule : index → GSeTT.Typed-Syntax.Ctx × (Globular-TT.Syntax.Pre-Ty index))
                                                   (assumption : Globular-TT.Rules.well-founded index rule)
                                                   (eqdec-index : eqdec index) where
  open import Globular-TT.Syntax index
  open import Globular-TT.Eqdec-syntax index eqdec-index
  open import Globular-TT.Rules index rule
  open import Globular-TT.CwF-Structure index rule

  dec-∈ : ∀ (n : ℕ) (A : Pre-Ty) (Γ : Pre-Ctx) → dec (n # A ∈ Γ)
  dec-∈ n A ⊘ = inr λ{()}
  dec-∈ n A (Γ ∙ x # B) with dec-∈ n A Γ
  ...                    | inl n∈Γ = inl (inl n∈Γ)
  ...                    | inr n∉Γ with eqdecℕ n x | eqdec-Ty A B
  ...                              | inl idp | inl idp = inl (inr (idp , idp))
  ...                              | inr n≠x | _ = inr λ{(inl n∈Γ) → n∉Γ n∈Γ; (inr (idp , idp)) → n≠x idp}
  ...                              | inl idp | inr A≠B_ = inr λ{(inl n∈Γ) → n∉Γ n∈Γ;  (inr (_ , A=B)) → A≠B A=B}

  {- Decidability in the fragment of the theory with only globular contexts -}
  -- termination is really tricky, and involves reasonning both on depth and dimension at the same time !
  dec-G⊢T : ∀ (Γ : GSeTT.Typed-Syntax.Ctx) n A → dim A ≤ n →  dec (GPre-Ctx (fst Γ) ⊢T A)
  dec-G⊢t : ∀ (Γ : GSeTT.Typed-Syntax.Ctx) n d A t → dim A ≤ n → depth t ≤ d →  dec (GPre-Ctx (fst Γ) ⊢t t # A)
  dec-G⊢S : ∀ (Δ Γ : GSeTT.Typed-Syntax.Ctx) n d γ → dimC (GPre-Ctx (fst Γ)) ≤ n → depthS γ ≤ d → dec (GPre-Ctx (fst Δ) ⊢S γ > GPre-Ctx (fst Γ))

  dec-G⊢T Γ _ ∗ _ = inl (ob (GCtx _ (snd Γ)))
  dec-G⊢T Γ (S n) (⇒ A t u) (S≤ i)  with dec-G⊢T Γ n A i | dec-G⊢t Γ n _ A t i (n≤n _) | dec-G⊢t Γ n _ A u i (n≤n _)
  ...                         | inl Γ⊢A | inl Γ⊢t:A | inl Γ⊢u:A = inl (ar Γ⊢A Γ⊢t:A Γ⊢u:A)
  ...                         | inr Γ⊬A | _ | _ = inr λ{(ar Γ⊢A _ _) → Γ⊬A Γ⊢A}
  ...                         | inl _ | inr Γ⊬t:A  | _ = inr λ{(ar _ Γ⊢t:A _) → Γ⊬t:A Γ⊢t:A}
  ...                         | inl _ | inl _  | inr Γ⊬u:A = inr λ{(ar _ _ Γ⊢u:A) → Γ⊬u:A Γ⊢u:A}

  dec-G⊢t Γ n _ A (Var x) _ (0≤ _) with dec-∈ x A (GPre-Ctx (fst Γ))
  ...                              | inl x∈Γ = inl (var (GCtx _ (snd Γ)) x∈Γ)
  ...                              | inr x∉Γ = inr λ {(var _ x∈Γ) → x∉Γ x∈Γ}
  dec-G⊢t Γ n (S d) A (Tm-constructor i γ) dimA≤n (S≤ dγ≤d) with eqdec-Ty A (Ti i [ γ ]Pre-Ty )
  ...                                         | inr A≠Ti = inr λ{(tm _ _ idp) → A≠Ti idp}
  ...                                         | inl idp
                                                    with dec-G⊢T (fst (rule i)) n (Ti i) (=-≤ (dim[] _ _ ^) dimA≤n)
  ...                                                 | inr Ci⊬Ti = inr λ t → Ci⊬Ti (Γ⊢tm→Ci⊢Ti t)
  ...                                                 | inl Ci⊢Ti with dec-G⊢S Γ (fst (rule i)) n d γ
                                                                               (≤T (≤-= (assumption i Ci⊢Ti) (dim[] _ _ ^)) dimA≤n)    -- dim Ci ≤ dim A
                                                                               dγ≤d                                                    -- depth γ ≤ d
  ...                                                             | inr Γ⊬γ = inr λ t → Γ⊬γ (Γ⊢tm→Γ⊢γ t)
  ...                                                             | inl Γ⊢γ = inl (tm Ci⊢Ti Γ⊢γ idp)

  dec-G⊢S Δ (nil , _) _ _ <> (0≤ _) _ = inl (es (GCtx _ (snd Δ)))
  dec-G⊢S Δ ((Γ :: _) , _) _ _ <> _ _ = inr λ {()}
  dec-G⊢S Δ (nil , _) _ _ < γ , x ↦ t > _ _ = inr λ {()}
  dec-G⊢S Δ ((Γ :: (y , A)) , Γ+⊢@(GSeTT.Rules.cc Γ⊢ Γ⊢A idp)) n d < γ , x ↦ t > dimΓ+≤n dγ+≤d with dec-G⊢S Δ (Γ , Γ⊢) n d γ
                                                                                (≤T (n≤max (dimC (GPre-Ctx Γ)) (dim (GPre-Ty A))) dimΓ+≤n) -- dim Γ ≤ n
                                                                                (≤T (n≤max (depthS γ) (depth t)) dγ+≤d)                    -- depth γ ≤ d
                                                                                | dec-G⊢t Δ n d ((GPre-Ty A) [ γ ]Pre-Ty) t
                                                                                ((≤T (=-≤ (dim[] _ _) (m≤max (dimC (GPre-Ctx Γ)) (dim (GPre-Ty A)))) dimΓ+≤n)) -- dim A[γ] ≤ n
                                                                                (≤T (m≤max (depthS γ) (depth t)) dγ+≤d)                                        -- depth t ≤ d
                                                                                | eqdecℕ y x
  ...                                                    | inl Δ⊢γ:Γ | inl Δ⊢t | inl idp = inl (sc Δ⊢γ:Γ (GCtx _ Γ+⊢) Δ⊢t idp)
  ...                                                    | inr Δ⊬γ:Γ | _ | _  = inr λ {(sc Δ⊢γ:Γ _ _ idp) → Δ⊬γ:Γ Δ⊢γ:Γ}
  ...                                                    | inl _ | inr Δ⊬t | _ = inr λ {(sc _ _ Δ⊢t idp) → Δ⊬t Δ⊢t}
  ...                                                    | inl _ | inl _ | inr n≠x = inr λ {(sc _ _ _ idp) → n≠x idp}

  {- Decidability of judgments for contexts, types, terms and substitution towards a glaobular context -}
  dec-⊢C : ∀ Γ → dec (Γ ⊢C)
  dec-⊢T : ∀ Γ A →  dec (Γ ⊢T A)
  dec-⊢t : ∀ Γ A t → dec (Γ ⊢t t # A)
  dec-⊢S:G : ∀ Δ (Γ : GSeTT.Typed-Syntax.Ctx) γ → dec (Δ ⊢S γ > GPre-Ctx (fst Γ))

  dec-⊢T Γ ∗ with dec-⊢C Γ
  ...        | inl Γ⊢ = inl (ob Γ⊢)
  ...        | inr Γ⊬ = inr λ {(ob Γ⊢) → Γ⊬ Γ⊢}

  dec-⊢T Γ (⇒ A t u) with dec-⊢T Γ A | dec-⊢t Γ A t | dec-⊢t Γ A u
  ...                 | inl Γ⊢A | inl Γ⊢t:A | inl Γ⊢u:A = inl (ar Γ⊢A Γ⊢t:A Γ⊢u:A)
  ...                 | inr Γ⊬A | _ | _ = inr λ {(ar Γ⊢A _ _) → Γ⊬A Γ⊢A}
  ...                 | inl _ | inr Γ⊬t:A | _ = inr λ {(ar _ Γ⊢t:A _) → Γ⊬t:A Γ⊢t:A}
  ...                 | inl _ | inl _ | inr Γ⊬u:A = inr λ {(ar _ _ Γ⊢u:A) → Γ⊬u:A Γ⊢u:A}

  dec-⊢t Γ A (Var x) with dec-⊢C Γ | dec-∈ x A Γ
  ...                | inl Γ⊢ | inl x∈Γ = inl (var Γ⊢ x∈Γ)
  ...                | inr Γ⊬ | _ = inr λ {(var Γ⊢ _) → Γ⊬ Γ⊢}
  ...                | inl _ | inr x∉Γ = inr λ {(var _ x∈Γ) → x∉Γ x∈Γ}
  dec-⊢t Γ A (Tm-constructor i γ) with eqdec-Ty A (Ti i [ γ ]Pre-Ty)
  ...                                   | inr A≠Ti = inr λ{(tm _ _ idp) → A≠Ti idp}
  ...                                   | inl idp
                                              with dec-G⊢T (fst (rule i)) _ (Ti i) (n≤n _) | dec-⊢S:G Γ (fst (rule i)) γ
  ...                                              | inl Ci⊢Ti | inl Γ⊢γ = inl (tm Ci⊢Ti Γ⊢γ idp)
  ...                                              | inr Ci⊬Ti | _ = inr λ t → Ci⊬Ti (Γ⊢tm→Ci⊢Ti t)
  ...                                              | inl _ | inr Γ⊬γ = inr λ t → Γ⊬γ (Γ⊢tm→Γ⊢γ t)

  dec-⊢C ⊘ = inl ec
  dec-⊢C (Γ ∙ n # A) with dec-⊢C Γ | dec-⊢T Γ A | eqdecℕ n (C-length Γ)
  ...                 | inl Γ⊢ | inl Γ⊢A | inl idp = inl (cc Γ⊢ Γ⊢A idp)
  ...                 | inr Γ⊬ | _ | _ = inr λ {(cc Γ⊢ _ idp) → Γ⊬ Γ⊢}
  ...                 | inl _ | inr Γ⊬A | _ = inr λ {(cc _ Γ⊢A idp) → Γ⊬A Γ⊢A}
  ...                 | inl _ | inl _ | inr n≠l = inr λ {(cc _ _ idp) → n≠l idp}

  dec-⊢S:G Δ (nil , _) <> with (dec-⊢C Δ)
  ...             | inl Δ⊢ = inl (es Δ⊢)
  ...             | inr Δ⊬ = inr λ{(es Δ⊢) → Δ⊬ Δ⊢}
  dec-⊢S:G Δ (nil , _) < γ , x ↦ x₁ > = inr λ{()}
  dec-⊢S:G Δ ((Γ :: _) , _) <> = inr λ{()}
  dec-⊢S:G Δ ((Γ :: (v , A)) , Γ+⊢@(GSeTT.Rules.cc Γ⊢ Γ⊢A idp)) < γ , x ↦ t > with dec-⊢S:G Δ (Γ , Γ⊢) γ | dec-⊢t Δ ((GPre-Ty A) [ γ ]Pre-Ty) t | eqdecℕ x (length Γ)
  ...                                                                | inl Δ⊢γ | inl Δ⊢t | inl idp = inl (sc Δ⊢γ (GCtx _ Γ+⊢) Δ⊢t idp)
  ...                                                                | inr Δ⊬γ | _ | _ = inr λ{(sc Δ⊢γ _ _ idp) → Δ⊬γ Δ⊢γ}
  ...                                                                | inl _ | inr Δ⊬t | _ = inr λ{(sc _ _ Δ⊢t idp) → Δ⊬t Δ⊢t}
  ...                                                                | inl _ | inl _ | inr x≠x = inr λ{(sc _ _ _ idp) → x≠x idp}

  {- Decidability of substitution -}
  dec-⊢S : ∀ Δ Γ γ → dec (Δ ⊢S γ > Γ)
  dec-⊢S Δ ⊘ <> with (dec-⊢C Δ)
  ...             | inl Δ⊢ = inl (es Δ⊢)
  ...             | inr Δ⊬ = inr λ{(es Δ⊢) → Δ⊬ Δ⊢}
  dec-⊢S Δ ⊘ < γ , x ↦ x₁ > = inr λ{()}
  dec-⊢S Δ (Γ ∙ _ # _) <> = inr λ{()}
  dec-⊢S Δ (Γ ∙ v # A) < γ , x ↦ t > with dec-⊢S Δ Γ γ | dec-⊢C (Γ ∙ v # A) | dec-⊢t Δ (A [ γ ]Pre-Ty) t | eqdecℕ x v
  ...                                                                | inl Δ⊢γ | inl Γ+⊢ | inl Δ⊢t | inl idp  = inl (sc Δ⊢γ Γ+⊢ Δ⊢t idp)
  ...                                                                | inr Δ⊬γ | _ | _ | _  = inr λ{(sc Δ⊢γ _ _ idp) → Δ⊬γ Δ⊢γ}
  ...                                                                | inl _ | inr Γ+⊬ | _ | _  = inr λ{(sc _ Γ⊢ _ idp) → Γ+⊬ Γ⊢}
  ...                                                                | inl _ | inl _ | inr Δ⊬t | _  = inr λ{(sc _ _ Δ⊢t idp) → Δ⊬t Δ⊢t}
  ...                                                                | inl _ | inl _ | inl _ | inr x≠x  = inr λ{(sc _ _ _ idp) → x≠x idp}

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization


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

open import Cubical.Data.List.Base       public
open import Cubical.Data.List.Properties 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:
-- Andreas, 2017-12-04, Re: issue #2862, reported by m0davis,
-- Make sure there is similar problem with functions.

open import Agda.Builtin.Equality

data Bool : Set where
  true false : Bool

module N where
  val : Bool  -- Should fail

module M where
  open N
  val = true
  val≡true : val ≡ true
  val≡true = refl

open N
val = false

data ⊥ : Set where

¬val≡true : val ≡ true → ⊥
¬val≡true ()

-- val≡true : val ≡ true
-- val≡true = Z.va val true

boom : ⊥
boom = ¬val≡true Z.val≡true

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Definition.Typed.Consequences.Inequality where

open import Definition.Untyped hiding (U≢ne; ℕ≢ne; B≢ne; U≢B; ℕ≢B)
open import Definition.Typed
open import Definition.Typed.EqRelInstance
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Fundamental.Reducibility
open import Definition.Typed.Consequences.Syntactic

open import Tools.Product
open import Tools.Empty

A≢B : ∀ {A B Γ} (_⊩′⟨_⟩A_ _⊩′⟨_⟩B_ : Con Term → TypeLevel → Term → Set)
      (A-intr : ∀ {l} → Γ ⊩′⟨ l ⟩A A → Γ ⊩⟨ l ⟩ A)
      (B-intr : ∀ {l} → Γ ⊩′⟨ l ⟩B B → Γ ⊩⟨ l ⟩ B)
      (A-elim : ∀ {l} → Γ ⊩⟨ l ⟩ A → ∃ λ l′ → Γ ⊩′⟨ l′ ⟩A A)
      (B-elim : ∀ {l} → Γ ⊩⟨ l ⟩ B → ∃ λ l′ → Γ ⊩′⟨ l′ ⟩B B)
      (A≢B′ : ∀ {l l′} ([A] : Γ ⊩′⟨ l ⟩A A) ([B] : Γ ⊩′⟨ l′ ⟩B B)
            → ShapeView Γ l l′ A B (A-intr [A]) (B-intr [B]) → ⊥)
    → Γ ⊢ A ≡ B → ⊥
A≢B {A} {B} _ _ A-intr B-intr A-elim B-elim A≢B′ A≡B with reducibleEq A≡B
A≢B {A} {B} _ _ A-intr B-intr A-elim B-elim A≢B′ A≡B | [A] , [B] , [A≡B] =
  let _ , [A]′ = A-elim ([A])
      _ , [B]′ = B-elim ([B])
      [A≡B]′ = irrelevanceEq [A] (A-intr [A]′) [A≡B]
  in  A≢B′ [A]′ [B]′ (goodCases (A-intr [A]′) (B-intr [B]′) [A≡B]′)

U≢ℕ′ : ∀ {Γ B l l′}
       ([U] : Γ ⊩′⟨ l ⟩U)
       ([ℕ] : Γ ⊩ℕ B)
     → ShapeView Γ l l′ _ _ (Uᵣ [U]) (ℕᵣ [ℕ]) → ⊥
U≢ℕ′ a b ()

U≢ℕ-red : ∀ {B Γ} → Γ ⊢ B ⇒* ℕ → Γ ⊢ U ≡ B → ⊥
U≢ℕ-red D = A≢B (λ Γ l A → Γ ⊩′⟨ l ⟩U) (λ Γ l B → Γ ⊩ℕ B) Uᵣ ℕᵣ
                (λ x → extractMaybeEmb (U-elim x))
                (λ x → extractMaybeEmb (ℕ-elim′ D x))
                U≢ℕ′

-- U and ℕ cannot be judgmentally equal.
U≢ℕ : ∀ {Γ} → Γ ⊢ U ≡ ℕ → ⊥
U≢ℕ U≡ℕ =
  let _ , ⊢ℕ = syntacticEq U≡ℕ
  in  U≢ℕ-red (id ⊢ℕ) U≡ℕ

-- U and Empty
U≢Empty′ : ∀ {Γ B l l′}
       ([U] : Γ ⊩′⟨ l ⟩U)
       ([Empty] : Γ ⊩Empty B)
     → ShapeView Γ l l′ _ _ (Uᵣ [U]) (Emptyᵣ [Empty]) → ⊥
U≢Empty′ a b ()

U≢Empty-red : ∀ {B Γ} → Γ ⊢ B ⇒* Empty → Γ ⊢ U ≡ B → ⊥
U≢Empty-red D = A≢B (λ Γ l A → Γ ⊩′⟨ l ⟩U) (λ Γ l B → Γ ⊩Empty B) Uᵣ Emptyᵣ
                (λ x → extractMaybeEmb (U-elim x))
                (λ x → extractMaybeEmb (Empty-elim′ D x))
                U≢Empty′

U≢Emptyⱼ : ∀ {Γ} → Γ ⊢ U ≡ Empty → ⊥
U≢Emptyⱼ U≡Empty =
  let _ , ⊢Empty = syntacticEq U≡Empty
  in  U≢Empty-red (id ⊢Empty) U≡Empty

-- U and Unit
U≢Unit′ : ∀ {Γ B l l′}
       ([U] : Γ ⊩′⟨ l ⟩U)
       ([Unit] : Γ ⊩Unit B)
     → ShapeView Γ l l′ _ _ (Uᵣ [U]) (Unitᵣ [Unit]) → ⊥
U≢Unit′ a b ()

U≢Unit-red : ∀ {B Γ} → Γ ⊢ B ⇒* Unit → Γ ⊢ U ≡ B → ⊥
U≢Unit-red D = A≢B (λ Γ l A → Γ ⊩′⟨ l ⟩U) (λ Γ l B → Γ ⊩Unit B) Uᵣ Unitᵣ
                (λ x → extractMaybeEmb (U-elim x))
                (λ x → extractMaybeEmb (Unit-elim′ D x))
                U≢Unit′

U≢Unitⱼ : ∀ {Γ} → Γ ⊢ U ≡ Unit → ⊥
U≢Unitⱼ U≡Unit =
  let _ , ⊢Unit = syntacticEq U≡Unit
  in  U≢Unit-red (id ⊢Unit) U≡Unit

-- ℕ and Empty

ℕ≢Empty′ : ∀ {Γ B l l'}
           ([ℕ] : Γ ⊩ℕ ℕ)
           ([Empty] : Γ ⊩Empty B)
           → ShapeView Γ l l' _ _ (ℕᵣ [ℕ]) (Emptyᵣ [Empty]) → ⊥
ℕ≢Empty′ a b ()

ℕ≢Empty-red : ∀ {B Γ} → Γ ⊢ B ⇒* Empty → Γ ⊢ ℕ ≡ B → ⊥
ℕ≢Empty-red D = A≢B (λ Γ l A → Γ ⊩ℕ A) (λ Γ l B → Γ ⊩Empty B) ℕᵣ Emptyᵣ
                (λ x → extractMaybeEmb (ℕ-elim x))
                (λ x → extractMaybeEmb (Empty-elim′ D x))
                ℕ≢Empty′

ℕ≢Emptyⱼ : ∀ {Γ} → Γ ⊢ ℕ ≡ Empty → ⊥
ℕ≢Emptyⱼ ℕ≡Empty =
  let _ , ⊢Empty = syntacticEq ℕ≡Empty
  in  ℕ≢Empty-red (id ⊢Empty) ℕ≡Empty

-- ℕ and Unit

ℕ≢Unit′ : ∀ {Γ B l l'}
           ([ℕ] : Γ ⊩ℕ ℕ)
           ([Unit] : Γ ⊩Unit B)
           → ShapeView Γ l l' _ _ (ℕᵣ [ℕ]) (Unitᵣ [Unit]) → ⊥
ℕ≢Unit′ a b ()

ℕ≢Unit-red : ∀ {B Γ} → Γ ⊢ B ⇒* Unit → Γ ⊢ ℕ ≡ B → ⊥
ℕ≢Unit-red D = A≢B (λ Γ l A → Γ ⊩ℕ A) (λ Γ l B → Γ ⊩Unit B) ℕᵣ Unitᵣ
                (λ x → extractMaybeEmb (ℕ-elim x))
                (λ x → extractMaybeEmb (Unit-elim′ D x))
                ℕ≢Unit′

ℕ≢Unitⱼ : ∀ {Γ} → Γ ⊢ ℕ ≡ Unit → ⊥
ℕ≢Unitⱼ ℕ≡Unit =
  let _ , ⊢Unit = syntacticEq ℕ≡Unit
  in  ℕ≢Unit-red (id ⊢Unit) ℕ≡Unit

-- Empty and Unit

Empty≢Unit′ : ∀ {Γ B l l'}
           ([Empty] : Γ ⊩Empty Empty)
           ([Unit] : Γ ⊩Unit B)
           → ShapeView Γ l l' _ _ (Emptyᵣ [Empty]) (Unitᵣ [Unit]) → ⊥
Empty≢Unit′ a b ()

Empty≢Unit-red : ∀ {B Γ} → Γ ⊢ B ⇒* Unit → Γ ⊢ Empty ≡ B → ⊥
Empty≢Unit-red D = A≢B (λ Γ l A → Γ ⊩Empty A) (λ Γ l B → Γ ⊩Unit B) Emptyᵣ Unitᵣ
                (λ x → extractMaybeEmb (Empty-elim x))
                (λ x → extractMaybeEmb (Unit-elim′ D x))
                Empty≢Unit′

Empty≢Unitⱼ : ∀ {Γ} → Γ ⊢ Empty ≡ Unit → ⊥
Empty≢Unitⱼ Empty≡Unit =
  let _ , ⊢Unit = syntacticEq Empty≡Unit
  in  Empty≢Unit-red (id ⊢Unit) Empty≡Unit

-- Universe and binding types

U≢B′ : ∀ {B Γ l l′} W
       ([U] : Γ ⊩′⟨ l ⟩U)
       ([W] : Γ ⊩′⟨ l′ ⟩B⟨ W ⟩ B)
     → ShapeView Γ l l′ _ _ (Uᵣ [U]) (Bᵣ W [W]) → ⊥
U≢B′ W a b ()

U≢B-red : ∀ {B F G Γ} W → Γ ⊢ B ⇒* ⟦ W ⟧ F ▹ G → Γ ⊢ U ≡ B → ⊥
U≢B-red W D = A≢B (λ Γ l A → Γ ⊩′⟨ l ⟩U)
                  (λ Γ l A → Γ ⊩′⟨ l ⟩B⟨ W ⟩ A) Uᵣ (Bᵣ W)
                  (λ x → extractMaybeEmb (U-elim x))
                  (λ x → extractMaybeEmb (B-elim′ W D x))
                  (U≢B′ W)

-- U and Π F ▹ G for any F and G cannot be judgmentally equal.
U≢B : ∀ {F G Γ} W → Γ ⊢ U ≡ ⟦ W ⟧ F ▹ G → ⊥
U≢B W U≡W =
  let _ , ⊢W = syntacticEq U≡W
  in  U≢B-red W (id ⊢W) U≡W

U≢Π : ∀ {F G Γ} → _
U≢Π {F} {G} {Γ} = U≢B {F} {G} {Γ} BΠ
U≢Σ : ∀ {F G Γ} → _
U≢Σ {F} {G} {Γ} = U≢B {F} {G} {Γ} BΣ

U≢ne′ : ∀ {K Γ l l′}
       ([U] : Γ ⊩′⟨ l ⟩U)
       ([K] : Γ ⊩ne K)
     → ShapeView Γ l l′ _ _ (Uᵣ [U]) (ne [K]) → ⊥
U≢ne′ a b ()

U≢ne-red : ∀ {B K Γ} → Γ ⊢ B ⇒* K → Neutral K → Γ ⊢ U ≡ B → ⊥
U≢ne-red D neK = A≢B (λ Γ l A → Γ ⊩′⟨ l ⟩U) (λ Γ l B → Γ ⊩ne B) Uᵣ ne
                     (λ x → extractMaybeEmb (U-elim x))
                     (λ x → extractMaybeEmb (ne-elim′ D neK x))
                     U≢ne′

-- U and K for any neutral K cannot be judgmentally equal.
U≢ne : ∀ {K Γ} → Neutral K → Γ ⊢ U ≡ K → ⊥
U≢ne neK U≡K =
  let _ , ⊢K = syntacticEq U≡K
  in  U≢ne-red (id ⊢K) neK U≡K

ℕ≢B′ : ∀ {A B Γ l l′} W
       ([ℕ] : Γ ⊩ℕ A)
       ([W] : Γ ⊩′⟨ l′ ⟩B⟨ W ⟩ B)
     → ShapeView Γ l l′ _ _ (ℕᵣ [ℕ]) (Bᵣ W [W]) → ⊥
ℕ≢B′ W a b ()

ℕ≢B-red : ∀ {A B F G Γ} W → Γ ⊢ A ⇒* ℕ → Γ ⊢ B ⇒* ⟦ W ⟧ F ▹ G → Γ ⊢ A ≡ B → ⊥
ℕ≢B-red W D D′ = A≢B (λ Γ l A → Γ ⊩ℕ A)
                     (λ Γ l A → Γ ⊩′⟨ l ⟩B⟨ W ⟩ A) ℕᵣ (Bᵣ W)
                     (λ x → extractMaybeEmb (ℕ-elim′ D x))
                     (λ x → extractMaybeEmb (B-elim′ W D′ x))
                     (ℕ≢B′ W)

-- ℕ and B F ▹ G for any F and G cannot be judgmentally equal.
ℕ≢B : ∀ {F G Γ} W → Γ ⊢ ℕ ≡ ⟦ W ⟧ F ▹ G → ⊥
ℕ≢B W ℕ≡W =
  let ⊢ℕ , ⊢W = syntacticEq ℕ≡W
  in  ℕ≢B-red W (id ⊢ℕ) (id ⊢W) ℕ≡W

ℕ≢Π : ∀ {F G Γ} → _
ℕ≢Π {F} {G} {Γ} = ℕ≢B {F} {G} {Γ} BΠ
ℕ≢Σ : ∀ {F G Γ} → _
ℕ≢Σ {F} {G} {Γ} = ℕ≢B {F} {G} {Γ} BΣ

-- Empty and Π
Empty≢B′ : ∀ {A B Γ l l′} W
       ([Empty] : Γ ⊩Empty A)
       ([W] : Γ ⊩′⟨ l′ ⟩B⟨ W ⟩ B)
     → ShapeView Γ l l′ _ _ (Emptyᵣ [Empty]) (Bᵣ W [W]) → ⊥
Empty≢B′ W a b ()

Empty≢B-red : ∀ {A B F G Γ} W → Γ ⊢ A ⇒* Empty → Γ ⊢ B ⇒* ⟦ W ⟧ F ▹ G → Γ ⊢ A ≡ B → ⊥
Empty≢B-red W D D′ = A≢B (λ Γ l A → Γ ⊩Empty A)
                         (λ Γ l A → Γ ⊩′⟨ l ⟩B⟨ W ⟩ A) Emptyᵣ (Bᵣ W)
                         (λ x → extractMaybeEmb (Empty-elim′ D x))
                         (λ x → extractMaybeEmb (B-elim′ W D′ x))
                         (Empty≢B′ W)

Empty≢Bⱼ : ∀ {F G Γ} W → Γ ⊢ Empty ≡ ⟦ W ⟧ F ▹ G → ⊥
Empty≢Bⱼ W Empty≡W =
  let ⊢Empty , ⊢W = syntacticEq Empty≡W
  in  Empty≢B-red W (id ⊢Empty) (id ⊢W) Empty≡W

Empty≢Πⱼ : ∀ {F G Γ} → _
Empty≢Πⱼ {F} {G} {Γ} = Empty≢Bⱼ {F} {G} {Γ} BΠ
Empty≢Σⱼ : ∀ {F G Γ} → _
Empty≢Σⱼ {F} {G} {Γ} = Empty≢Bⱼ {F} {G} {Γ} BΣ

-- Unit and Π
Unit≢B′ : ∀ {A B Γ l l′} W
       ([Unit] : Γ ⊩Unit A)
       ([W] : Γ ⊩′⟨ l′ ⟩B⟨ W ⟩ B)
     → ShapeView Γ l l′ _ _ (Unitᵣ [Unit]) (Bᵣ W [W]) → ⊥
Unit≢B′ W a b ()

Unit≢B-red : ∀ {A B F G Γ} W → Γ ⊢ A ⇒* Unit → Γ ⊢ B ⇒* ⟦ W ⟧ F ▹ G → Γ ⊢ A ≡ B → ⊥
Unit≢B-red W D D′ = A≢B (λ Γ l A → Γ ⊩Unit A)
                    (λ Γ l A → Γ ⊩′⟨ l ⟩B⟨ W ⟩ A) Unitᵣ (Bᵣ W)
                    (λ x → extractMaybeEmb (Unit-elim′ D x))
                    (λ x → extractMaybeEmb (B-elim′ W D′ x))
                    (Unit≢B′ W)

Unit≢Bⱼ : ∀ {F G Γ} W → Γ ⊢ Unit ≡ ⟦ W ⟧ F ▹ G → ⊥
Unit≢Bⱼ W Unit≡W =
  let ⊢Unit , ⊢W = syntacticEq Unit≡W
  in  Unit≢B-red W (id ⊢Unit) (id ⊢W) Unit≡W

Unit≢Πⱼ : ∀ {F G Γ} → _
Unit≢Πⱼ {F} {G} {Γ} = Unit≢Bⱼ {F} {G} {Γ} BΠ
Unit≢Σⱼ : ∀ {F G Γ} → _
Unit≢Σⱼ {F} {G} {Γ} = Unit≢Bⱼ {F} {G} {Γ} BΣ

ℕ≢ne′ : ∀ {A K Γ l l′}
       ([ℕ] : Γ ⊩ℕ A)
       ([K] : Γ ⊩ne K)
     → ShapeView Γ l l′ _ _ (ℕᵣ [ℕ]) (ne [K]) → ⊥
ℕ≢ne′ a b ()

ℕ≢ne-red : ∀ {A B K Γ} → Γ ⊢ A ⇒* ℕ → Γ ⊢ B ⇒* K → Neutral K → Γ ⊢ A ≡ B → ⊥
ℕ≢ne-red D D′ neK = A≢B (λ Γ l A → Γ ⊩ℕ A) (λ Γ l B → Γ ⊩ne B) ℕᵣ ne
                        (λ x → extractMaybeEmb (ℕ-elim′ D x))
                        (λ x → extractMaybeEmb (ne-elim′ D′ neK x))
                        ℕ≢ne′

-- ℕ and K for any neutral K cannot be judgmentally equal.
ℕ≢ne : ∀ {K Γ} → Neutral K → Γ ⊢ ℕ ≡ K → ⊥
ℕ≢ne neK ℕ≡K =
  let ⊢ℕ , ⊢K = syntacticEq ℕ≡K
  in  ℕ≢ne-red (id ⊢ℕ) (id ⊢K) neK ℕ≡K

-- Empty and neutral
Empty≢ne′ : ∀ {A K Γ l l′}
       ([Empty] : Γ ⊩Empty A)
       ([K] : Γ ⊩ne K)
     → ShapeView Γ l l′ _ _ (Emptyᵣ [Empty]) (ne [K]) → ⊥
Empty≢ne′ a b ()

Empty≢ne-red : ∀ {A B K Γ} → Γ ⊢ A ⇒* Empty → Γ ⊢ B ⇒* K → Neutral K → Γ ⊢ A ≡ B → ⊥
Empty≢ne-red D D′ neK = A≢B (λ Γ l A → Γ ⊩Empty A) (λ Γ l B → Γ ⊩ne B) Emptyᵣ ne
                        (λ x → extractMaybeEmb (Empty-elim′ D x))
                        (λ x → extractMaybeEmb (ne-elim′ D′ neK x))
                        Empty≢ne′

Empty≢neⱼ : ∀ {K Γ} → Neutral K → Γ ⊢ Empty ≡ K → ⊥
Empty≢neⱼ neK Empty≡K =
  let ⊢Empty , ⊢K = syntacticEq Empty≡K
  in  Empty≢ne-red (id ⊢Empty) (id ⊢K) neK Empty≡K

-- Unit and neutral
Unit≢ne′ : ∀ {A K Γ l l′}
       ([Unit] : Γ ⊩Unit A)
       ([K] : Γ ⊩ne K)
     → ShapeView Γ l l′ _ _ (Unitᵣ [Unit]) (ne [K]) → ⊥
Unit≢ne′ a b ()

Unit≢ne-red : ∀ {A B K Γ} → Γ ⊢ A ⇒* Unit → Γ ⊢ B ⇒* K → Neutral K → Γ ⊢ A ≡ B → ⊥
Unit≢ne-red D D′ neK = A≢B (λ Γ l A → Γ ⊩Unit A) (λ Γ l B → Γ ⊩ne B) Unitᵣ ne
                        (λ x → extractMaybeEmb (Unit-elim′ D x))
                        (λ x → extractMaybeEmb (ne-elim′ D′ neK x))
                        Unit≢ne′

Unit≢neⱼ : ∀ {K Γ} → Neutral K → Γ ⊢ Unit ≡ K → ⊥
Unit≢neⱼ neK Unit≡K =
  let ⊢Unit , ⊢K = syntacticEq Unit≡K
  in  Unit≢ne-red (id ⊢Unit) (id ⊢K) neK Unit≡K

B≢ne′ : ∀ {A K Γ l l′} W
       ([W] : Γ ⊩′⟨ l ⟩B⟨ W ⟩ A)
       ([K] : Γ ⊩ne K)
     → ShapeView Γ l l′ _ _ (Bᵣ W [W]) (ne [K]) → ⊥
B≢ne′ W a b ()

B≢ne-red : ∀ {A B F G K Γ} W → Γ ⊢ A ⇒* ⟦ W ⟧ F ▹ G → Γ ⊢ B ⇒* K → Neutral K
     → Γ ⊢ A ≡ B → ⊥
B≢ne-red W D D′ neK = A≢B (λ Γ l A → Γ ⊩′⟨ l ⟩B⟨ W ⟩ A)
                          (λ Γ l B → Γ ⊩ne B) (Bᵣ W) ne
                          (λ x → extractMaybeEmb (B-elim′ W D x))
                          (λ x → extractMaybeEmb (ne-elim′ D′ neK x))
                          (B≢ne′ W)

-- ⟦ W ⟧ F ▹ G and K for any W, F, G and neutral K cannot be judgmentally equal.
B≢ne : ∀ {F G K Γ} W → Neutral K → Γ ⊢ ⟦ W ⟧ F ▹ G ≡ K → ⊥
B≢ne W neK W≡K =
  let ⊢W , ⊢K = syntacticEq W≡K
  in  B≢ne-red W (id ⊢W) (id ⊢K) neK W≡K

Π≢ne : ∀ {F G K Γ} → _
Π≢ne {F} {G} {K} {Γ} = B≢ne {F} {G} {K} {Γ} BΠ
Σ≢ne : ∀ {F G K Γ} → _
Σ≢ne {F} {G} {K} {Γ} = B≢ne {F} {G} {K} {Γ} BΣ

-- Π and Σ
Π≢Σ′ : ∀ {A B Γ l l′}
       ([A] : Γ ⊩′⟨ l ⟩B⟨ BΠ ⟩ A)
       ([B] : Γ ⊩′⟨ l′ ⟩B⟨ BΣ ⟩ B)
     → ShapeView Γ l l′ _ _ (Bᵣ BΠ [A]) (Bᵣ BΣ [B]) → ⊥
Π≢Σ′ a b ()

Π≢Σ-red : ∀ {A B F G H E Γ} → Γ ⊢ A ⇒* Π F ▹ G → Γ ⊢ B ⇒* Σ H ▹ E → Γ ⊢ A ≡ B → ⊥
Π≢Σ-red D D′ = A≢B (λ Γ l A → Γ ⊩′⟨ l ⟩B⟨ BΠ ⟩ A)
                   (λ Γ l A → Γ ⊩′⟨ l ⟩B⟨ BΣ ⟩ A) (Bᵣ BΠ) (Bᵣ BΣ)
                   (λ x → extractMaybeEmb (B-elim′ BΠ D x))
                   (λ x → extractMaybeEmb (B-elim′ BΣ D′ x))
                   Π≢Σ′

Π≢Σ : ∀ {Γ F G H E} → Γ ⊢ Π F ▹ G ≡ Σ H ▹ E → ⊥
Π≢Σ Π≡Σ =
  let ⊢Π , ⊢Σ = syntacticEq Π≡Σ
  in  Π≢Σ-red (id ⊢Π) (id ⊢Σ) Π≡Σ


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
-}

module LibraBFT.Impl.Base.Types where
  open import LibraBFT.Prelude
  open import LibraBFT.Hash

  NodeId : Set
  NodeId = ℕ

  _≟NodeId_ : (n1 n2 : NodeId) → Dec (n1 ≡ n2)
  _≟NodeId_ = _≟ℕ_

  UID : Set
  UID = Hash

  _≟UID_ : (u₀ u₁ : UID) → Dec (u₀ ≡ u₁)
  _≟UID_ = _≟Hash_

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
module Category.FAM where

open import Level
open import Relation.Binary.PropositionalEquality
open import Function using (_∘_; id; _∘′_)

------------------------------------------------------------------------
-- Functors

record IsFunctor {ℓ} (F : Set ℓ → Set ℓ)
                 (_<$>_ : ∀ {A B} → (A → B) → F A → F B)
                 : Set (suc ℓ) where
    field
        identity : {A : Set ℓ} (a : F A) → id <$> a ≡ a
        homo : ∀ {A B C} (f : B → C) (g : A → B) (a : F A)
            → (f ∘ g) <$> a ≡ f <$> (g <$> a)

record Functor {ℓ} (F : Set ℓ → Set ℓ) : Set (suc ℓ) where
    infixl 4 _<$>_ _<$_
    field
        _<$>_ : ∀ {A B} → (A → B) → F A → F B
        isFunctor : IsFunctor F _<$>_

    -- An textual synonym of _<$>_
    fmap : ∀ {A B} → (A → B) → F A → F B
    fmap = _<$>_

    -- Replace all locations in the input with the same value.
    -- The default definition is fmap . const, but this may be overridden with a
    -- more efficient version.
    _<$_ : ∀ {A B} → A → F B → F A
    x <$ y = Function.const x <$> y

    open IsFunctor isFunctor public

-- open Functor {{...}} public

------------------------------------------------------------------------
-- Applicatives (not indexed)

record IsApplicative {ℓ} (F : Set ℓ → Set ℓ)
                 (pure : {A : Set ℓ} → A → F A)
                 (_⊛_ : {A B : Set ℓ} → (F (A → B)) → F A → F B)
                 : Set (suc ℓ) where
    field
        identity : {A : Set ℓ} (x : F A) → pure id ⊛ x ≡ x
        compose : {A B C : Set ℓ} (f : F (B → C)) (g : F (A → B))
            → (x : F A)
            → ((pure _∘′_ ⊛ f) ⊛ g) ⊛ x ≡ f ⊛ (g ⊛ x)
        homo : ∀ {A B} (f : A → B) (x : A)
             → pure f ⊛ pure x ≡ pure (f x)
        interchange : ∀ {A B} (f : F (A → B)) (x : A)
            → f ⊛ pure x ≡ pure (λ f → f x) ⊛ f

record Applicative {ℓ} (F : Set ℓ → Set ℓ) : Set (suc ℓ) where
    infixl 4 _⊛_ _<⊛_ _⊛>_
    infix  4 _⊗_

    field
        pure : {A : Set ℓ} → A → F A
        _⊛_ : {A B : Set ℓ} → (F (A → B)) → F A → F B
        isApplicative : IsApplicative F pure _⊛_

    open IsApplicative isApplicative public

    _<⊛_ : ∀ {A B} → F A → F B → F A
    x <⊛ y = x

    _⊛>_ : ∀ {A B} → F A → F B → F B
    x ⊛> y = y

    functor : Functor F
    functor = record
        { _<$>_ = λ f x → pure f ⊛ x
        ; isFunctor = record
            { identity = App.identity
            ; homo = λ {A} {B} {C} f g x →
                begin
                    pure (f ∘ g) ⊛ x
                ≡⟨ cong (λ w → _⊛_ w x) (sym (App.homo (λ g → (f ∘ g)) g)) ⟩
                    (pure ((λ g → (f ∘ g))) ⊛ pure g) ⊛ x
                ≡⟨ cong (λ w → (w ⊛ pure g) ⊛ x) (sym (App.homo (λ f → _∘_ f) f)) ⟩
                    ((pure (λ f → _∘_ f) ⊛ pure f) ⊛ pure g) ⊛ x
                ≡⟨ App.compose (pure f) (pure g) x ⟩
                    pure f ⊛ (pure g ⊛ x)
                ∎
            }
        }
        where
            open ≡-Reasoning
            module App = IsApplicative isApplicative

    instance
        ApplicativeFunctor : Functor F
        ApplicativeFunctor = functor

    open import Data.Product
    open Functor {{...}}

    _⊗_ : ∀ {A B} → F A → F B → F (A × B)
    x ⊗ y = _,_ <$> x ⊛ y

    zipWith : ∀ {A B C} → (A → B → C) → F A → F B → F C
    zipWith f x y = f <$> x ⊛ y

-- open Applicative {{...}} public

----------------------------------------------------------------------
-- Monad

record IsMonad {ℓ} (M : Set ℓ → Set ℓ)
                 (return : {A : Set ℓ} → A → M A)
                 (_>>=_ : {A B : Set ℓ} → M A → (A → M B) → M B)
                 : Set (suc ℓ) where
    field
        left-identity : {A B : Set ℓ} (x : A) (fs : A → M B) → return x >>= fs ≡ fs x
        right-identity : {A : Set ℓ} (xs : M A) → xs >>= return ≡ xs
        assoc : {A B C : Set ℓ} (x : M A) (fs : A → M B) (g : B → M C)
            → (x >>= fs) >>= g ≡ (x >>= λ x' → fs x' >>= g)
        temp : {A B : Set ℓ} (x : A) (fs : M (A → B))
            → (fs >>= λ f → return x >>= (return ∘ f)) ≡ (fs >>= λ f → (return ∘ f) x)

record Monad {ℓ} (M : Set ℓ → Set ℓ) : Set (suc ℓ) where
    infixl 1 _>>=_ _>>_ _>=>_
    infixr 1 _=<<_ _<=<_

    field
        return : {A : Set ℓ} → A → M A
        _>>=_ : {A B : Set ℓ} → M A → (A → M B) → M B
        isMonad : IsMonad M return _>>=_

    _>>_ : ∀ {A B} → M A → M B → M B
    m₁ >> m₂ = m₁ >>= λ _ → m₂

    _=<<_ : ∀ {A B} → (A → M B) → M A → M B
    f =<< c = c >>= f

    _>=>_ : ∀ {A : Set ℓ} {B C} → (A → M B) → (B → M C) → (A → M C)
    f >=> g = _=<<_ g ∘ f

    _<=<_ : ∀ {A : Set ℓ} {B C} → (B → M C) → (A → M B) → (A → M C)
    g <=< f = f >=> g

    join : ∀ {A} → M (M A) → M A
    join m = m >>= id

    congruence : ∀ {A B : Set ℓ} (fs : M A) (g h : A → M B)
        → (∀ f → g f ≡ h f)
        → (fs >>= g) ≡ (fs >>= h)
    congruence fs g h prop =
        begin
            (fs >>= g)
        ≡⟨ sym (right-identity (fs >>= g)) ⟩
            (fs >>= g >>= return)
        ≡⟨ assoc fs g return ⟩
            (fs >>= (λ f → g f >>= return))
        ≡⟨ cong (λ w → fs >>= (λ f → w f >>= return)) {!   !} ⟩
            (fs >>= (λ f → h f >>= return))
        ≡⟨ sym (assoc fs h return) ⟩
            (fs >>= h >>= return)
        ≡⟨ right-identity (fs >>= h) ⟩
            (fs >>= h)
        ∎
        where
            open ≡-Reasoning
            open IsMonad isMonad

    -- (fs >>= (λ f → return x >>= return ∘ f))
    -- (fs >>= (λ f → (return ∘ f) x))

    applicative : Applicative M
    applicative = record
        { pure = return
        ; _⊛_ = λ fs xs → fs >>= λ f → xs >>= return ∘′ f
        ; isApplicative = record
            { identity = λ xs → begin
                    (return id >>= λ f → xs >>= λ x → return (f x))
                ≡⟨ Mon.left-identity id (λ f → xs >>= λ x → return (f x)) ⟩
                    (xs >>= λ x → return (id x))
                ≡⟨ refl ⟩
                    (xs >>= λ x → return x)
                ≡⟨ refl ⟩
                    (xs >>= return)
                ≡⟨ Mon.right-identity xs ⟩
                    xs
                ∎
            -- { identity = λ xs → begin
            --         (do
            --             f ← (return id)
            --             x ← xs
            --             (return (f x)))
            --     ≡⟨ Mon.left-identity id (λ f → do
            --             x ← xs
            --             (return (f x)))
            --     ⟩
            --         (do
            --             x ← xs
            --             return (id x))
            --     ≡⟨ refl ⟩
            --         (do
            --             x ← xs
            --             return x)
            --     ≡⟨ Mon.right-identity xs ⟩
            --         xs
            --     ∎

            -- left-identity : {A B : Set ℓ} (x : A) (f : A → M B) → return x >>= f ≡ f x
            -- right-identity : {A : Set ℓ} (xs : M A) → xs >>= return ≡ xs
            -- → (x >>= f) >>= g ≡ (x >>= λ x' → f x' >>= g)
            ; compose = λ fs gs xs → begin
                    (return _∘′_ >>=
                        (λ flip → fs >>= return ∘′ flip) >>=
                        (λ f → gs >>= return ∘′ f) >>=
                        (λ f → xs >>= return ∘′ f))
                ≡⟨ cong (λ w → w >>=
                    (λ f → gs >>= return ∘′ f) >>=
                    (λ f → xs >>= return ∘′ f)) (Mon.left-identity _∘′_ (λ flip → fs >>= return ∘′ flip))
                ⟩
                    (fs >>= return ∘′ _∘′_ >>=
                        (λ f → gs >>= return ∘′ f) >>=
                        (λ f → xs >>= return ∘′ f))
                ≡⟨ Mon.assoc (fs >>= return ∘′ _∘′_) (λ f → gs >>= return ∘′ f) (λ f → xs >>= return ∘′ f) ⟩
                    ((fs >>= return ∘′ _∘′_) >>= (λ h → gs >>= return ∘′ h >>= λ f → xs >>= return ∘′ f))
                ≡⟨ {!   !} ⟩
                    -- {!   !}
                -- ≡⟨ cong (λ w → fs >>= λ r → {!   !}) {!   !} ⟩
                    (fs >>= (λ f → (gs >>= λ g → xs >>= return ∘′ g) >>= return ∘′ f))
                ∎
            ; homo = λ f x → begin
                    (return f >>= λ f' → return x >>= return ∘ f')
                ≡⟨ Mon.left-identity f (λ f' → return x >>= return ∘ f') ⟩
                    (return x >>= return ∘ f)
                ≡⟨ Mon.left-identity x (return ∘ f) ⟩
                    return (f x)
                ∎

            -- left-identity : return x >>= f ≡ f x
            -- right-identity : xs >>= return ≡ xs
            -- assoc : (x >>= f) >>= g ≡ (x >>= λ x' → f x' >>= g)
            ; interchange = λ fs x →
                begin
                    (fs >>= (λ f → return x >>= return ∘ f))
                ≡⟨ congruence fs (λ f → return x >>= return ∘ f) (λ f → (return ∘ f) x) (λ f → Mon.left-identity x (return ∘ f)) ⟩
                    (fs >>= (λ f → (return ∘ f) x))
                ≡⟨ sym (Mon.left-identity (λ f → f x) (λ f' → fs >>= (λ f → return (f' f)))) ⟩
                    (return (λ f → f x) >>= (λ f' → fs >>= (λ f → return (f' f))))
                ∎
            }
        }

    -- -- ≡⟨ sym (Mon.right-identity (fs >>= (λ f → return x >>= return ∘ f))) ⟩
    -- --     (fs >>= (λ f → return x >>= return ∘ f) >>= return)
    -- -- ≡⟨ Mon.assoc fs (λ f → return x >>= return ∘ f) return ⟩
    -- --     (fs >>= (λ f → return x >>= return ∘ f >>= return))
    -- -- ≡⟨ cong (λ w → fs >>= λ f → w f >>= return) {!   !} ⟩
    -- ≡⟨ cong (λ w → w >>= (λ f → return x >>= return ∘ f)) (sym (Mon.right-identity fs)) ⟩
    --     (fs >>= return >>= (λ f → return x >>= return ∘ f))
    -- ≡⟨ Mon.assoc fs return (λ f → return x >>= return ∘ f) ⟩
    --     (fs >>= λ f → return f >>= λ f → return x >>= return ∘ f)
    -- ≡⟨ cong (λ w → fs >>= λ f → w f) {!   !} ⟩
    --     {!   !}
    -- ≡⟨ {!   !} ⟩
    --     (fs >>= (λ f → (return ∘ f) x >>= return))
    -- ≡⟨ sym (Mon.assoc fs (λ f → return (f x)) return) ⟩
    --     ((fs >>= λ f → (return ∘ f) x) >>= return)
    -- ≡⟨ Mon.right-identity (fs >>= λ f → return (f x)) ⟩
        where
            open ≡-Reasoning
            open Applicative applicative
            module Mon = IsMonad isMonad
            --
            -- lemma :  {A B : Set ℓ} (x : A) → (λ f → return x >>= return ∘′ f) ≡ (λ f → return (f x))
            -- lemma x = begin
            --         (λ f → return x >>= return ∘′ f)
            --     ≡⟨ cong (λ w f → w) (Mon.left-identity x (λ f → {!   !})) ⟩
            --         {!   !}
            --     ≡⟨ {!   !} ⟩
            --         {!   !}
            --     ≡⟨ {!   !} ⟩
            --         {!   !}
            --     ≡⟨ {!   !} ⟩
            --         (λ f → return (f x))
            --     ∎
                -- begin
                --     (return x >>= return ∘′ f)
                -- ≡⟨ Mon.left-identity x (return ∘′ f) ⟩
                --     return (f x)
                -- ∎
            -- lemma :  {A B : Set ℓ} (x : A) (f : A → M B) → (return x >>= return ∘′ f) ≡ return (f x)
            -- lemma x f = begin
            --         (return x >>= return ∘′ f)
            --     ≡⟨ Mon.left-identity x (return ∘′ f) ⟩
            --         return (f x)
            --     ∎
--
-- rawIApplicative : RawIApplicative M
-- rawIApplicative = record
-- { pure = return
-- ; _⊛_  = λ f x → f >>= λ f' → x >>= λ x' → return (f' x')
-- }

max_stars_repo_name: banacorn/FAM

max_issues_repo_name: banacorn/FAM

max_forks_repo_name: banacorn/FAM


text:
-- Andreas, 2020-06-21, issue #4768
-- Problem was: @0 appearing in "Not a finite domain" message.

open import Agda.Builtin.Bool
open import Agda.Primitive.Cubical

f : (i : I) → IsOne i → Set
f i (i0 = i1) = Bool

-- EXPECTED:
-- Not a finite domain: IsOne i
-- when checking that the pattern (i0 = i1) has type IsOne i

max_forks_repo_name: shlevy/agda


text:
module ClashingImport where

X = TODO--Can't-make-this-happen!

postulate A : Set

import Imports.A
open Imports.A

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.MonoidSolver.CommSolver where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure

open import Cubical.Data.FinData
open import Cubical.Data.Nat using (ℕ; _+_; iter)
open import Cubical.Data.Vec

open import Cubical.Algebra.CommMonoid

open import Cubical.Algebra.MonoidSolver.MonoidExpression

private
  variable
    ℓ : Level

module Eval (M : CommMonoid ℓ) where
  open CommMonoidStr (snd M)
  open CommMonoidTheory M

  Env : ℕ → Type ℓ
  Env n = Vec ⟨ M ⟩ n

  -- evaluation of an expression (without normalization)
  ⟦_⟧ : ∀{n} → Expr ⟨ M ⟩ n → Env n → ⟨ M ⟩
  ⟦ ε⊗ ⟧ v      = ε
  ⟦ ∣ i ⟧ v     = lookup i v
  ⟦ e₁ ⊗ e₂ ⟧ v = ⟦ e₁ ⟧ v · ⟦ e₂ ⟧ v

  -- a normalform is a vector of multiplicities, counting the occurances of each variable in an expression
  NormalForm : ℕ → Type _
  NormalForm n = Vec ℕ n

  _⊞_ : {n : ℕ} → NormalForm n → NormalForm n → NormalForm n
  x ⊞ y = zipWith _+_ x y

  emptyForm : {n : ℕ} → NormalForm n
  emptyForm = replicate 0

  -- e[ i ] is the i-th unit vector
  e[_] : {n : ℕ} → Fin n → NormalForm n
  e[ Fin.zero ]    = 1 ∷ emptyForm
  e[ (Fin.suc j) ] = 0 ∷ e[ j ]

  -- normalization of an expression
  normalize : {n : ℕ} → Expr ⟨ M ⟩ n → NormalForm n
  normalize (∣ i)     = e[ i ]
  normalize ε⊗        = emptyForm
  normalize (e₁ ⊗ e₂) = (normalize e₁) ⊞ (normalize e₂)

  -- evaluation of normalform
  eval : {n : ℕ} → NormalForm n → Env n → ⟨ M ⟩
  eval [] v = ε
  eval (x ∷ xs) (v ∷ vs) = iter x (λ w → v · w) (eval xs vs)

  -- some calculations
  emptyFormEvaluatesToε : {n : ℕ} (v : Env n) → eval emptyForm v ≡ ε
  emptyFormEvaluatesToε [] = refl
  emptyFormEvaluatesToε (v ∷ vs) = emptyFormEvaluatesToε vs

  UnitVecEvaluatesToVar : ∀{n} (i : Fin n) (v : Env n) →  eval e[ i ] v ≡ lookup i v
  UnitVecEvaluatesToVar zero (v ∷ vs) =
    v · eval emptyForm vs ≡⟨ cong₂ _·_ refl (emptyFormEvaluatesToε vs) ⟩
    v · ε                 ≡⟨ ·IdR _ ⟩
    v                     ∎
  UnitVecEvaluatesToVar (suc i) (v ∷ vs) = UnitVecEvaluatesToVar i vs

  evalIsHom : ∀ {n} (x y : NormalForm n) (v : Env n)
            → eval (x ⊞ y) v ≡ (eval x v) · (eval y v)
  evalIsHom [] [] v = sym (·IdL _)
  evalIsHom (x ∷ xs) (y ∷ ys) (v ∷ vs) =
    lemma x y (evalIsHom xs ys vs)
      where
      lemma : ∀ x y {a b c}(p : a ≡ b · c)
            → iter (x + y) (v ·_) a ≡ iter x (v ·_) b · iter y (v ·_) c
      lemma 0 0 p = p
      lemma 0 (ℕ.suc y) p = (cong₂ _·_ refl (lemma 0 y p)) ∙ commAssocl _ _ _
      lemma (ℕ.suc x) y p = (cong₂ _·_ refl (lemma x y p)) ∙ ·Assoc _ _ _

module EqualityToNormalform (M : CommMonoid ℓ) where
  open Eval M
  open CommMonoidStr (snd M)

  -- proof that evaluation of an expression is invariant under normalization
  isEqualToNormalform : {n : ℕ}
                      → (e : Expr ⟨ M ⟩ n)
                      → (v : Env n)
                      → eval (normalize e) v ≡ ⟦ e ⟧ v
  isEqualToNormalform ε⊗ v = emptyFormEvaluatesToε v
  isEqualToNormalform (∣ i) v = UnitVecEvaluatesToVar i v
  isEqualToNormalform (e₁ ⊗ e₂) v =
    eval ((normalize e₁) ⊞ (normalize e₂)) v          ≡⟨ evalIsHom (normalize e₁) (normalize e₂) v ⟩
    (eval (normalize e₁) v) · (eval (normalize e₂) v) ≡⟨ cong₂ _·_ (isEqualToNormalform e₁ v) (isEqualToNormalform e₂ v) ⟩
    ⟦ e₁ ⟧ v · ⟦ e₂ ⟧ v                               ∎

  solve : {n : ℕ}
        → (e₁ e₂ : Expr ⟨ M ⟩ n)
        → (v : Env n)
        → (p : eval (normalize e₁) v ≡ eval (normalize e₂) v)
        → ⟦ e₁ ⟧ v ≡ ⟦ e₂ ⟧ v
  solve e₁ e₂ v p =
    ⟦ e₁ ⟧ v              ≡⟨ sym (isEqualToNormalform e₁ v) ⟩
    eval (normalize e₁) v ≡⟨ p ⟩
    eval (normalize e₂) v ≡⟨ isEqualToNormalform e₂ v ⟩
    ⟦ e₂ ⟧ v              ∎

solve : (M : CommMonoid ℓ)
        {n : ℕ} (e₁ e₂ : Expr ⟨ M ⟩ n) (v : Eval.Env M n)
        (p :  Eval.eval M (Eval.normalize M e₁) v ≡ Eval.eval M (Eval.normalize M e₂) v)
        → _
solve M = EqualityToNormalform.solve M

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
------------------------------------------------------------------------
-- The cubical identity type
------------------------------------------------------------------------

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

module Equality.Id where

open import Equality
import Equality.Path as P
open import Prelude

import Agda.Builtin.Cubical.Id as Id

------------------------------------------------------------------------
-- Equality

infix 4 _≡_

_≡_ : ∀ {a} {A : Type a} → A → A → Type a
_≡_ = Id.Id

refl : ∀ {a} {A : Type a} {x : A} → x ≡ x
refl = Id.conid P.1̲ P.refl

------------------------------------------------------------------------
-- Various derived definitions and properties

reflexive-relation : ∀ ℓ → Reflexive-relation ℓ
Reflexive-relation._≡_  (reflexive-relation _) = _≡_
Reflexive-relation.refl (reflexive-relation _) = λ _ → refl

equality-with-J₀ : ∀ {a p} → Equality-with-J₀ a p reflexive-relation
Equality-with-J₀.elim      equality-with-J₀ = λ P r → Id.primIdJ
                                                        (λ _ → P) (r _)
Equality-with-J₀.elim-refl equality-with-J₀ = λ _ _ → refl

equivalence-relation⁺ : ∀ ℓ → Equivalence-relation⁺ ℓ
equivalence-relation⁺ _ = J₀⇒Equivalence-relation⁺ equality-with-J₀

equality-with-paths :
  ∀ {a p} → P.Equality-with-paths a p equivalence-relation⁺
equality-with-paths =
  P.Equality-with-J₀⇒Equality-with-paths equality-with-J₀

open P.Derived-definitions-and-properties equality-with-paths public
  hiding (_≡_; refl; reflexive-relation; equality-with-J₀)

open import Equality.Path.Isomorphisms equality-with-paths public

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- Andreas, 2012-02-24 example by Ramana Kumar
{-# OPTIONS --sized-types #-}
-- {-# OPTIONS --show-implicit -v tc.size.solve:20 -v tc.conv.size:15 #-}
module SizeInconsistentMeta4 where

open import Data.Nat using (ℕ;zero;suc) renaming (_<_ to _N<_)
open import Data.Product using (_,_;_×_)
open import Data.List using (List)
open import Relation.Binary using (Rel;_Respects₂_;Transitive;IsEquivalence)
open import Relation.Binary.Product.StrictLex using (×-Lex;×-transitive)
open import Relation.Binary.List.StrictLex using (Lex-<) renaming (transitive to Lex<-trans)

open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)

import Level
open import Size using (Size;↑_)

-- keeping the definition of Vec for the positivity check
infixr 5 _∷_
data Vec {a} (A : Set a) : ℕ → Set a where
  []  : Vec A zero
  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

{- produces different error
data Lex-< {A : _} (_≈_ _<_ : Rel A Level.zero) : Rel (List A) Level.zero where
postulate
  Lex<-trans : ∀ {P _≈_ _<_} →
               IsEquivalence _≈_ → _<_ Respects₂ _≈_ → Transitive _<_ →
               Transitive (Lex-< _≈_ _<_)
-}

postulate
  N<-trans : Transitive _N<_
  -- Vec : ∀ {a} (A : Set a) → ℕ → Set a
  Vec→List : ∀ {a n} {A : Set a} → Vec A n → List A

data Type : {z : Size} → Set where
  TyApp : {z : Size} (n : ℕ) → (as : Vec (Type {z}) n) → Type {↑ z}

infix 4 _<_
data _<_ : {z : Size} → Rel (Type {z}) Level.zero where
  TyApp<TyApp : ∀ {z} {n₁} {as₁} {n₂} {as₂} → ×-Lex _≡_ _N<_ (Lex-< _≡_ (_<_ {z})) (n₁ , Vec→List as₁) (n₂ , Vec→List as₂) → _<_ {↑ z} (TyApp n₁ as₁) (TyApp n₂ as₂)

<-trans : {z : Size} → Transitive (_<_ {z})
<-trans (TyApp<TyApp p) (TyApp<TyApp q) = TyApp<TyApp (×-transitive PropEq.isEquivalence (PropEq.resp₂ _N<_) N<-trans {_≤₂_ = Lex-< _≡_ _<_ } (Lex<-trans PropEq.isEquivalence (PropEq.resp₂ _<_) <-trans) p q)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- Andreas, 2013-12-28
-- Reported by jesper.cockx, Dec 20, 2013

-- WAS:  In the following example, there is an unsolved instance
-- argument, but no part of the code is highlighted.

typeof : ∀ {{T : Set}} → T → Set
typeof {{T}} x = T

test : {A : Set} {B : Set} (y : A) → typeof y
test y = y

-- Should solve the instance argument, no constraint should remain.