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

open import lib.Basics
open import lib.types.Nat
open import lib.types.Sigma

module lib.types.PathSeq where

{-
This is a library on reified equational reasoning.
When you write the following (with the usual equational reasoning combinators):

  t : a == e
  t = a =⟨ p ⟩
      b =⟨ q ⟩
      c =⟨ r ⟩
      d =⟨ s ⟩
      e ∎

it just creates the concatenation of [p], [q], [r] and [s] and there is no way
to say “remove the last step to get the path from [a] to [d]”.
With the present library you would write:

  t : PathSeq a e
  t = a =⟪ p ⟫
      b =⟪ q ⟫
      c =⟪ r ⟫
      d =⟪ s ⟫
      e ∎∎

Then the actual path from [a] to [e] is [↯ t], and you can strip any number
of steps from the beginning or the end:

  ↯ t !2
-}

infix  15 _∎∎
infixr 10 _=⟪_⟫_
infixr 10 _=⟪idp⟫_

data PathSeq {i} {A : Type i} : A → A → Type i where
  _∎∎ : (a : A) → PathSeq a a
  _=⟪_⟫_ : (a : A) {a' a'' : A} (p : a == a') (s : PathSeq a' a'') → PathSeq a a''

infix 30 _=-=_
_=-=_ = PathSeq

_=⟪idp⟫_ : ∀ {i} {A : Type i} (a : A) {a' : A} (s : PathSeq a a') → PathSeq a a'
a =⟪idp⟫ s = s

module _ {i} {A : Type i} where

  infix 0 ↯_

  ↯_ : {a a' : A} (s : PathSeq a a') → a == a'
  ↯ a ∎∎ = idp
  ↯ a =⟪ p ⟫ a' ∎∎ = p
  ↯ a =⟪ p ⟫ s = p ∙ (↯ s)

  private
    point-from-start : (n : ℕ) {a a' : A} (s : PathSeq a a') → A
    point-from-start O {a} s = a
    point-from-start (S n) (a ∎∎) = a
    point-from-start (S n) (a =⟪ p ⟫ s) = point-from-start n s

  _-! : (n : ℕ) {a a' : A} (s : PathSeq a a') → PathSeq (point-from-start n s) a'
  (O -!) s = s
  (S n -!) (a ∎∎) = a ∎∎
  (S n -!) (a =⟪ p ⟫ s) = (n -!) s

  private
    last1 : {a a' : A} (s : PathSeq a a') → A
    last1 (a ∎∎) = a
    last1 (a =⟪ p ⟫ a' ∎∎) = a
    last1 (a =⟪ p ⟫ s) = last1 s

    strip : {a a' : A} (s : PathSeq a a') → PathSeq a (last1 s)
    strip (a ∎∎) = a ∎∎
    strip (a =⟪ p ⟫ a' ∎∎) = a ∎∎
    strip (a =⟪ p ⟫ a' =⟪ p' ⟫ s) = a =⟪ p ⟫ strip (a' =⟪ p' ⟫ s)

    point-from-end : (n : ℕ) {a a' : A} (s : PathSeq a a') → A
    point-from-end O {a} {a'} s = a'
    point-from-end (S n) s = point-from-end n (strip s)

  !- : (n : ℕ) {a a' : A} (s : PathSeq a a') → PathSeq a (point-from-end n s)
  !- O s = s
  !- (S n) s = !- n (strip s)

  _-# : (n : ℕ) {a a' : A} (s : PathSeq a a') → PathSeq a (point-from-start n s)
  (O -#) s = _ ∎∎
  (S n -#) (a ∎∎) = a ∎∎
  (S n -#) (a =⟪ p ⟫ s) = a =⟪ p ⟫ (n -#) s

  private
    split : {a a' : A} (s : PathSeq a a')
      → Σ A (λ a'' → (PathSeq a a'') × (a'' == a'))
    split (a ∎∎) = (a , ((a ∎∎) , idp))
    split (a =⟪ p ⟫ a' ∎∎) = (a , ((a ∎∎) , p))
    split (a =⟪ p ⟫ s) = let (a'' , (t , q)) = split s in (a'' , ((a =⟪ p ⟫ t) , q))

    infix 80 _∙∙_
    _∙∙_ : {a a' a'' : A} (s : PathSeq a a') (p : a' == a'') → PathSeq a a''
    (a ∎∎) ∙∙ p = a =⟪ p ⟫ _ ∎∎
    (a =⟪ p ⟫ s) ∙∙ p' = a =⟪ p ⟫ s ∙∙ p'

    point-from-end' : (n : ℕ) {a a' : A} (s : PathSeq a a') → A
    point-from-end' n (a ∎∎) = a
    point-from-end' O (a =⟪ p ⟫ s) = point-from-end' O s
    point-from-end' (S n) (a =⟪ p ⟫ s) = point-from-end' n (fst (snd (split (a =⟪ p ⟫ s))))

  #- : (n : ℕ) {a a' : A} (s : PathSeq a a') → PathSeq (point-from-end' n s) a'
  #- n (a ∎∎) = a ∎∎
  #- O (a =⟪ p ⟫ s) = #- O s
  #- (S n) (a =⟪ p ⟫ s) = let (a' , (t , q)) = split (a =⟪ p ⟫ s) in #- n t ∙∙ q

  infix 120 _!0 _!1 _!2 _!3 _!4 _!5
  _!0 = !- 0
  _!1 = !- 1
  _!2 = !- 2
  _!3 = !- 3
  _!4 = !- 4
  _!5 = !- 5

  0! = 0 -!
  1! = 1 -!
  2! = 2 -!
  3! = 3 -!
  4! = 4 -!
  5! = 5 -!

  infix 120 _#0 _#1 _#2 _#3 _#4 _#5
  _#0 = #- 0
  _#1 = #- 1
  _#2 = #- 2
  _#3 = #- 3
  _#4 = #- 4
  _#5 = #- 5

  0# = 0 -#
  1# = 1 -#
  2# = 2 -#
  3# = 3 -#
  4# = 4 -#
  5# = 5 -#

  private
    postulate   -- Demo
      a b c d e : A
      p : a == b
      q : b == c
      r : c == d
      s : d == e

    t : PathSeq a e
    t =
      a =⟪ p ⟫
      b =⟪idp⟫
      b =⟪ q ⟫
      c =⟪ idp ⟫
      c =⟪ r ⟫
      d =⟪ s ⟫
      e =⟪idp⟫
      e ∎∎

    t' : a == e
    t' = ↯
      a =⟪ p ⟫
      b =⟪ q ⟫
      c =⟪ idp ⟫
      c =⟪ r ⟫
      d =⟪ s ⟫
      e ∎∎

    ex0 : t' == (↯ t)
    ex0 = idp

    ex1 : t' == p ∙ q ∙ r ∙ s
    ex1 = idp

    ex2 : (↯ t !1) == p ∙ q ∙ r
    ex2 = idp

    ex3 : (↯ t !3) == p ∙ q  -- The [idp] count
    ex3 = idp

    ex4 : (↯ 2! t) == r ∙ s
    ex4 = idp

    ex5 : (↯ 4! t) == s
    ex5 = idp

    ex6 : (↯ t #1) == s
    ex6 = idp

    ex7 : (↯ t #3) == r ∙ s
    ex7 = idp

    ex8 : (↯ 2# t) == p ∙ q
    ex8 = idp

    ex9 : (↯ 4# t) == p ∙ q ∙ r
    ex9 = idp

apd= : ∀ {i j} {A : Type i} {B : A → Type j} {f g : Π A B}
       (p : f ∼ g) {a b : A} (q : a == b)
       → apd f q ▹ p b == p a ◃ apd g q
apd= {B = B} p {b} idp = idp▹ {B = B} (p b) ∙ ! (◃idp {B = B} (p b))

apd=-red : ∀ {i j} {A : Type i} {B : A → Type j} {f g : Π A B}
           (p : f ∼ g) {a b : A} (q : a == b)
           {u : B b} (s : g b =-= u)
           → apd f q ▹ (↯ _ =⟪ p b ⟫ s) == p a ◃ (apd g q ▹ (↯ s))
apd=-red {B = B} p {b} idp s = coh (p b) s  where

  coh : ∀ {i} {A : Type i} {u v w : A} (p : u == v) (s : v =-= w)
    → (idp ∙' (↯ _ =⟪ p ⟫ s)) == p ∙ idp ∙' (↯ s)
  coh idp (a ∎∎) = idp
  coh idp (a =⟪ p₁ ⟫ s₁) = idp

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
{-# OPTIONS --universe-polymorphism #-}

open import Categories.Category
open import Categories.Object.Terminal
open import Level

module Categories.Object.Terminal.Exponentials {o ℓ e : Level}
    (C : Category o ℓ e)
    (T : Terminal C) where

open Category C
open Terminal T

import Categories.Object.Exponential
import Categories.Object.Product
import Categories.Object.Product.Morphisms
import Categories.Object.Terminal.Products

open Categories.Object.Exponential C hiding (repack)
open Categories.Object.Product C
open Categories.Object.Product.Morphisms C
open Categories.Object.Terminal.Products C T

[_↑⊤] : Obj → Obj
[ B ↑⊤] = B

[_↑⊤]-exponential : (B : Obj) → Exponential ⊤ B
[ B ↑⊤]-exponential = record
    { B^A       = [ B ↑⊤]
    ; product   = [ B ×⊤]-product
    ; eval      = id
    ; λg        = λ {X} p g → g ∘ repack [ X ×⊤]-product p
    ; β         = λ {X} p {g} →
        begin
            id ∘ (g ∘ [ p ]⟨ id , ! ⟩) ∘ [ p ]π₁
        ↓⟨ identityˡ ⟩
            (g ∘ [ p ]⟨ id , ! ⟩) ∘ [ p ]π₁
        ↓⟨ assoc ⟩
            g ∘ [ p ]⟨ id , ! ⟩ ∘ [ p ]π₁
        ↓⟨ refl ⟩∘⟨ Product.⟨⟩∘ p ⟩
            g ∘ [ p ]⟨ id ∘ [ p ]π₁ , ! ∘ [ p ]π₁ ⟩
        ↓⟨ refl ⟩∘⟨ Product.⟨⟩-cong₂ p identityˡ (!-unique₂ (! ∘ [ p ]π₁) [ p ]π₂) ⟩
            g ∘ [ p ]⟨ [ p ]π₁ , [ p ]π₂ ⟩
        ↓⟨ refl ⟩∘⟨ Product.η p ⟩
            g ∘ id
        ↓⟨ identityʳ ⟩
            g
        ∎
    ; λ-unique  = λ{X} p {g}{h} h-commutes →
        begin
            h
        ↑⟨ identityʳ ⟩
            h ∘ id
        ↑⟨ refl ⟩∘⟨ Product.commute₁ p ⟩
            h ∘ [ p ]π₁ ∘ [ p ]⟨ id , ! ⟩
        ↑⟨ assoc ⟩
            (h ∘ [ p ]π₁) ∘ [ p ]⟨ id , ! ⟩
        ↑⟨ identityˡ ⟩∘⟨ refl ⟩
            (id ∘ h ∘ [ p ]π₁) ∘ [ p ]⟨ id , ! ⟩
        ↓⟨ h-commutes ⟩∘⟨ refl ⟩
            g ∘ repack [ X ×⊤]-product p
        ∎
    }
    where
    open HomReasoning
    open Equiv

[⊤↑_] : Obj → Obj
[⊤↑ B ] = ⊤

[⊤↑_]-exponential : (A : Obj) → Exponential A ⊤
[⊤↑ A ]-exponential = record
    { B^A       = [⊤↑ A ]
    ; product   = [⊤× A ]-product
    ; eval      = !
    ; λg        = λ _ _ → !
    ; β         = λ _   → !-unique₂ _ _
    ; λ-unique  = λ _ _ → !-unique₂ _ _
    }

ext: agda

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

open import Groups.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Groups.Subgroups.Normal.Definition

module Groups.Subgroups.Normal.Examples {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) where

open import Groups.Subgroups.Examples G
open Setoid S
open Equivalence eq
open Group G

trivialSubgroupIsNormal : normalSubgroup G trivialSubgroup
trivialSubgroupIsNormal {g} k=0 = transitive (+WellDefined reflexive (transitive (+WellDefined k=0 reflexive) identLeft)) (invRight {g})

improperSubgroupIsNormal : normalSubgroup G improperSubgroup
improperSubgroupIsNormal _ = record {}


text:
module Isomorphism where

  import Sets
  open Sets

  infix 20 _≅_

  data _≅_ (A B : Set) : Set where
    iso : (i : A -> B)(j : B -> A) ->
	  (forall x -> j (i x) == x) ->
	  (forall y -> i (j y) == y) ->
	  A ≅ B

  refl-≅ : (A : Set) -> A ≅ A
  refl-≅ A = iso id id (\x -> refl) (\x -> refl)

  iso[×] : {A₁ A₂ B₁ B₂ : Set} -> A₁ ≅ A₂ -> B₁ ≅ B₂ -> A₁ [×] B₁ ≅ A₂ [×] B₂
  iso[×] (iso a₁₂ a₂₁ p₁₁ p₂₂) (iso b₁₂ b₂₁ q₁₁ q₂₂) =
    iso ab₁₂ ab₂₁ pq₁₁ pq₂₂ where

    ab₁₂ = a₁₂ <×> b₁₂
    ab₂₁ = a₂₁ <×> b₂₁

    pq₂₂ : (z : _ [×] _) -> ab₁₂ (ab₂₁ z) == z
    pq₂₂ < x , y > =
      subst (\ ∙ -> < ∙ , b₁₂ (b₂₁ y) > == < x , y >) (p₂₂ x)
      $ cong < x ,∙> (q₂₂ y)

    pq₁₁ : (z : _ [×] _) -> ab₂₁ (ab₁₂ z) == z
    pq₁₁ < x , y > =
      subst (\ ∙ -> < ∙ , b₂₁ (b₁₂ y) > == < x , y >) (p₁₁ x)
      $ cong < x ,∙> (q₁₁ y)

  iso[+] : {A₁ A₂ B₁ B₂ : Set} -> A₁ ≅ A₂ -> B₁ ≅ B₂ -> A₁ [+] B₁ ≅ A₂ [+] B₂
  iso[+] (iso a₁₂ a₂₁ p₁₁ p₂₂) (iso b₁₂ b₂₁ q₁₁ q₂₂) =
    iso ab₁₂ ab₂₁ pq₁₁ pq₂₂ where

    ab₁₂ = a₁₂ <+> b₁₂
    ab₂₁ = a₂₁ <+> b₂₁

    pq₂₂ : (z : _ [+] _) -> ab₁₂ (ab₂₁ z) == z
    pq₂₂ (inl x) = cong inl (p₂₂ x)
    pq₂₂ (inr y) = cong inr (q₂₂ y)

    pq₁₁ : (z : _ [+] _) -> ab₂₁ (ab₁₂ z) == z
    pq₁₁ (inl x) = cong inl (p₁₁ x)
    pq₁₁ (inr y) = cong inr (q₁₁ y)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --cubical --no-import-sorts #-}

module MoreLogic where -- hProp logic

open import MoreLogic.Reasoning public
open import MoreLogic.Definitions public
open import MoreLogic.Properties public

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Properties.Reflexivity {{eqrel : EqRelSet}} where

open import Definition.Untyped
open import Definition.Typed
open import Definition.LogicalRelation

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

-- Reflexivity of reducible types.
reflEq : ∀ {l Γ A} ([A] : Γ ⊩⟨ l ⟩ A) → Γ ⊩⟨ l ⟩ A ≡ A / [A]
reflEq (Uᵣ′ l′ l< ⊢Γ) = (U₌ PE.refl)
reflEq (ℕᵣ D) = ιx (ℕ₌ (red D))
reflEq (ne′ K [ ⊢A , ⊢B , D ] neK K≡K) =
  ιx (ne₌ _ [ ⊢A , ⊢B , D ] neK K≡K)
reflEq (Πᵣ′ F G [ ⊢A , ⊢B , D ] ⊢F ⊢G A≡A [F] [G] G-ext) =
  Π₌ _ _ D A≡A
     (λ ρ ⊢Δ → reflEq ([F] ρ ⊢Δ))
     (λ ρ ⊢Δ [a] → reflEq ([G] ρ ⊢Δ [a]))
reflEq (emb′ 0<1 [A]) = ιx (reflEq [A])

reflNatural-prop : ∀ {Γ n}
                 → Natural-prop Γ n
                 → [Natural]-prop Γ n n
reflNatural-prop (sucᵣ (ℕₜ n d t≡t prop)) =
  sucᵣ (ℕₜ₌ n n d d t≡t
            (reflNatural-prop prop))
reflNatural-prop zeroᵣ = zeroᵣ
reflNatural-prop (ne (neNfₜ neK ⊢k k≡k)) = ne (neNfₜ₌ neK neK k≡k)

-- Reflexivity of reducible terms.
reflEqTerm : ∀ {l Γ A t} ([A] : Γ ⊩⟨ l ⟩ A)
           → Γ ⊩⟨ l ⟩ t ∷ A / [A]
           → Γ ⊩⟨ l ⟩ t ≡ t ∷ A / [A]
reflEqTerm (Uᵣ′ ⁰ 0<1 ⊢Γ) (Uₜ A d typeA A≡A [A]) =
  Uₜ₌ A A d d typeA typeA A≡A [A] [A] (reflEq [A])
reflEqTerm (ℕᵣ D) (ιx (ℕₜ n [ ⊢t , ⊢u , d ] t≡t prop)) =
  ιx (ℕₜ₌ n n [ ⊢t , ⊢u , d ] [ ⊢t , ⊢u , d ] t≡t
      (reflNatural-prop prop))
reflEqTerm (ne′ K D neK K≡K) (ιx (neₜ k d (neNfₜ neK₁ ⊢k k≡k))) =
  ιx (neₜ₌ k k d d (neNfₜ₌ neK₁ neK₁ k≡k))
reflEqTerm (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Πₜ f d funcF f≡f [f] [f]₁) =
  Πₜ₌ f f d d funcF funcF f≡f
      (Πₜ f d funcF f≡f [f] [f]₁)
      (Πₜ f d funcF f≡f [f] [f]₁)
      (λ ρ ⊢Δ [a] → [f] ρ ⊢Δ [a] [a] (reflEqTerm ([F] ρ ⊢Δ) [a]))
reflEqTerm (emb′ 0<1 [A]) (ιx t) = ιx (reflEqTerm [A] t)

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
open import Oscar.Prelude
open import Oscar.Class.IsPrecategory
open import Oscar.Class.Transitivity

module Oscar.Class.Precategory where

record Precategory 𝔬 𝔯 ℓ : Ø ↑̂ (𝔬 ∙̂ 𝔯 ∙̂ ℓ) where
  constructor ∁
  infix 4 _∼̇_
  field
    {𝔒} : Ø 𝔬
    _∼_ : 𝔒 → 𝔒 → Ø 𝔯
    _∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ
    _↦_ : Transitivity.type _∼_
    ⦃ `IsPrecategory ⦄ : IsPrecategory _∼_ _∼̇_ _↦_


text:
------------------------------------------------------------------------
-- Fixity and associativity
------------------------------------------------------------------------

module RecursiveDescent.Hybrid.Mixfix.Fixity where

open import Data.Fin using (Fin; zero; suc; #_)
open import Data.Fin.Props using (eq?)
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

data Associativity : Set where
  left  : Associativity
  right : Associativity
  non   : Associativity

-- A combination of fixity and associativity. Only infix operators
-- have associativity.

-- Note that infix is a reserved word.

data Fixity : Set where
  prefx  : Fixity
  infx   : (assoc : Associativity) -> Fixity
  postfx : Fixity
  closed : Fixity

Fixity-is-finite : LeftInverse Fixity (Fin 6)
Fixity-is-finite = record
  { from         = from
  ; to           = to
  ; left-inverse = left-inverse
  }
  where
  to : Fixity -> Fin 6
  to prefx        = # 0
  to (infx left)  = # 1
  to (infx right) = # 2
  to (infx non)   = # 3
  to postfx       = # 4
  to closed       = # 5

  from : Fin 6 -> Fixity
  from zero                                   = prefx
  from (suc zero)                             = infx left
  from (suc (suc zero))                       = infx right
  from (suc (suc (suc zero)))                 = infx non
  from (suc (suc (suc (suc zero))))           = postfx
  from (suc (suc (suc (suc (suc zero)))))     = closed
  from (suc (suc (suc (suc (suc (suc ()))))))

  left-inverse : from LeftInverseOf to
  left-inverse prefx        = refl
  left-inverse (infx left)  = refl
  left-inverse (infx right) = refl
  left-inverse (infx non)   = refl
  left-inverse postfx       = refl
  left-inverse closed       = refl

_≟_ : Decidable (_≡_ {Fixity})
_≟_ = eq? injection
  where open LeftInverse Fixity-is-finite

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module logic where

open import Level
open import Relation.Nullary
open import Relation.Binary hiding (_⇔_ )
open import Data.Empty

data Bool : Set where
    true : Bool
    false : Bool

record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
   constructor ⟪_,_⟫
   field
      proj1 : A
      proj2 : B

data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
   case1 : A → A ∨ B
   case2 : B → A ∨ B

_⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
_⇔_ A B =  ( A → B ) ∧ ( B → A )

∧-exch : {n m : Level} {A  : Set n} { B : Set m } → A ∧ B → B ∧ A
∧-exch p = ⟪ _∧_.proj2 p , _∧_.proj1 p ⟫

∨-exch : {n m : Level} {A  : Set n} { B : Set m } → A ∨ B → B ∨ A
∨-exch (case1 x) = case2 x
∨-exch (case2 x) = case1 x

contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a )

double-neg : {n  : Level } {A : Set n} → A → ¬ ¬ A
double-neg A notnot = notnot A

double-neg2 : {n  : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
double-neg2 notnot A = notnot ( double-neg A )

de-morgan : {n  : Level } {A B : Set n} →  A ∧ B  → ¬ ( (¬ A ) ∨ (¬ B ) )
de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))

dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
dont-or {A} {B} (case2 b) ¬A = b

dont-orb :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ B → A
dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
dont-orb {A} {B} (case1 a) ¬B = a

infixr  130 _∧_
infixr  140 _∨_
infixr  150 _⇔_

_/\_ : Bool → Bool → Bool
true /\ true = true
_ /\ _ = false

_\/_ : Bool → Bool → Bool
false \/ false = false
_ \/ _ = true

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

_<=>_ : Bool → Bool → Bool
true <=> true = true
false <=> false = true
_ <=> _ = false

open import Relation.Binary.PropositionalEquality

record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)  where
   field
       fun←  :  S → R
       fun→  :  R → S
       fiso← : (x : R)  → fun← ( fun→ x )  ≡ x
       fiso→ : (x : S ) → fun→ ( fun← x )  ≡ x

injection :  {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m)
injection R S f = (x y : R) → f x ≡ f y → x ≡ y

¬t=f : (t : Bool ) → ¬ ( not t ≡ t)
¬t=f true ()
¬t=f false ()

infixr  130 _\/_
infixr  140 _/\_

≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B
≡-Bool-func {true} {true} a→b b→a = refl
≡-Bool-func {false} {true} a→b b→a with b→a refl
... | ()
≡-Bool-func {true} {false} a→b b→a with a→b refl
... | ()
≡-Bool-func {false} {false} a→b b→a = refl

bool-≡-? : (a b : Bool) → Dec ( a ≡ b )
bool-≡-? true true = yes refl
bool-≡-? true false = no (λ ())
bool-≡-? false true = no (λ ())
bool-≡-? false false = yes refl

¬-bool-t : {a : Bool} →  ¬ ( a ≡ true ) → a ≡ false
¬-bool-t {true} ne = ⊥-elim ( ne refl )
¬-bool-t {false} ne = refl

¬-bool-f : {a : Bool} →  ¬ ( a ≡ false ) → a ≡ true
¬-bool-f {true} ne = refl
¬-bool-f {false} ne = ⊥-elim ( ne refl )

¬-bool : {a : Bool} →  a ≡ false  → a ≡ true → ⊥
¬-bool refl ()

lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥
lemma-∧-0 {true} {true} refl ()
lemma-∧-0 {true} {false} ()
lemma-∧-0 {false} {true} ()
lemma-∧-0 {false} {false} ()

lemma-∧-1 : {a b : Bool} → a /\ b ≡ true → b ≡ false → ⊥
lemma-∧-1 {true} {true} refl ()
lemma-∧-1 {true} {false} ()
lemma-∧-1 {false} {true} ()
lemma-∧-1 {false} {false} ()

bool-and-tt : {a b : Bool} → a ≡ true → b ≡ true → ( a /\ b ) ≡ true
bool-and-tt refl refl = refl

bool-∧→tt-0 : {a b : Bool} → ( a /\ b ) ≡ true → a ≡ true
bool-∧→tt-0 {true} {true} refl = refl
bool-∧→tt-0 {false} {_} ()

bool-∧→tt-1 : {a b : Bool} → ( a /\ b ) ≡ true → b ≡ true
bool-∧→tt-1 {true} {true} refl = refl
bool-∧→tt-1 {true} {false} ()
bool-∧→tt-1 {false} {false} ()

bool-or-1 : {a b : Bool} → a ≡ false → ( a \/ b ) ≡ b
bool-or-1 {false} {true} refl = refl
bool-or-1 {false} {false} refl = refl
bool-or-2 : {a b : Bool} → b ≡ false → (a \/ b ) ≡ a
bool-or-2 {true} {false} refl = refl
bool-or-2 {false} {false} refl = refl

bool-or-3 : {a : Bool} → ( a \/ true ) ≡ true
bool-or-3 {true} = refl
bool-or-3 {false} = refl

bool-or-31 : {a b : Bool} → b ≡ true  → ( a \/ b ) ≡ true
bool-or-31 {true} {true} refl = refl
bool-or-31 {false} {true} refl = refl

bool-or-4 : {a : Bool} → ( true \/ a ) ≡ true
bool-or-4 {true} = refl
bool-or-4 {false} = refl

bool-or-41 : {a b : Bool} → a ≡ true  → ( a \/ b ) ≡ true
bool-or-41 {true} {b} refl = refl

bool-and-1 : {a b : Bool} →  a ≡ false → (a /\ b ) ≡ false
bool-and-1 {false} {b} refl = refl
bool-and-2 : {a b : Bool} →  b ≡ false → (a /\ b ) ≡ false
bool-and-2 {true} {false} refl = refl
bool-and-2 {false} {false} refl = refl

max_stars_repo_name: shinji-kono/HyperReal-in-agda

max_issues_repo_name: shinji-kono/HyperReal-in-agda

max_forks_repo_name: shinji-kono/HyperReal-in-agda


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Instances.Semilattice where

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.Semilattice

open import Cubical.Categories.Category
open import Cubical.Categories.Instances.Poset

open Category

module _ {ℓ} (L : Semilattice ℓ) where

  open MeetSemilattice L

  SemilatticeCategory : Category ℓ ℓ
  SemilatticeCategory = PosetCategory IndPoset

max_stars_repo_name: mzeuner/cubical

max_issues_repo_name: mzeuner/cubical

max_forks_repo_name: mzeuner/cubical


text:
-- Andreas, 2013-03-22
module Issue473a where

data D : Set where
  d : D

data P : D → Set where
  p : P d

record Rc : Set where
  constructor c
  field f : D

works : {r : Rc} → P (Rc.f r) → Set
works p = D

works' : (r : Rc) → P (Rc.f r) → Set
works' (c .d) p = D

-- We remove the constructor:

record R : Set where
  field f : D

test : {r : R} → P (R.f r) → Set
test p = D

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Ad-hoc monoid typeclass module

module Utils.Monoid where

open import Data.List
open import Data.String

record Monoid {α}(A : Set α) : Set α where
  constructor rec
  field
    append   : A → A → A
    identity : A

infixr 5 _<>_
_<>_ : ∀ {α}{A : Set α} ⦃ _ : Monoid A ⦄ → A → A → A
_<>_ ⦃ dict ⦄ a b = Monoid.append dict a b

mempty : ∀ {α}{A : Set α} ⦃ _ : Monoid A ⦄ → A
mempty ⦃ dict ⦄ = Monoid.identity dict

instance
  MonoidList : ∀ {α A} → Monoid {α} (List A)
  MonoidList = rec Data.List._++_ []

  MonoidString : Monoid String
  MonoidString = rec Data.String._++_ ""

max_stars_repo_name: AndrasKovacs/SemanticsWithApplications

max_issues_repo_name: AndrasKovacs/SemanticsWithApplications

max_forks_repo_name: AndrasKovacs/SemanticsWithApplications


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

-- Exposes the core of hott
module hott.core where

-- The basic types of hott

open import hott.core.equality  public -- Equality type
open import hott.core.sigma     public -- Dependent pairs
open import hott.core.universe  public -- Universes
open import hott.core.universe.pointed public
                                       -- and the pointed ones.

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


text:
-- 2016-01-14 Andreas, issue reported by Martin Stone Davis

open import Common.Equality

module _ {K : Set} where

record Map : Set where
  field
    unmap : K

record _∉_ (k : K) (m : Map) : Set where
  field
    un∉ : Map.unmap m ≡ k

pattern ∉∅ = record { un∉ = refl }

not-here : ∀ {k : K} {m : Map} (k∉m : k ∉ m) → Set
not-here ∉∅ = K

-- WAS: internal error due to record pattern not yet treated
-- for pattern synonyms.


text:
open import Theory
open import Categories.Category using (Category)
open import Categories.Category.CartesianClosed

module Soundness {o ℓ e}
  (𝒞 : Category o ℓ e)
  (CC : CartesianClosed 𝒞)
  {ℓ₁ ℓ₂ ℓ₃}
  (Th : Theory ℓ₁ ℓ₂ ℓ₃)
  where

  open Theory.Theory Th
  open import Semantics 𝒞 CC Sg
  open import Syntax
  open Term Sg

  open import Categories.Category.Cartesian 𝒞
  open import Categories.Category.BinaryProducts 𝒞
  open import Categories.Object.Product 𝒞
  open import Categories.Object.Terminal 𝒞 using (Terminal)

  open Category 𝒞
  open CartesianClosed CC
  open Cartesian cartesian
  open BinaryProducts products
  module T = Terminal terminal

  open import Data.Product using (Σ; Σ-syntax; proj₁; proj₂)

  module _ (M : Model 𝒞 CC Th) where
    open Structure (proj₁ M)
    open HomReasoning

    soundness : forall {Γ A} {e₁ e₂ : Γ ⊢ A}
      -> Γ ⊢ e₁ ≡ e₂
      -> ⟦ e₁ ⟧ ≈ ⟦ e₂ ⟧
    soundness-sub : forall {Γ Γ′} {γ₁ γ₂ : Γ ⊨ Γ′}
      -> Γ ⊨ γ₁ ≡ γ₂
      -> ⟦ γ₁ ⟧S ≈ ⟦ γ₂ ⟧S

    soundness (ax x) = proj₂ M x
    soundness refl = Equiv.refl
    soundness (sym D) = Equiv.sym (soundness D)
    soundness (trans D D₁) = Equiv.trans (soundness D) (soundness D₁)
    soundness sub/id = identityʳ
    soundness sub/∙ = sym-assoc
    soundness (eta/Unit e) = T.!-unique ⟦ e ⟧
    soundness (beta/*₁ _ e₂) = project₁
    soundness (beta/*₂ e₁ _) = project₂
    soundness (eta/* _) = g-η
    soundness (beta/=> e e′) =
      begin
        ⟦ app (abs e) e′ ⟧
      ≈˘⟨ ∘-resp-≈ʳ (Equiv.trans ⁂∘⟨⟩ (⟨⟩-cong₂ identityʳ identityˡ)) ⟩
        eval′ ∘ (λg ⟦ e ⟧ ⁂ Category.id 𝒞) ∘ ⟨ Category.id 𝒞 , ⟦ e′ ⟧ ⟩
      ≈⟨ Equiv.trans sym-assoc (∘-resp-≈ˡ β′) ⟩
        ⟦ e [ ext Term.id e′ ] ⟧
      ∎
    soundness (eta/=> e) =
      begin
        ⟦ abs (app (e [ weaken ]) var) ⟧
      ≈˘⟨ λ-cong (∘-resp-≈ʳ (⟨⟩-cong₂ Equiv.refl identityˡ)) ⟩
        λg (eval′ ∘ ⟨ ⟦ e ⟧ ∘ π₁ , Category.id 𝒞 ∘ π₂ ⟩)
      ≈˘⟨ λ-cong (∘-resp-≈ʳ ⁂∘⟨⟩) ⟩
        λg (eval′ ∘ (⟦ e ⟧ ⁂ Category.id 𝒞) ∘ ⟨ π₁ , π₂ ⟩)
      ≈⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ η)) ⟩
        λg (eval′ ∘ (⟦ e ⟧ ⁂ Category.id 𝒞) ∘ Category.id 𝒞)
      ≈⟨ λ-cong (∘-resp-≈ʳ identityʳ) ⟩
        λg (eval′ ∘ (⟦ e ⟧ ⁂ Category.id 𝒞))
      ≈⟨ η-exp′ ⟩
        ⟦ e ⟧
      ∎
    soundness (comm/func _ Γ′ γ f e) = assoc
    soundness (comm/unit _ Γ′ γ) = Equiv.sym (T.!-unique (T.! ∘ ⟦ γ ⟧S))
    soundness comm/pair = Product.∘-distribʳ-⟨⟩ product
    soundness comm/fst = assoc
    soundness comm/snd = assoc
    soundness (comm/abs {γ = γ} {e = e}) =
      begin
        λg ⟦ e ⟧ ∘ ⟦ γ ⟧S
      ≈⟨ exp.subst product product ⟩
        λg (⟦ e ⟧ ∘ (⟦ γ ⟧S ⁂ Category.id 𝒞))
      ≈˘⟨ λ-cong (∘-resp-≈ʳ (Equiv.trans (∘-resp-≈ʳ η) identityʳ)) ⟩
        λg (⟦ e ⟧ ∘ (⟦ γ ⟧S ⁂ Category.id 𝒞) ∘ ⟨ π₁ , π₂ ⟩)
      ≈⟨ λ-cong (∘-resp-≈ʳ (⁂∘⟨⟩)) ⟩
        λg (⟦ e ⟧ ∘ ⟨ ⟦ γ ⟧S ∘ π₁ , Category.id 𝒞 ∘ π₂ ⟩)
      ≈⟨ λ-cong (∘-resp-≈ʳ (⟨⟩-cong₂ Equiv.refl identityˡ)) ⟩
        λg (⟦ e ⟧ ∘ ⟨ ⟦ γ ⟧S ∘ π₁ , π₂ ⟩ )
      ∎
    soundness comm/app = Equiv.trans assoc (∘-resp-≈ʳ ⟨⟩∘)
    soundness (var/ext γ _) = project₂
    soundness (cong/sub D D′) = ∘-resp-≈ (soundness D′) (soundness-sub D)
    soundness (cong/pair D D₁) = ⟨⟩-cong₂ (soundness D) (soundness D₁)
    soundness (cong/fst D) = ∘-resp-≈ʳ (soundness D)
    soundness (cong/snd D) = ∘-resp-≈ʳ (soundness D)
    soundness (cong/app D D₁) = ∘-resp-≈ʳ (⟨⟩-cong₂ (soundness D) (soundness D₁))
    soundness (cong/abs D) = λ-cong (soundness D)
    soundness (cong/func D) = ∘-resp-≈ Equiv.refl (soundness D)

    soundness-sub refl = Equiv.refl
    soundness-sub (sym D) = Equiv.sym (soundness-sub D)
    soundness-sub (trans D D₁) = Equiv.trans (soundness-sub D) (soundness-sub D₁)
    soundness-sub (!-unique {γ = γ}) = T.!-unique ⟦ γ ⟧S
    soundness-sub η-pair =
      begin
        ⟨ π₁ , π₂ ⟩
      ≈⟨ Product.η product ⟩
        Category.id 𝒞
      ∎
    soundness-sub ext∙ = ⟨⟩∘
    soundness-sub (cong/ext D D′) = ⟨⟩-cong₂ (soundness-sub D) (soundness D′)
    soundness-sub weaken/ext = project₁
    soundness-sub (cong/∙ D D₁) = ∘-resp-≈ (soundness-sub D) (soundness-sub D₁)
    soundness-sub id∙ˡ = identityˡ
    soundness-sub id∙ʳ = identityʳ
    soundness-sub assoc∙ = assoc

max_stars_repo_name: elpinal/exsub-ccc

max_issues_repo_name: elpinal/exsub-ccc

max_forks_repo_name: elpinal/exsub-ccc


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

open import lib.Basics

module lib.types.TwoSemiCategory where

module _ {i j} {El : Type i} (Arr : El → El → Type j)
  (_ : ∀ x y → has-level 1 (Arr x y)) where

  record TwoSemiCategoryStructure : Type (lmax i j) where
    field
      comp : ∀ {x y z} → Arr x y → Arr y z → Arr x z
      assoc : ∀ {x y z w} (a : Arr x y) (b : Arr y z) (c : Arr z w)
        → comp (comp a b) c == comp a (comp b c)
      {- coherence -}
      pentagon-identity : ∀ {v w x y z} (a : Arr v w) (b : Arr w x) (c : Arr x y) (d : Arr y z)
        → assoc (comp a b) c d ◃∙
          assoc a b (comp c d) ◃∎
          =ₛ
          ap (λ s → comp s d) (assoc a b c) ◃∙
          assoc a (comp b c) d ◃∙
          ap (comp a) (assoc b c d) ◃∎

record TwoSemiCategory i j : Type (lsucc (lmax i j)) where
  constructor two-semi-category
  field
    El : Type i
    Arr : El → El → Type j
    Arr-level : ∀ x y → has-level 1 (Arr x y)
    two-semi-cat-struct : TwoSemiCategoryStructure Arr Arr-level

  open TwoSemiCategoryStructure two-semi-cat-struct public

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
open import Categories
open import Functors
open import RMonads

module RMonads.REM.Adjunction {a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}
                              {J : Fun C D}(M : RMonad J)  where

open import Library
open import RAdjunctions
open import RMonads.REM M
open import RMonads.REM.Functors J M

open Fun
open RAdj
open RAlg
open RAlgMorph
open RMonad M
open Cat D

REMAdj : RAdj J EM
REMAdj = record {
  L = REML;
  R = REMR;
  left   = λ f → comp (amor f) η;
  right  = λ{_ B} f → record{
    amor = astr B f;
    ahom = sym (alaw2 B)};
  lawa    = λ {_ Y} f →
    RAlgMorphEq (
      proof
      astr Y (comp (amor f) η)
      ≅⟨ sym (ahom f) ⟩
      comp (amor f) (bind η)
      ≅⟨ cong (comp (amor f)) law1 ⟩
      comp (amor f) iden
      ≅⟨ idr ⟩
      amor f ∎);
  lawb    = λ {_ B} f → sym (alaw1 B);
  natleft = λ f g h →
    proof
    comp (amor g) (comp (comp (amor h) η) (HMap J f))
    ≅⟨ cong (comp (amor g)) ass ⟩
    comp (amor g) (comp (amor h) (comp η (HMap J f)))
    ≅⟨ cong (comp (amor g) ∘ comp (amor h)) (sym law2) ⟩
    comp (amor g) (comp (amor h) (comp (bind (comp η (HMap J f))) η))
    ≅⟨ cong (comp (amor g)) (sym ass) ⟩
    comp (amor g) (comp (comp (amor h) (bind (comp η (HMap J f)))) η)
    ≅⟨ sym ass ⟩
    comp (comp (amor g) (comp (amor h) (bind (comp η (HMap J f))))) η
    ∎;
  natright = λ{W}{X}{Y}{Z} f g h →
    RAlgMorphEq (
      proof
      astr Z (comp (amor g) (comp h (HMap J f)))
      ≅⟨ sym (ahom g) ⟩
      comp (amor g) (astr Y (comp h (HMap J f)))
      ≅⟨ cong (λ h₁ → comp (amor g) (astr Y (comp h₁ (HMap J f)))) (alaw1 Y) ⟩
      comp (amor g) (astr Y (comp (comp (astr Y h) η) (HMap J f)))
      ≅⟨ cong (comp (amor g) ∘ astr Y) ass ⟩
      comp (amor g) (astr Y (comp (astr Y h) (comp η (HMap J f))))
      ≅⟨ cong (comp (amor g)) (alaw2 Y) ⟩
      comp (amor g) (comp (astr Y h) (bind (comp η (HMap J f))))
      ∎)}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


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

open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Rings.Homomorphisms.Definition
open import Rings.Ideals.Definition

module Rings.Homomorphisms.Kernel {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_+1_ _*1_ : A → A → A} {_+2_ _*2_ : B → B → B} {R1 : Ring S _+1_ _*1_} {R2 : Ring T _+2_ _*2_} {f : A → B} (fHom : RingHom R1 R2 f) where

open import Groups.Homomorphisms.Kernel (RingHom.groupHom fHom)

ringKernelIsIdeal : Ideal R1 groupKernelPred
Ideal.isSubgroup ringKernelIsIdeal = groupKernelIsSubgroup
Ideal.accumulatesTimes ringKernelIsIdeal {x} {y} fx=0 = transitive (RingHom.ringHom fHom) (transitive (Ring.*WellDefined R2 fx=0 reflexive) (transitive (Ring.*Commutative R2) (Ring.timesZero R2)))
  where
    open Setoid T
    open Equivalence eq


text:
-- Andreas, 2017-07-28, issue #776 reported by p.giarusso on 30 Dec 2012

open import Agda.Primitive

-- Note Set₁ instead of Set (suc l)
data _:=:_ {l : Level} (A : Set l) (B : Set l) : Set₁ where
  proof : {F : Set l → Set l} → F A → F B → A :=: B

-- WAS: no error message

-- Expected:
-- The type of the constructor does not fit in the sort of the
-- datatype, since Set (lsuc l) is not less or equal than Set₁
-- when checking the constructor proof in the declaration of _:=:_

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Cubical.HITs.Susp
open import Cubical.Data.Nat
open import Cubical.Data.NatMinusOne
open import Cubical.Data.Empty
open import Cubical.Foundations.Prelude

S₊ : ℕ₋₁ → Type₀
S₊ neg1 = ⊥
S₊ (suc n) = Susp (S₊ n)

S : ℕ → Type₀
S n = S₊ (ℕ→ℕ₋₁ n)

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
{-# OPTIONS -v treeless:20 #-}
module _ where

data N : Set where
  zero : N
  suc : N → N

_+_ : N → N → N
zero + n = n
suc m + n = suc (m + n)

record P A B : Set where
  constructor _,_
  field fst : A
        snd : B

open P

{-# INLINE fst #-}
{-# INLINE snd #-}

-- Without handling repeated cases:
-- g = λ a → case a of b , c → b (case a of d , e → e)
-- Should be
-- g = λ a → case a of b , c → b c
g : P (N → N) N → N
g z = fst z (snd z)

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
import Structure.Logic.Classical.NaturalDeduction

-- TODO: MAybe rename to SetBoundedQuantification
module Structure.Logic.Classical.SetTheory.SetBoundedQuantification {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} ⦃ classicLogic : _ ⦄ (_∈_ : Domain → Domain → Formula) where
open Structure.Logic.Classical.NaturalDeduction.ClassicalLogic {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} (classicLogic)

open import Functional hiding (Domain)
open import Lang.Instance
import      Lvl
open import Type.Dependent
open import Structure.Logic.Classical.PredicateBoundedQuantification {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} ⦃ classicLogic ⦄

-- Bounded universal quantifier
∀ₛ : Domain → (Domain → Formula) → Formula
∀ₛ(S)(P) = ∀ₚ(_∈ S)(P)

[∀ₛ]-intro : ∀{S}{P} → (∀{x} → Proof(x ∈ S) → Proof(P(x))) → Proof(∀ₛ(S)(P))
[∀ₛ]-intro = [∀ₚ]-intro

[∀ₛ]-elim : ∀{S}{P} → Proof(∀ₛ(S)(P)) → ∀{x} → Proof(x ∈ S) → Proof(P(x))
[∀ₛ]-elim = [∀ₚ]-elim

-- Bounded existential quantifier
∃ₛ : Domain → (Domain → Formula) → Formula
∃ₛ(S)(P) = ∃ₚ(_∈ S)(P)

[∃ₛ]-intro : ∀{S}{P}{x} → Proof(x ∈ S) → Proof(P(x)) → Proof(∃ₛ(S)(P))
[∃ₛ]-intro = [∃ₚ]-intro

[∃ₛ]-elim : ∀{S}{P}{Q} → (∀{x} → Proof(x ∈ S) → Proof(P(x)) → Proof(Q)) → Proof(∃ₛ(S)(P)) → Proof(Q)
[∃ₛ]-elim = [∃ₚ]-elim

[∃ₛ]-witness : ∀{S : Domain}{P : Domain → Formula} → ⦃ _ : Proof(∃ₛ S P) ⦄ → Domain
[∃ₛ]-witness = [∃ₚ]-witness

[∃ₛ]-domain : ∀{S : Domain}{P : Domain → Formula} → ⦃ p : Proof(∃ₛ S P) ⦄ → Proof([∃ₛ]-witness{S}{P} ⦃ p ⦄ ∈ S)
[∃ₛ]-domain = [∃ₚ]-bound

[∃ₛ]-proof : ∀{S : Domain}{P : Domain → Formula} → ⦃ p : Proof(∃ₛ S P) ⦄ → Proof(P([∃ₛ]-witness{S}{P} ⦃ p ⦄))
[∃ₛ]-proof = [∃ₚ]-proof

Uniqueₛ : Domain → (Domain → Formula) → Formula
Uniqueₛ(S)(P) = Uniqueₚ(_∈ S)(P)

-- Bounded unique existential quantifier
∃ₛ! : Domain → (Domain → Formula) → Formula
∃ₛ!(S)(P) = ∃ₚ!(_∈ S)(P)

[∃ₛ!]-witness : ∀{S : Domain}{P : Domain → Formula} → ⦃ _ : Proof(∃ₛ! S P) ⦄ → Domain
[∃ₛ!]-witness = [∃ₚ!]-witness

[∃ₛ!]-domain : ∀{S : Domain}{P : Domain → Formula} → ⦃ p : Proof(∃ₛ! S P) ⦄ → Proof([∃ₛ!]-witness{S}{P} ⦃ p ⦄ ∈ S)
[∃ₛ!]-domain = [∃ₚ!]-bound

[∃ₛ!]-proof : ∀{S : Domain}{P : Domain → Formula} → ⦃ p : Proof(∃ₛ! S P) ⦄ → Proof(P([∃ₛ!]-witness{S}{P} ⦃ p ⦄))
[∃ₛ!]-proof = [∃ₚ!]-proof

[∃ₛ!]-unique : ∀{S : Domain}{P : Domain → Formula} → ⦃ p : Proof(∃ₛ! S P) ⦄ → Proof(∀ₗ(x ↦ P(x) ⟶ (x ≡ [∃ₛ!]-witness{S}{P} ⦃ p ⦄)))
[∃ₛ!]-unique = [∃ₚ!]-unique

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
-- Andreas, AIM XXIII 2016-04-21 Overloaded projections

-- Milestone 1: Check overloaded projections on rhs (without postponing).

module _ (A : Set) (a : A) where

module RecDefs where

  record R B : Set where
    field f : B
  open R public

  record S B : Set where
    field f : B
  open S public

  record T B : Set where
    field f : B → B
  open T public

open RecDefs public

r : R A
R.f r = a

s : S A
S.f s = f r

t : R A → S A
S.f (t r) = f r

u : _
u = f s

v = f s

w : ∀{A} → T A → A → A
w t x = f t x

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Non-empty lists
------------------------------------------------------------------------

module Data.List.NonEmpty where

open import Category.Monad
open import Data.Bool
open import Data.Bool.Properties
open import Data.List as List using (List; []; _∷_)
open import Data.Maybe using (nothing; just)
open import Data.Nat as Nat
open import Data.Product using (∃; proj₁; proj₂; _,_; ,_)
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
open import Data.Unit
open import Data.Vec as Vec using (Vec; []; _∷_)
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence
  using () renaming (module Equivalence to Eq)
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
open import Relation.Nullary.Decidable using (⌊_⌋)

------------------------------------------------------------------------
-- Non-empty lists

infixr 5 _∷_

record List⁺ {a} (A : Set a) : Set a where
  constructor _∷_
  field
    head : A
    tail : List A

open List⁺ public

[_] : ∀ {a} {A : Set a} → A → List⁺ A
[ x ] = x ∷ []

infixr 5 _∷⁺_

_∷⁺_ : ∀ {a} {A : Set a} → A → List⁺ A → List⁺ A
x ∷⁺ y ∷ xs = x ∷ y ∷ xs

length : ∀ {a} {A : Set a} → List⁺ A → ℕ
length (x ∷ xs) = suc (List.length xs)

------------------------------------------------------------------------
-- Conversion

toList : ∀ {a} {A : Set a} → List⁺ A → List A
toList (x ∷ xs) = x ∷ xs

fromVec : ∀ {n a} {A : Set a} → Vec A (suc n) → List⁺ A
fromVec (x ∷ xs) = x ∷ Vec.toList xs

toVec : ∀ {a} {A : Set a} (xs : List⁺ A) → Vec A (length xs)
toVec (x ∷ xs) = x ∷ Vec.fromList xs

lift : ∀ {a b} {A : Set a} {B : Set b} →
       (∀ {m} → Vec A (suc m) → ∃ λ n → Vec B (suc n)) →
       List⁺ A → List⁺ B
lift f xs = fromVec (proj₂ (f (toVec xs)))

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

map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → List⁺ A → List⁺ B
map f (x ∷ xs) = (f x ∷ List.map f xs)

-- Right fold. Note that s is only applied to the last element (see
-- the examples below).

foldr : ∀ {a b} {A : Set a} {B : Set b} →
        (A → B → B) → (A → B) → List⁺ A → B
foldr {A = A} {B} c s (x ∷ xs) = foldr′ x xs
  where
  foldr′ : A → List A → B
  foldr′ x []       = s x
  foldr′ x (y ∷ xs) = c x (foldr′ y xs)

-- Left fold. Note that s is only applied to the first element (see
-- the examples below).

foldl : ∀ {a b} {A : Set a} {B : Set b} →
        (B → A → B) → (A → B) → List⁺ A → B
foldl c s (x ∷ xs) = List.foldl c (s x) xs

-- Append (several variants).

infixr 5 _⁺++⁺_ _++⁺_ _⁺++_

_⁺++⁺_ : ∀ {a} {A : Set a} → List⁺ A → List⁺ A → List⁺ A
(x ∷ xs) ⁺++⁺ (y ∷ ys) = x ∷ (xs List.++ y ∷ ys)

_⁺++_ : ∀ {a} {A : Set a} → List⁺ A → List A → List⁺ A
(x ∷ xs) ⁺++ ys = x ∷ (xs List.++ ys)

_++⁺_ : ∀ {a} {A : Set a} → List A → List⁺ A → List⁺ A
xs ++⁺ ys = List.foldr _∷⁺_ ys xs

concat : ∀ {a} {A : Set a} → List⁺ (List⁺ A) → List⁺ A
concat (xs ∷ xss) = xs ⁺++ List.concat (List.map toList xss)

monad : ∀ {f} → RawMonad (List⁺ {a = f})
monad = record
  { return = [_]
  ; _>>=_  = λ xs f → concat (map f xs)
  }

reverse : ∀ {a} {A : Set a} → List⁺ A → List⁺ A
reverse = lift (,_ ∘′ Vec.reverse)

-- Snoc.

infixl 5 _∷ʳ_ _⁺∷ʳ_

_∷ʳ_ : ∀ {a} {A : Set a} → List A → A → List⁺ A
[]       ∷ʳ y = [ y ]
(x ∷ xs) ∷ʳ y = x ∷ (xs List.∷ʳ y)

_⁺∷ʳ_ : ∀ {a} {A : Set a} → List⁺ A → A → List⁺ A
xs ⁺∷ʳ x = toList xs ∷ʳ x

-- A snoc-view of non-empty lists.

infixl 5 _∷ʳ′_

data SnocView {a} {A : Set a} : List⁺ A → Set a where
  _∷ʳ′_ : (xs : List A) (x : A) → SnocView (xs ∷ʳ x)

snocView : ∀ {a} {A : Set a} (xs : List⁺ A) → SnocView xs
snocView (x ∷ xs)              with List.initLast xs
snocView (x ∷ .[])             | []            = []       ∷ʳ′ x
snocView (x ∷ .(xs List.∷ʳ y)) | xs List.∷ʳ' y = (x ∷ xs) ∷ʳ′ y

-- The last element in the list.

last : ∀ {a} {A : Set a} → List⁺ A → A
last xs with snocView xs
last .(ys ∷ʳ y) | ys ∷ʳ′ y = y

-- Groups all contiguous elements for which the predicate returns the
-- same result into lists.

split : ∀ {a} {A : Set a}
        (p : A → Bool) → List A →
        List (List⁺ (∃ (T ∘ p)) ⊎ List⁺ (∃ (T ∘ not ∘ p)))
split p []       = []
split p (x ∷ xs) with p x | P.inspect p x | split p xs
... | true  | P.[ px≡t ] | inj₁ xs′ ∷ xss = inj₁ ((x , Eq.from T-≡     ⟨$⟩ px≡t) ∷⁺ xs′) ∷ xss
... | true  | P.[ px≡t ] | xss            = inj₁ [ x , Eq.from T-≡     ⟨$⟩ px≡t ]        ∷ xss
... | false | P.[ px≡f ] | inj₂ xs′ ∷ xss = inj₂ ((x , Eq.from T-not-≡ ⟨$⟩ px≡f) ∷⁺ xs′) ∷ xss
... | false | P.[ px≡f ] | xss            = inj₂ [ x , Eq.from T-not-≡ ⟨$⟩ px≡f ]        ∷ xss

-- If we flatten the list returned by split, then we get the list we
-- started with.

flatten : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} →
          List (List⁺ (∃ P) ⊎ List⁺ (∃ Q)) → List A
flatten = List.concat ∘
          List.map Sum.[ toList ∘ map proj₁ , toList ∘ map proj₁ ]

flatten-split :
  ∀ {a} {A : Set a}
  (p : A → Bool) (xs : List A) → flatten (split p xs) ≡ xs
flatten-split p []       = refl
flatten-split p (x ∷ xs)
  with p x | P.inspect p x | split p xs | flatten-split p xs
... | true  | P.[ _ ] | []         | hyp = P.cong (_∷_ x) hyp
... | true  | P.[ _ ] | inj₁ _ ∷ _ | hyp = P.cong (_∷_ x) hyp
... | true  | P.[ _ ] | inj₂ _ ∷ _ | hyp = P.cong (_∷_ x) hyp
... | false | P.[ _ ] | []         | hyp = P.cong (_∷_ x) hyp
... | false | P.[ _ ] | inj₁ _ ∷ _ | hyp = P.cong (_∷_ x) hyp
... | false | P.[ _ ] | inj₂ _ ∷ _ | hyp = P.cong (_∷_ x) hyp

-- Groups all contiguous elements /not/ satisfying the predicate into
-- lists. Elements satisfying the predicate are dropped.

wordsBy : ∀ {a} {A : Set a} → (A → Bool) → List A → List (List⁺ A)
wordsBy p =
  List.gfilter Sum.[ const nothing , just ∘′ map proj₁ ] ∘ split p

------------------------------------------------------------------------
-- Examples

-- Note that these examples are simple unit tests, because the type
-- checker verifies them.

private
 module Examples {A B : Set}
                 (_⊕_ : A → B → B)
                 (_⊗_ : B → A → B)
                 (f : A → B)
                 (a b c : A)
                 where

  hd : head (a ∷⁺ b ∷⁺ [ c ]) ≡ a
  hd = refl

  tl : tail (a ∷⁺ b ∷⁺ [ c ]) ≡ b ∷ c ∷ []
  tl = refl

  mp : map f (a ∷⁺ b ∷⁺ [ c ]) ≡ f a ∷⁺ f b ∷⁺ [ f c ]
  mp = refl

  right : foldr _⊕_ f (a ∷⁺ b ∷⁺ [ c ]) ≡ a ⊕ (b ⊕ f c)
  right = refl

  left : foldl _⊗_ f (a ∷⁺ b ∷⁺ [ c ]) ≡ (f a ⊗ b) ⊗ c
  left = refl

  ⁺app⁺ : (a ∷⁺ b ∷⁺ [ c ]) ⁺++⁺ (b ∷⁺ [ c ]) ≡
          a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
  ⁺app⁺ = refl

  ⁺app : (a ∷⁺ b ∷⁺ [ c ]) ⁺++ (b ∷ c ∷ []) ≡
          a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
  ⁺app = refl

  app⁺ : (a ∷ b ∷ c ∷ []) ++⁺ (b ∷⁺ [ c ]) ≡
          a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
  app⁺ = refl

  conc : concat ((a ∷⁺ b ∷⁺ [ c ]) ∷⁺ [ b ∷⁺ [ c ] ]) ≡
         a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
  conc = refl

  rev : reverse (a ∷⁺ b ∷⁺ [ c ]) ≡ c ∷⁺ b ∷⁺ [ a ]
  rev = refl

  snoc : (a ∷ b ∷ c ∷ []) ∷ʳ a ≡ a ∷⁺ b ∷⁺ c ∷⁺ [ a ]
  snoc = refl

  snoc⁺ : (a ∷⁺ b ∷⁺ [ c ]) ⁺∷ʳ a ≡ a ∷⁺ b ∷⁺ c ∷⁺ [ a ]
  snoc⁺ = refl

  split-true : split (const true) (a ∷ b ∷ c ∷ []) ≡
               inj₁ ((a , tt) ∷⁺ (b , tt) ∷⁺ [ c , tt ]) ∷ []
  split-true = refl

  split-false : split (const false) (a ∷ b ∷ c ∷ []) ≡
                inj₂ ((a , tt) ∷⁺ (b , tt) ∷⁺ [ c , tt ]) ∷ []
  split-false = refl

  split-≡1 :
    split (λ n → ⌊ n Nat.≟ 1 ⌋) (1 ∷ 2 ∷ 3 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ []) ≡
    inj₁ [ 1 , tt ] ∷ inj₂ ((2 , tt) ∷⁺ [ 3 , tt ]) ∷
    inj₁ ((1 , tt) ∷⁺ [ 1 , tt ]) ∷ inj₂ [ 2 , tt ] ∷ inj₁ [ 1 , tt ] ∷
    []
  split-≡1 = refl

  wordsBy-true : wordsBy (const true) (a ∷ b ∷ c ∷ []) ≡ []
  wordsBy-true = refl

  wordsBy-false : wordsBy (const false) (a ∷ b ∷ c ∷ []) ≡
                  (a ∷⁺ b ∷⁺ [ c ]) ∷ []
  wordsBy-false = refl

  wordsBy-≡1 :
    wordsBy (λ n → ⌊ n Nat.≟ 1 ⌋) (1 ∷ 2 ∷ 3 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ []) ≡
    (2 ∷⁺ [ 3 ]) ∷ [ 2 ] ∷ []
  wordsBy-≡1 = refl


text:
open import Relation.Binary using (IsDecEquivalence)
open import Agda.Builtin.Equality

module UnifyWith (FunctionName : Set) ⦃ isDecEquivalenceA : IsDecEquivalence (_≡_ {A = FunctionName}) ⦄ where

open import UnifyTermF FunctionName
open import UnifyMguF FunctionName
open import UnifyMguCorrectF FunctionName

open import Data.Fin using (Fin; suc; zero)
open import Data.Nat hiding (_≤_)
open import Relation.Binary.PropositionalEquality renaming ([_] to [[_]])
open import Function using (_∘_; id; case_of_; _$_; flip)
open import Relation.Nullary
open import Data.Product renaming (map to _***_)
open import Data.Empty
open import Data.Maybe
open import Category.Functor
open import Category.Monad
import Level
open RawMonad (Data.Maybe.monad {Level.zero})
open import Data.Sum
open import Data.Maybe using (maybe; maybe′; nothing; just; monad; Maybe)
open import Data.List renaming (_++_ to _++L_)
open ≡-Reasoning
open import Data.Vec using (Vec; []; _∷_) renaming (_++_ to _++V_; map to mapV)

open import Data.Unit

-- moved to UnifyMguCorrectF


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

module Data.Quiver.Morphism where

-- Morphism of Quivers, as well as some useful kit (identity, composition, equivalence)
-- also define map on paths, and that it behaves well wrt morphisms and morphism equivalence.

-- See the further comments around the definition of equivalence, as that is quite the
-- mine field.

open import Level
open import Function using () renaming (id to idFun; _∘_ to _⊚_)
open import Data.Quiver
open import Data.Quiver.Paths using (module Paths)
open import Relation.Binary using (IsEquivalence; Reflexive; Symmetric; Transitive)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (Star; gmap; ε; _◅_)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; naturality)
open import Relation.Binary.PropositionalEquality.Properties
  using (trans-symʳ; trans-symˡ)
open import Relation.Binary.PropositionalEquality.Subst.Properties
  using (module Shorthands; module Transport; module TransportOverQ; module TransportMor; module TransportStar)

infix 4 _≃_

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

-- A Morphism of Quivers. As this is meant to be used as the underlying part of a
-- Category, the fields should be named the same as for Functor.
record Morphism (G : Quiver o ℓ e) (G′ : Quiver o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  private
    module G  = Quiver G
    module G′ = Quiver G′

  field
    F₀       : G.Obj → G′.Obj
    F₁       : ∀ {A B} → A G.⇒ B → F₀ A G′.⇒ F₀ B
    F-resp-≈ : ∀ {A B} {f g : A G.⇒ B} → f G.≈ g → F₁ f G′.≈ F₁ g

id : {G : Quiver o ℓ e} → Morphism G G
id = record { F₀ = idFun ; F₁ = idFun ; F-resp-≈ = idFun }

_∘_ : {G₁ G₂ G₃ : Quiver o ℓ e} (m₁ : Morphism G₂ G₃) (m₂ : Morphism G₁ G₂) → Morphism G₁ G₃
m₁ ∘ m₂ = record
  { F₀ = F₀ m₁ ⊚ F₀ m₂
  ; F₁ = F₁ m₁ ⊚ F₁ m₂
  ; F-resp-≈ = F-resp-≈ m₁ ⊚ F-resp-≈ m₂
  }
  where open Morphism

-- Morphism equivalence.  Note how it is mixed, with
-- propositional equivalence mixed with edge-setoid equivalence.

-- Ideally, we'd like something weaker, aking to natural isomorphism  here.
-- However, there is no notion of composition (nor identity) for edges, so that
-- doesn't work (no commuting squares in quivers, so the naturality condition cannot
-- be written down).  So one choice that works is to be strict. Note that introducing
-- node equality might work too, but that would be even further from the notion of
-- category used here, so that we could not reasonably end up with an adjoint.

record _≃_ {G : Quiver o ℓ e} {G′ : Quiver o′ ℓ′ e′}
    (M M′ : Morphism G G′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  open Quiver G using (_⇒_)
  open Quiver G′ using (_≈_)
  private
    module M  = Morphism M
    module M′ = Morphism M′
  open Shorthands (Quiver._⇒_ G′)

  -- Pick a presentation of equivalence for graph morphisms that works
  -- well with functor equality.

  field
    F₀≡ : ∀ {X} → M.F₀ X ≡ M′.F₀ X
    F₁≡ : ∀ {A B} {f : A ⇒ B} → M.F₁ f ▸ F₀≡ ≈ F₀≡ ◂ M′.F₁ f

-- Prove that ≃ is an equivalence relation
module _ {G : Quiver o ℓ e} {G′ : Quiver o′ ℓ′ e′} where
  open Quiver
  open Morphism
  open _≃_

  private
    ≃-refl : Reflexive {A = Morphism G G′} _≃_
    ≃-refl = record { F₀≡ = refl ; F₁≡ = Equiv.refl G′}

    ≃-sym : Symmetric {A = Morphism G G′} _≃_
    ≃-sym {i} {j} eq = record
      { F₀≡ = sym (F₀≡ eq)
      ; F₁≡ = λ {_ _ f} →
        let open EdgeReasoning G′
            open Transport (_⇒_ G′)
            open TransportOverQ (_⇒_ G′) (_≈_ G′)
            e₁ = F₀≡ eq
        in begin
          F₁ j f ▸ sym e₁                        ≡˘⟨ cong (_◂ (F₁ j f ▸ _)) (trans-symˡ e₁) ⟩
          trans (sym e₁) e₁ ◂ (F₁ j f ▸ sym e₁)  ≡˘⟨ ◂-assocˡ (sym e₁) (F₁ j f ▸ sym e₁) ⟩
          sym e₁ ◂ e₁ ◂ (F₁ j f ▸ sym e₁)        ≡⟨ cong (sym e₁ ◂_) (◂-▸-comm e₁ (F₁ j f) (sym e₁)) ⟩
          sym e₁ ◂ ((e₁ ◂ F₁ j f) ▸ sym e₁)      ≈˘⟨ ◂-resp-≈ (sym e₁) (▸-resp-≈ (F₁≡ eq) (sym e₁)) ⟩
          sym e₁ ◂ (F₁ i f ▸ e₁ ▸ sym e₁)        ≡⟨ cong (sym e₁ ◂_) (▸-assocʳ (F₁ i f) (sym e₁)) ⟩
          sym e₁ ◂ (F₁ i f ▸ trans e₁ (sym e₁))  ≡⟨ cong (λ p → sym e₁ ◂ (F₁ i f ▸ p)) (trans-symʳ e₁) ⟩
          sym e₁ ◂ F₁ i f                        ∎
      }

    ≃-trans : Transitive {A = Morphism G G′} _≃_
    ≃-trans {i} {j} {k} eq eq′ = record
      { F₀≡ = trans (F₀≡ eq) (F₀≡ eq′)
      ; F₁≡ = λ {_ _ f} →
        let open EdgeReasoning G′
            open Transport (_⇒_ G′)
            open TransportOverQ (_⇒_ G′) (_≈_ G′)
        in begin
          F₁ i f ▸ trans (F₀≡ eq) (F₀≡ eq′)  ≡˘⟨ ▸-assocʳ (F₁ i f) (F₀≡ eq′) ⟩
          (F₁ i f ▸ F₀≡ eq) ▸ F₀≡ eq′        ≈⟨ ▸-resp-≈ (F₁≡ eq) (F₀≡ eq′) ⟩
          (F₀≡ eq ◂ F₁ j f) ▸ F₀≡ eq′        ≡˘⟨ ◂-▸-comm (F₀≡ eq) (F₁ j f) (F₀≡ eq′) ⟩
          F₀≡ eq ◂ (F₁ j f ▸ F₀≡ eq′)        ≈⟨ ◂-resp-≈ (F₀≡ eq) (F₁≡ eq′) ⟩
          F₀≡ eq ◂ (F₀≡ eq′ ◂ F₁ k f)        ≡⟨ ◂-assocˡ (F₀≡ eq) (F₁ k f) ⟩
          trans (F₀≡ eq) (F₀≡ eq′) ◂ F₁ k f  ∎
      }

  ≃-Equivalence : IsEquivalence _≃_
  ≃-Equivalence = record
      { refl  = ≃-refl
      ; sym   = ≃-sym
      ; trans = ≃-trans {- λ {G i j k} eq eq′ →  -}
      }

-- Furthermore, it respects morphism composition
≃-resp-∘ : {A B C : Quiver o ℓ e} {f g : Morphism B C} {h i : Morphism A B} →
  f ≃ g → h ≃ i → (f ∘ h) ≃ (g ∘ i)
≃-resp-∘ {B = G} {H} {f} {g} {h} {i} eq eq′ = record
  { F₀≡ = trans (cong (F₀ f) (F₀≡ eq′)) (F₀≡ eq)
  ; F₁≡ = λ {_ _ j} →
    let open EdgeReasoning H
        open Transport (_⇒_ H)
        open TransportOverQ (_⇒_ H) (_≈_ H)
        open Transport (_⇒_ G) using () renaming (_▸_ to _▹_; _◂_ to _◃_)
        open TransportMor (_⇒_ G) (_⇒_ H)
        e₁ = F₀≡ eq
        e₂ = F₀≡ eq′
    in begin
      F₁ (f ∘ h) j ▸ trans (cong (F₀ f) e₂) e₁    ≡˘⟨ ▸-assocʳ (F₁ f (F₁ h j)) e₁ ⟩
      F₁ f (F₁ h j) ▸ cong (F₀ f) e₂ ▸ e₁         ≡˘⟨ cong (_▸ e₁) ( M-resp-▸ (F₀ f) (F₁ f) (F₁ h j) e₂) ⟩
      F₁ f (F₁ h j ▹ e₂) ▸ e₁                     ≈⟨ F₁≡ eq ⟩
      e₁ ◂ F₁ g (F₁ h j ▹ e₂)                     ≈⟨ ◂-resp-≈ e₁ (F-resp-≈ g (F₁≡ eq′)) ⟩
      e₁ ◂ F₁ g (e₂ ◃ F₁ i j)                     ≡⟨ cong (e₁ ◂_) (M-resp-◂ (F₀ g) (F₁ g) e₂ (F₁ i j) ) ⟩
      e₁ ◂ cong (F₀ g) e₂ ◂ F₁ g (F₁ i j)         ≡⟨ ◂-assocˡ e₁ (F₁ g (F₁ i j)) ⟩
      trans e₁ (cong (F₀ g) e₂) ◂ F₁ g (F₁ i j)   ≡˘⟨ cong (_◂ F₁ g (F₁ i j)) (naturality (λ _ → e₁)) ⟩
      trans (cong (F₀ f) e₂) e₁ ◂ F₁ g (F₁ i j)   ∎
  }
  where
    open Quiver using (_⇒_; _≈_; module EdgeReasoning)
    open Morphism
    open _≃_

-- We can induce a map from paths in on quiver to the in the target
module _ {G₁ G₂ : Quiver o ℓ e} (G⇒ : Morphism G₁ G₂) where
  open Quiver G₁ renaming (_⇒_ to _⇒₁_; Obj to Obj₁)
  open Quiver G₂ renaming (_⇒_ to _⇒₂_; Obj to Obj₂; module Equiv to Equiv₂)
  open Morphism G⇒ using (F₀; F₁; F-resp-≈)
  open Paths renaming (_≈*_ to [_]_≈*_)

  qmap : {A B : Obj₁} → Star _⇒₁_ A B → Star _⇒₂_ (F₀ A) (F₀ B)
  qmap = gmap F₀ F₁

  -- this is needed, because this uses F-resp-≈ and not ≡
  -- unlike gmap-cong
  map-resp : {A B : Obj₁} (f : Star _⇒₁_ A B) {g : Star _⇒₁_ A B} →
      [ G₁ ] f ≈* g → [ G₂ ] qmap f ≈* qmap g
  map-resp ε ε = ε
  map-resp (x ◅ f) (f≈* ◅ eq) = F-resp-≈ f≈* ◅ map-resp f eq

module _ {G H : Quiver o ℓ e} {f g : Morphism G H}
         (f≈g : f ≃ g) where
  open Quiver G
  open Paths H using (_≈*_; _◅_)
  open Morphism
  open _≃_ f≈g
  open Transport (Quiver._⇒_ H)
  open TransportStar (Quiver._⇒_ H)

  map-F₁≡ : {A B : Obj} (hs : Star _⇒_ A B) →
            qmap f hs ▸* F₀≡ ≈* F₀≡ ◂* qmap g hs
  map-F₁≡ ε        = Paths.≡⇒≈* H (◂*-▸*-ε F₀≡)
  map-F₁≡ (hs ◅ h) = begin
    (F₁ f hs ◅ qmap f h) ▸* F₀≡   ≡⟨ ◅-▸* (F₁ f hs) _ F₀≡ ⟩
    F₁ f hs ◅ (qmap f h ▸* F₀≡)   ≈⟨ Quiver.Equiv.refl H ◅ map-F₁≡ h ⟩
    F₁ f hs ◅ (F₀≡ ◂* qmap g h)   ≡⟨ ◅-◂*-▸ (F₁ f hs) F₀≡ _ ⟩
    (F₁ f hs ▸ F₀≡) ◅ qmap g h    ≈⟨ F₁≡ ◅ (Paths.refl H) ⟩
    (F₀≡ ◂ F₁ g hs) ◅ qmap g h    ≡˘⟨ ◂*-◅ F₀≡ (F₁ g hs) _ ⟩
    F₀≡ ◂* (F₁ g hs ◅ qmap g h)   ∎
    where open Paths.PathEqualityReasoning H

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module Highlighting where

Set-one : Set₂
Set-one = Set₁

record R (A : Set) : Set-one where
  constructor con

  field X : Set

  F : Set → Set → Set
  F A B = B

  field P : F A X → Set

  -- Note: we cannot check highlighting of non-termination
  -- any more (Andreas, 2014-09-05), since termination failure
  -- is a type error now.
  {-# NON_TERMINATING #-}
  Q : F A X → Set
  Q = Q

postulate P : _

open import Highlighting.M

data D (A : Set) : Set-one where
  d : let X = D in X A


text:
module SecondOrder.MContext {ℓ} (arity : Set ℓ) (sort : Set ℓ)  where

  data MContext : Set ℓ where
    ctx-empty : MContext
    ctx-slot : arity → sort → MContext
    _,,_ : MContext → MContext → MContext

  infixl 5 _,,_

  infix 4 [_,_]∈_

  -- the meta-variables of a given type in a context
  data [_,_]∈_ (Λ : arity) (A : sort) : MContext → Set ℓ where
    var-slot : [ Λ , A ]∈ ctx-slot Λ A
    var-inl : ∀ {Θ ψ} (x : [ Λ , A ]∈ Θ) → [ Λ , A ]∈ Θ ,, ψ
    var-inr : ∀ {Θ ψ} (y : [ Λ , A ]∈ ψ) → [ Λ , A ]∈ Θ ,, ψ

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
module _ where

open import Common.Prelude hiding (_>>=_)
open import Common.Reflection
open import Common.Equality

module _ (A : Set) where
  record R : Set where

  `R₀ : Type
  `R₀ = def (quote R) []

  `R₁ : Term → Type
  `R₁ a = def (quote R) (vArg a ∷ [])

  `Nat : Type
  `Nat = def (quote Nat) []

  _`→_ : Type → Type → Type
  a `→ b = pi (vArg a) (abs "x" b)

  helper-type₀ : Type
  helper-type₀ = `R₀ `→ `R₀

  helper-type₁ : Type
  helper-type₁ = `R₁ `Nat `→ `R₁ `Nat

  helper-term : Term
  helper-term = var 0 []

  helper-patterns : List (Arg Pattern)
  helper-patterns = vArg (var "_") ∷
                    []

  defineHelper : Type → TC ⊤
  defineHelper t =
    freshName "n" >>= λ n →
    declareDef (vArg n) t >>= λ _ →
    defineFun n (clause helper-patterns helper-term ∷ [])

  noFail : TC ⊤ → TC Bool
  noFail m = catchTC (bindTC m λ _ → returnTC true) (returnTC false)

  mac : Type → Tactic
  mac t hole =
    noFail (defineHelper t) >>= λ b →
    quoteTC b >>= unify hole

  macro
    mac₀ : Tactic
    mac₀ = mac helper-type₀

    mac₁ : Tactic
    mac₁ = mac helper-type₁

  within-module-succeeds₀ : mac₀ ≡ true
  within-module-succeeds₀ = refl

  within-module-fails₁ : mac₁ ≡ false
  within-module-fails₁ = refl

outside-module-fails₀ : mac₀ Nat ≡ false
outside-module-fails₀ = refl

outside-module-succeeds₁ : mac₁ Nat ≡ true
outside-module-succeeds₁ = refl


text:
------------------------------------------------------------------------
-- Well-typed substitutions
------------------------------------------------------------------------

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

module Data.Fin.Substitution.Typed where

open import Data.Context as Ctx hiding (map)
open import Data.Context.WellFormed
open import Data.Context.Properties using (module ContextFormationLemmas)
open import Data.Fin using (Fin; zero; suc)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Nat using (ℕ; suc)
open import Data.Vec as Vec using (Vec; []; _∷_; map)
open import Data.Vec.Properties using (map-cong; map-∘; lookup-map)
open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
  using (Pointwise; []; _∷_)
open import Function as Fun using (_∘_)
open import Level using (_⊔_) renaming (zero to lzero; suc to lsuc)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Relation.Unary using (Pred)

------------------------------------------------------------------------
-- Abstract typing
--
-- Well-typed substitutions are defined over an abstract "type
-- system", i.e. a pair of formation and typing judgments and
-- substitution lemmas for raw terms and types.

-- An abtract typing judgment _⊢_∈_ : Typing Bnd Term Type is a
-- ternary relation which, in a given Bnd-context, relates Term-terms
-- to their Type-types.

Typing : ∀ {t₁ t₂ t₃} →
         Pred ℕ t₁ → Pred ℕ t₂ → Pred ℕ t₃ → ∀ ℓ →
         Set (t₁ ⊔ t₂ ⊔ t₃ ⊔ lsuc ℓ)
Typing Bnd Term Type ℓ = ∀ {n} → Ctx Bnd n → Term n → Type n → Set ℓ

------------------------------------------------------------------------
-- Abstract well-typed substitutions (aka context morphisms)

record TypedSub {t}
                (Type : Pred ℕ t)      -- Type syntax
                (Term : Pred ℕ lzero)  -- Term syntax
                ℓ
                : Set (lsuc (t ⊔ ℓ)) where

  -- The underlying type assignment system

  infix 4 _⊢_∈_ _⊢_wf

  field
    _⊢_wf : Wf Type Type ℓ            -- Type formation judgment
    _⊢_∈_ : Typing Type Term Type ℓ   -- Typing judgment

  -- Weakening and term substitutions in types.

  field
    typeExtension       : Extension Type          -- weakening of types
    typeTermApplication : Application Type Term   -- app. of term subst.
    termSimple          : Simple Term             -- simple term subst.

  open ContextFormation _⊢_wf          using (_wf)
  open Application typeTermApplication using (_/_)

  infix  4 _⊢/_∈_
  infixr 5 _∷_

  -- Typed substitutions.
  --
  -- A typed substitution Δ ⊢/ σ ∈ Γ is a substitution σ which, when
  -- applied to a well-typed term Γ ⊢ t ∈ a in a source context Γ,
  -- yields a well-typed term Δ ⊢ t / σ ∈ a / σ in a well-formed
  -- target context Δ.

  data _⊢/_∈_ {n} (Δ : Ctx Type n) :
              ∀ {m} → Sub Term m n → Ctx Type m → Set (t ⊔ ℓ) where
    []  : Δ wf → Δ ⊢/ [] ∈ []
    _∷_ : ∀ {m t} {a : Type m} {σ : Sub Term m n} {Γ} →
          Δ ⊢ t ∈ a / σ → Δ ⊢/ σ ∈ Γ → Δ ⊢/ t ∷ σ ∈ a ∷ Γ

  -- The domains of well-typed substitutions are well-formed.

  /∈-wf : ∀ {m n Δ} {σ : Sub Term m n} {Γ} → Δ ⊢/ σ ∈ Γ → Δ wf
  /∈-wf ([] Δ-wf) = Δ-wf
  /∈-wf (_ ∷ σ∈Γ) = /∈-wf σ∈Γ

------------------------------------------------------------------------
-- Operations on abstract well-typed substitutions

-- Operations on abstract typed substitutions that require weakening
-- of well-typed terms

record TypedWeakenOps {t ℓ} {Type : Pred ℕ t} {Term : Pred ℕ lzero}
                      (typedSub : TypedSub Type Term ℓ)
                      : Set (lsuc (t ⊔ ℓ)) where

  open TypedSub typedSub

  -- Operations on contexts and raw terms that require weakening

  private
    termExtension : Extension Term
    termExtension = record { weaken = Simple.weaken termSimple }

    module E = Extension termExtension
    module C = WeakenOps typeExtension

  open Simple           termSimple          using (wk)
  open Application      typeTermApplication using (_/_; _⊙_)
  open ContextFormation _⊢_wf               using (_wf; _∷_; wf-∷₁)

  field

    -- Weakening preserves well-typed terms.

    ∈-weaken : ∀ {n} {Δ : Ctx Type n} {t a b} → Δ ⊢ a wf → Δ ⊢ t ∈ b →
               (a ∷ Δ) ⊢ E.weaken t ∈ C.weaken b

    -- Well-typedness implies well-formedness of contexts.

    ∈-wf : ∀ {n} {Δ : Ctx Type n} {t a} → Δ ⊢ t ∈ a → Δ wf

    -- Lemmas relating type weakening to term substitutions

    /-wk : ∀ {n} {a : Type n} → a / wk ≡ C.weaken a

    /-weaken : ∀ {m n} {σ : Sub Term m n} a →
               a / map E.weaken σ ≡ a / σ / wk

    weaken-/-∷ : ∀ {n m} {t} {σ : Sub Term m n} (a : Type m) →
                 C.weaken a / (t ∷ σ) ≡ a / σ

  -- Some helper lemmas

  /-map-weaken : ∀ {m n} a (ρ : Sub Term m n) →
                 C.weaken (a / ρ) ≡ a / map E.weaken ρ
  /-map-weaken a ρ = begin
    C.weaken (a / ρ)    ≡⟨ sym /-wk ⟩
    a / ρ / wk          ≡⟨ sym (/-weaken a) ⟩
    a / map E.weaken ρ  ∎

  map-weaken-⊙-∷ : ∀ {m n} (σ : Sub Type m m) t (ρ : Sub Term m n) →
                   σ ⊙ ρ ≡ map C.weaken σ ⊙ (t ∷ ρ)
  map-weaken-⊙-∷ σ t ρ = sym (begin
    map C.weaken σ ⊙ (t ∷ ρ)          ≡⟨ sym (map-∘ _ C.weaken σ) ⟩
    map ((_/ (t ∷ ρ)) ∘ C.weaken) σ   ≡⟨ map-cong weaken-/-∷ σ ⟩
    map (_/ ρ) σ                      ≡⟨⟩
    σ ⊙ ρ                             ∎)

  -- Weakening preserves well-typed substitutions.

  /∈-weaken : ∀ {m n Δ a} {σ : Sub Term m n} {Γ} →
              Δ ⊢ a wf → Δ ⊢/ σ ∈ Γ →
              (a ∷ Δ) ⊢/ map E.weaken σ ∈ Γ
  /∈-weaken                         a-wf ([] Δ-wf)     = [] (a-wf ∷ Δ-wf)
  /∈-weaken {_} {_} {Δ} {a} {t ∷ σ} a-wf (t∈b/σ ∷ σ∈Γ) =
    subst (a ∷ Δ ⊢ _ ∈_) (/-map-weaken _ σ) (∈-weaken a-wf t∈b/σ) ∷
    (/∈-weaken a-wf σ∈Γ)

  -- A typed substitution consists of pointwise-typed terms.

  toPointwise : ∀ {m n Δ} {σ : Sub Term m n} {Γ} →
                Δ ⊢/ σ ∈ Γ → Pointwise (Δ ⊢_∈_) σ (C.toVec Γ ⊙ σ)
  toPointwise                     ([] Δ-wf)     = []
  toPointwise {_} {_} {Δ} {t ∷ σ} (t∈a/σ ∷ σ∈Γ) =
    subst (Δ ⊢ t ∈_) (sym (weaken-/-∷ _)) t∈a/σ ∷
    subst (Pointwise (_⊢_∈_ Δ) σ) (map-weaken-⊙-∷ _ t σ) (toPointwise σ∈Γ)

  -- Look up an entry in a typed substitution.

  lookup : ∀ {m n Δ} {σ : Sub Term m n} {Γ} →
           Δ ⊢/ σ ∈ Γ → (x : Fin m) → Δ ⊢ Vec.lookup σ x ∈ C.lookup Γ x / σ
  lookup {_} {_} {Δ} {σ} {Γ} σ∈Γ x =
    subst (Δ ⊢ _ ∈_) (lookup-map x _ (C.toVec Γ))
          (PW.lookup (toPointwise σ∈Γ) x)

  -- Extension by a typed term.

  ∈-/∷ : ∀ {m n Δ} {σ : Sub Term m n} {Γ t a b} →
         (b ∷ Δ) ⊢ t ∈ C.weaken (a / σ) → Δ ⊢/ σ ∈ Γ →
         b ∷ Δ ⊢/ t E./∷ σ ∈ a ∷ Γ
  ∈-/∷ t∈a/σ σ∈Γ =
    subst (_⊢_∈_ _ _) (/-map-weaken _ _) t∈a/σ ∷ /∈-weaken b-wf σ∈Γ

    where
    b∷Δ-wf = ∈-wf t∈a/σ
    b-wf   = wf-∷₁ b∷Δ-wf

-- Operations on abstract typed substitutions that require simple term
-- substitutions

record TypedSimple {t ℓ} {Type : Pred ℕ t} {Term : Pred ℕ lzero}
                   (typedSub : TypedSub Type Term ℓ)
                   : Set (lsuc (t ⊔ ℓ)) where

  -- Operations on abstract typed substitutions that require weakening
  -- of terms

  field typedWeakenOps : TypedWeakenOps typedSub

  open TypedWeakenOps   typedWeakenOps public
  open TypedSub         typedSub
  open ContextFormation _⊢_wf using (_wf; _⊢_wfExt; []; _∷_; wf-∷₂)
  open Application      typeTermApplication using (_/_)

  private
    module S = Simple    termSimple
    module C = WeakenOps typeExtension
  open S using (_↑; _↑⋆_; id; wk; sub)

  -- Context operations that require term substitutions in types.

  open SubstOps typeTermApplication termSimple using (_E/_)

  field

    -- Takes variables to well-typed Tms.

    ∈-var : ∀ {n} {Γ : Ctx Type n} →
            ∀ x → Γ wf → Γ ⊢ S.var x ∈ C.lookup Γ x

    -- Well-formedness of types implies well-formedness of contexts.

    wf-wf : ∀ {n} {Γ : Ctx Type n} {a} → Γ ⊢ a wf → Γ wf

    -- The identity substitution is an identity

    id-vanishes : ∀ {n} (a : Type n) → a / id ≡ a

  -- Lifting.

  ∈-↑ : ∀ {m n Δ} {σ : Sub Term m n} {a Γ} →
        Δ ⊢ a / σ wf → Δ ⊢/ σ ∈ Γ → a / σ ∷ Δ ⊢/ σ ↑ ∈ a ∷ Γ
  ∈-↑ a/σ-wf σ∈Γ = ∈-/∷ (∈-var zero (a/σ-wf ∷ (wf-wf a/σ-wf))) σ∈Γ

  ∈-↑⋆ : ∀ {k m n Δ} {E : CtxExt Type m k} {σ : Sub Term m n} {Γ} →
         Δ ⊢ (E E/ σ) wfExt → Δ ⊢/ σ ∈ Γ → (E E/ σ) ++ Δ ⊢/ σ ↑⋆ k ∈ (E ++ Γ)
  ∈-↑⋆ {E = []}            []                        σ∈Γ = σ∈Γ
  ∈-↑⋆ {E = a ∷ E} {Δ} {Γ} (a/σ↑⋆1+k-wf ∷ E/σ-wfExt) σ∈Γ =
    ∈-↑ {Γ = E ++ Γ} a/σ↑⋆1+k-wf (∈-↑⋆ {E = E} E/σ-wfExt σ∈Γ)

  -- The identity substitution.

  ∈-id : ∀ {n} {Γ : Ctx Type n} → Γ wf → Γ ⊢/ id ∈ Γ
  ∈-id []            = [] []
  ∈-id (a-wf ∷ Γ-wf) =
    ∈-/∷ (subst (_ ⊢ S.var zero ∈_) (sym (cong C.weaken (id-vanishes _)))
                (∈-var zero (a-wf ∷ Γ-wf)))
         (∈-id Γ-wf)

  -- Weakening.

  ∈-wk : ∀ {n} {Γ : Ctx Type n} {a} → Γ ⊢ a wf → a ∷ Γ ⊢/ wk ∈ Γ
  ∈-wk a-wf = /∈-weaken a-wf (∈-id (wf-wf a-wf))

  -- A substitution which only replaces the first variable.

  ∈-sub : ∀ {n} {Γ : Ctx Type n} {t a} → Γ ⊢ t ∈ a → Γ ⊢/ sub t ∈ a ∷ Γ
  ∈-sub t∈a =
    (subst (_ ⊢ _ ∈_) (sym (id-vanishes _)) t∈a) ∷ (∈-id (∈-wf t∈a))

  -- A substitution which only changes the type of the first variable.

  ∈-tsub : ∀ {n} {Γ : Ctx Type n} {a b} → b ∷ Γ ⊢ S.var zero ∈ C.weaken a →
           b ∷ Γ ⊢/ id ∈ a ∷ Γ
  ∈-tsub z∈a =
    ∈-/∷ (subst (_ ⊢ _ ∈_) (cong C.weaken (sym (id-vanishes _))) z∈a)
         (∈-id (wf-∷₂ (∈-wf z∈a)))

-- Application of typed substitutions to typed terms.

record TypedApplication {t ℓ} {Type : Pred ℕ t} {Term : Pred ℕ lzero}
                        (typedSub : TypedSub Type Term ℓ)
                        : Set (lsuc (t ⊔ ℓ)) where

  open TypedSub    typedSub
  open Application typeTermApplication using (_/_)

  -- Applications of term substitutions to terms

  field termTermApplication : Application Term Term

  private
    module C = WeakenOps typeExtension
    module A = Application termTermApplication
  open A using (_⊙_)

  field

    -- Post-application of substitutions to things.

    ∈-/ : ∀ {m n Δ} {σ : Sub Term m n} {Γ t a} →
          Γ ⊢ t ∈ a → Δ ⊢/ σ ∈ Γ → Δ ⊢ t A./ σ ∈ a / σ

    -- Application of composed substitutions is repeated application.

    /-⊙ : ∀ {m n k} {σ : Sub Term m n} {ρ : Sub Term n k} a →
          a / σ ⊙ ρ ≡ a / σ / ρ

  -- Reverse composition. (Fits well with post-application.)

  ∈-⊙ : ∀ {m n k Δ Γ E} {σ : Sub Term m n} {ρ : Sub Term n k} →
        Δ ⊢/ σ ∈ Γ → E ⊢/ ρ ∈ Δ → E ⊢/ σ ⊙ ρ ∈ Γ
  ∈-⊙ ([] Δ-wf)     ρ∈Δ = [] (/∈-wf ρ∈Δ)
  ∈-⊙ (t∈a/σ ∷ σ∈Γ) ρ∈Δ =
    (subst (_ ⊢ _ ∈_) (sym (/-⊙ _)) (∈-/ t∈a/σ ρ∈Δ)) ∷ (∈-⊙ σ∈Γ ρ∈Δ)

------------------------------------------------------------------------
-- Instantiations and code for facilitating instantiations

-- Abstract typed liftings from Term₁ to Term₂ terms

record LiftTyped {t ℓ₁ ℓ₂} {Type : Pred ℕ t} {Term₁ Term₂ : Pred ℕ lzero}
                 (typeTermSubst : TermLikeSubst Type Term₂)
                 (_⊢_wf  : Wf Type Type ℓ₁)
                 (_⊢₁_∈_ : Typing Type Term₁ Type ℓ₁)
                 (_⊢₂_∈_ : Typing Type Term₂ Type ℓ₂)
                 : Set (lsuc (t ⊔ ℓ₁ ⊔ ℓ₂)) where

  field rawLift : Lift Term₁ Term₂   -- Lifting between raw terms

  open TermLikeSubst typeTermSubst using (app; weaken; termSubst)
  private module S₂ = TermSubst termSubst

  typedSub : TypedSub Type Term₁ ℓ₁
  typedSub = record
    { _⊢_wf               = _⊢_wf
    ; _⊢_∈_               = _⊢₁_∈_
    ; typeExtension       = record { weaken = weaken }
    ; typeTermApplication = record { _/_    = app rawLift }
    ; termSimple          = Lift.simple rawLift
    }
  open TypedSub typedSub public hiding (_⊢_wf; _⊢_∈_; typeExtension)

  -- Simple typed Term₁ substitutions.

  field typedSimple : TypedSimple typedSub

  open Lift        rawLift             public
  open Application typeTermApplication public
  open TypedSimple typedSimple         public hiding (_⊢_∈_)

  field

    -- Lifts well-typed Term₁-terms to well-typed Term₂-terms.

    ∈-lift : ∀ {n} {Γ : Ctx Type n} {t a} → Γ ⊢₁ t ∈ a → Γ ⊢₂ (lift t) ∈ a

    -- A usefule lemma: lifting preserves variables.

    lift-var : ∀ {n} (x : Fin n) → lift (var x) ≡ S₂.var x

-- Abstract variable typings.

module VarTyping {t ℓ} {Type : Pred ℕ t}
                 (_⊢_wf : Wf Type Type (t ⊔ ℓ))
                 (typeExtension : Extension Type) where

  open ContextFormation _⊢_wf
  open WeakenOps        typeExtension

  infix 4 _⊢Var_∈_

  -- Abstract reflexive variable typings.

  data _⊢Var_∈_ {n} (Γ : Ctx Type n) : Fin n → Type n → Set (t ⊔ ℓ) where
    ∈-var : ∀ x → Γ wf → Γ ⊢Var x ∈ lookup Γ x

  -- Variable typing together with type formation forms
  -- a type assignment system.

-- Abstract typed variable substitutions (renamings).

record TypedVarSubst {t} (Type : Pred ℕ t) ℓ : Set (lsuc (t ⊔ ℓ)) where

  infix 4 _⊢_wf

  field
    _⊢_wf : Wf Type Type (t ⊔ ℓ)     -- Type formation judgment

    -- Generic application of renamings to raw types

    typeExtension      : Extension Type
    typeVarApplication : Application Type Fin

  open VarTyping {t} {t ⊔ ℓ} _⊢_wf typeExtension public

  open WeakenOps        typeExtension      using (weaken; toVec)
  open Application      typeVarApplication using (_/_)
  open ContextFormation _⊢_wf              using (_wf; _∷_)
  open VarSubst                            using (id; wk; _⊙_)

  field

    -- Context validity of type formation.

    wf-wf : ∀ {n} {Γ : Ctx Type n} {a}   → Γ ⊢ a wf  → Γ wf

    -- Lemmas about renamings in types

    /-wk        : ∀ {n} {a : Type n} → a / wk ≡ weaken a
    id-vanishes : ∀ {n} (a : Type n) → a / id ≡ a
    /-⊙         : ∀ {m n k} {ρ₁ : Sub Fin m n} {ρ₂ : Sub Fin n k} a →
                  a / ρ₁ ⊙ ρ₂ ≡ a / ρ₁ / ρ₂

  -- Typed renamings and associated lemmas.

  typedRenaming : TypedSub Type Fin (t ⊔ ℓ)
  typedRenaming = record
    { _⊢_wf               = _⊢_wf
    ; _⊢_∈_               = _⊢Var_∈_
    ; typeExtension       = typeExtension
    ; typeTermApplication = typeVarApplication
    ; termSimple          = VarSubst.simple
    }

  appLemmas : AppLemmas Type Fin
  appLemmas = record
    { application = typeVarApplication
    ; lemmas₄     = VarLemmas.lemmas₄
    ; id-vanishes = id-vanishes
    ; /-⊙         = /-⊙
    }

  weakenLemmas : WeakenLemmas Type Fin
  weakenLemmas = record
    { appLemmas = appLemmas
    ; /-wk      = /-wk
    }

  open AppLemmas    appLemmas    using (/-weaken)
  open WeakenLemmas weakenLemmas using (weaken-/-∷)

  -- Simple typed renamings.

  typedSimple : TypedSimple typedRenaming
  typedSimple = record
    { typedWeakenOps = record
      { ∈-weaken     = ∈-weaken
      ; ∈-wf         = ∈-wf
      ; /-wk         = /-wk
      ; /-weaken     = /-weaken
      ; weaken-/-∷   = weaken-/-∷
      }
    ; ∈-var          = ∈-var
    ; wf-wf          = wf-wf
    ; id-vanishes    = id-vanishes
    }
    where

    ∈-weaken : ∀ {n} {Γ : Ctx Type n} {x a b} →
               Γ ⊢ a wf → Γ ⊢Var x ∈ b →
               a ∷ Γ ⊢Var suc x ∈ weaken b
    ∈-weaken {_} {Γ} a-wf (∈-var x Γ-wf) =
      subst (_ ∷ Γ ⊢Var _ ∈_) (lookup-map x weaken (toVec Γ))
            (∈-var (suc x) (a-wf ∷ Γ-wf))

    ∈-wf : ∀ {n} {Γ : Ctx Type n} {x a} → Γ ⊢Var x ∈ a → Γ wf
    ∈-wf (∈-var x Γ-wf) = Γ-wf

  open TypedSub typedRenaming public
    renaming (_⊢/_∈_ to _⊢/Var_∈_) hiding (_⊢_wf; _/_)
  open TypedSimple typedSimple public
    hiding (typeExtension; _/_; _⊢_∈_; ∈-var; _⊢_wf; wf-wf; /-wk; id-vanishes)

  -- Applications of typed renamings to typed variables

  typedApplication : TypedApplication typedRenaming
  typedApplication = record
    { termTermApplication = VarSubst.application
    ; ∈-/ = ∈-/
    ; /-⊙ = /-⊙
    }
    where

    ∈-/ : ∀ {m n Δ} {ρ : Sub Fin m n} {Γ x a} →
          Γ ⊢Var x ∈ a → Δ ⊢/Var ρ ∈ Γ → Δ ⊢Var Vec.lookup ρ x ∈ a / ρ
    ∈-/ (∈-var x Γ-wf) ρ∈Γ = lookup ρ∈Γ x

  open TypedApplication typedApplication public
    using (_/_; ∈-/; ∈-⊙)

-- Abstract typed term substitutions.

record TypedTermSubst {t h} (Type : Pred ℕ t) (Term : Pred ℕ lzero) ℓ
                      (Helpers : ∀ {T} → Lift T Term → Set h)
                      : Set (lsuc (t ⊔ ℓ) ⊔ h) where

  infix 4 _⊢_∈_ _⊢_wf

  field
    _⊢_wf : Wf Type Type (t ⊔ ℓ)            -- Type formation judgment
    _⊢_∈_ : Typing Type Term Type (t ⊔ ℓ)   -- Typing judgment

    -- Lemmas about term substitutions in Types

    termLikeLemmas : TermLikeLemmas Type Term

  private
    module Tp = TermLikeLemmas termLikeLemmas
    module Tm = TermLemmas Tp.termLemmas
    module S  = TermSubst Tm.termSubst

  typeExtension : Extension Type
  typeExtension = record { weaken = Tp.weaken }

  private module C = WeakenOps typeExtension

  typedSub : TypedSub Type Term (t ⊔ ℓ)
  typedSub = record
    { _⊢_wf               = _⊢_wf
    ; _⊢_∈_               = _⊢_∈_
    ; typeExtension       = typeExtension
    ; termSimple          = S.simple
    ; typeTermApplication = Tp.termApplication
    }

  open ContextFormation _⊢_wf using (_wf)

  field

    -- Custom helper lemmas used to implement application of typed
    -- substitutions

    varHelpers  : Helpers S.varLift   -- lemmas about renamings
    termHelpers : Helpers S.termLift  -- lemmas about substitutions

    -- Context validity of type formation and typing.

    wf-wf : ∀ {n} {Γ : Ctx Type n} {a}   → Γ ⊢ a wf  → Γ wf
    ∈-wf  : ∀ {n} {Γ : Ctx Type n} {t a} → Γ ⊢ t ∈ a → Γ wf

    -- Takes variables to well-typed Tms.

    ∈-var : ∀ {n} {Γ : Ctx Type n} →
            ∀ x → Γ wf → Γ ⊢ S.var x ∈ C.lookup Γ x

    -- Generic application of typed Term′ substitutions to typed Terms.

    typedApp : ∀ {Term′ : Pred ℕ lzero}
               (_⊢′_∈_ : Typing Type Term′ Type (t ⊔ ℓ))
               (liftTyped : LiftTyped Tp.termLikeSubst _⊢_wf _⊢′_∈_ _⊢_∈_) →
               let open LiftTyped liftTyped using (rawLift; _⊢/_∈_; _/_)
               in (helpers : Helpers rawLift) →
                  ∀ {m n Γ Δ t a} {σ : Sub Term′ m n} →
                  Γ ⊢ t ∈ a → Δ ⊢/ σ ∈ Γ → Δ ⊢ S.app rawLift t σ ∈ a / σ

  typedVarSubst : TypedVarSubst Type (t ⊔ ℓ)
  typedVarSubst = record
    { _⊢_wf              = _⊢_wf
    ; typeVarApplication = Tp.varApplication
    ; typeExtension      = typeExtension
    ; wf-wf              = wf-wf
    ; /-wk               = refl
    ; id-vanishes        = id-vanishes
    ; /-⊙                = /-⊙
    }
    where
    open LiftSubLemmas Tp.varLiftSubLemmas using (liftAppLemmas)
    open LiftAppLemmas liftAppLemmas       using (id-vanishes; /-⊙)

  open TypedVarSubst typedVarSubst public
    using (_⊢Var_∈_; _⊢/Var_∈_; typedRenaming)
    renaming
    ( typedSimple    to varTypedSimple
    ; ∈-var          to Var∈-var
    ; ∈-↑            to Var∈-↑
    ; ∈-id           to Var∈-id
    ; ∈-wk           to Var∈-wk
    ; ∈-sub          to Var∈-sub
    ; ∈-tsub         to Var∈-tsub
    )

  varLiftTyped : LiftTyped Tp.termLikeSubst _⊢_wf _⊢Var_∈_ _⊢_∈_
  varLiftTyped = record
    { rawLift     = S.varLift
    ; typedSimple = varTypedSimple
    ; ∈-lift      = ∈-lift
    ; lift-var    = λ _ → refl
    }
    where

    ∈-lift : ∀ {n Γ x} {a : Type n} → Γ ⊢Var x ∈ a → Γ ⊢ S.var x ∈ a
    ∈-lift (Var∈-var x Γ-wf) = ∈-var x Γ-wf

  ∈-/Var : ∀ {m n} {Γ t a} {ρ : Sub Fin m n} {Δ} →
           Δ ⊢ t ∈ a → Γ ⊢/Var ρ ∈ Δ → Γ ⊢ t S./Var ρ ∈ a Tp./Var ρ
  ∈-/Var = typedApp _⊢Var_∈_ varLiftTyped varHelpers

  -- Operations on well-formed contexts that require weakening of
  -- well-formedness judgments.

  -- Simple typed substitutions.

  typedSimple : TypedSimple typedSub
  typedSimple = record
    { typedWeakenOps = record
      { ∈-weaken     = λ a-wf t∈b → ∈-/Var t∈b (Var∈-wk a-wf)
      ; ∈-wf         = ∈-wf
      ; /-wk         = Tp./-wk
      ; /-weaken     = Tp./-weaken
      ; weaken-/-∷   = Tp.weaken-/-∷
      }
    ; ∈-var          = ∈-var
    ; wf-wf          = wf-wf
    ; id-vanishes    = Tp.id-vanishes
    }

  termLiftTyped : LiftTyped Tp.termLikeSubst _⊢_wf _⊢_∈_ _⊢_∈_
  termLiftTyped = record
    { rawLift     = S.termLift
    ; typedSimple = typedSimple
    ; ∈-lift      = Fun.id
    ; lift-var    = λ _ → refl
    }

  -- Applications of typed term substitutions to typed terms

  typedApplication : TypedApplication typedSub
  typedApplication = record
    { termTermApplication = S.application
    ; ∈-/ = typedApp _⊢_∈_ termLiftTyped termHelpers
    ; /-⊙ = Tp./-⊙
    }

  open TypedSub typedSub public hiding (typeExtension)
  open TypedSimple typedSimple public hiding
    ( typeExtension; ∈-weaken; ∈-wf; ∈-var; wf-wf
    ; /-wk; /-weaken; weaken-/-∷; id-vanishes
    )
  open TypedApplication typedApplication public hiding (/-⊙)

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text:
-- {-# OPTIONS --verbose tc.records.ifs:15 #-}
-- {-# OPTIONS --verbose tc.constr.findInScope:15 #-}
-- {-# OPTIONS --verbose tc.term.args.ifs:15 #-}
-- {-# OPTIONS --verbose cta.record.ifs:15 #-}
-- {-# OPTIONS --verbose tc.section.apply:25 #-}
-- {-# OPTIONS --verbose tc.mod.apply:100 #-}
-- {-# OPTIONS --verbose scope.rec:15 #-}
-- {-# OPTIONS --verbose tc.rec.def:15 #-}

module 07-subclasses where

module Imports where
  module L where
    open import Agda.Primitive public
      using (Level; _⊔_) renaming (lzero to zero; lsuc to suc)

  -- extract from Function
  id : ∀ {a} {A : Set a} → A → A
  id x = x

  _$_ : ∀ {a b} {A : Set a} {B : A → Set b} →
        ((x : A) → B x) → ((x : A) → B x)
  f $ x = f x

  _∘_ : ∀ {a b c}
          {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
        (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
        ((x : A) → C (g x))
  f ∘ g = λ x → f (g x)

  -- extract from Data.Bool
  infixr 5 _∨_
  data Bool : Set where
    true  : Bool
    false : Bool

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

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

  -- extract from Relation.Nullary.Decidable and friends
  infix 3 ¬_

  data ⊥ : Set where

  ¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
  ¬ P = P → ⊥

  data Dec {p} (P : Set p) : Set p where
    yes : ( p :   P) → Dec P
    no  : (¬p : ¬ P) → Dec P
  ⌊_⌋ : ∀ {p} {P : Set p} → Dec P → Bool
  ⌊ yes _ ⌋ = true
  ⌊ no  _ ⌋ = false

  -- extract from Relation.Binary.PropositionalEquality
  data _≡_ {a} {A : Set a} (x : A) : A → Set a where
    refl : x ≡ x

  cong : ∀ {a b} {A : Set a} {B : Set b}
         (f : A → B) {x y} → x ≡ y → f x ≡ f y
  cong f refl = refl

  -- extract from Data.Nat
  data ℕ : Set where
    zero : ℕ
    suc  : (n : ℕ) → ℕ

  {-# BUILTIN NATURAL ℕ    #-}

  pred : ℕ → ℕ
  pred zero    = zero
  pred (suc n) = n

  _≟_ : (x y : ℕ) → Dec (x ≡ y)
  zero  ≟ zero   = yes refl
  suc m ≟ suc n  with m ≟ n
  suc m ≟ suc .m | yes refl = yes refl
  suc m ≟ suc n  | no prf   = no (prf ∘ cong pred)
  zero  ≟ suc n  = no λ()
  suc m ≟ zero   = no λ()

open Imports

-- Begin of actual example!

record Eq (A : Set) : Set where
  field eq : A → A → Bool

primEqBool : Bool → Bool → Bool
primEqBool true = id
primEqBool false = not

eqBool : Eq Bool
eqBool = record { eq = primEqBool }

primEqNat : ℕ → ℕ → Bool
primEqNat a b = ⌊ a ≟ b ⌋

primLtNat : ℕ → ℕ → Bool
primLtNat 0 _ = true
primLtNat (suc a) (suc b) = primLtNat a b
primLtNat _ _ = false

neq : {t : Set} → {{eqT : Eq t}} → t → t → Bool
neq a b = not $ eq a b
  where open Eq {{...}}

record Ord₁ (A : Set) : Set where
  field _<_ : A → A → Bool
        eqA : Eq A

ord₁Nat : Ord₁ ℕ
ord₁Nat = record { _<_ = primLtNat; eqA = eqNat }
  where eqNat : Eq ℕ
        eqNat = record { eq = primEqNat }

record Ord₂ {A : Set} (eqA : Eq A) : Set where
  field _<_ : A → A → Bool

ord₂Nat : Ord₂ (record { eq = primEqNat })
ord₂Nat = record { _<_ = primLtNat }

record Ord₃ (A : Set) : Set where
  field _<_ : A → A → Bool
        eqA : Eq A
  open Eq eqA public

ord₃Nat : Ord₃ ℕ
ord₃Nat = record { _<_ = primLtNat; eqA = eqNat }
  where eqNat : Eq ℕ
        eqNat = record { eq = primEqNat }

record Ord₄ {A : Set} (eqA : Eq A) : Set where
  field _<_ : A → A → Bool
  open Eq eqA public

ord₄Nat : Ord₄ (record { eq = primEqNat })
ord₄Nat = record { _<_ = primLtNat }

module test₁ where
  open Ord₁ {{...}}
  open Eq {{...}}

  eqNat : Eq _
  eqNat = eqA

  test₁ = 5 < 3
  test₂ = eq 5 3
  test₃ = eq true false
  test₄ : {A : Set} → {{ ordA : Ord₁ A }} → A → A → Bool
  test₄ a b = a < b ∨ eq a b
    where
      eqA' : Eq _
      eqA' = eqA

module test₂ where
  open Ord₂ {{...}}
  open Eq {{...}}

  eqNat : Eq ℕ
  eqNat = record { eq = primEqNat }

  test₁ = 5 < 3
  test₂ = eq 5 3
  test₃ = eq true false
  test₄ : {A : Set} → {eqA : Eq A} → {{ ordA : Ord₂ eqA }} → A → A → Bool
  test₄ {eqA = _} a b = a < b ∨ eq a b

module test₃ where
  open Ord₃ {{...}}
  open Eq {{...}} renaming (eq to eq')

  test₁ = 5 < 3
  test₂ = eq 5 3
  test₃ = eq' true false
  test₄ : {A : Set} → {{ ordA : Ord₃ A }} → A → A → Bool
  test₄ a b = a < b ∨ eq a b

module test₄ where
  open Ord₄ {{...}}
  open Eq {{...}} renaming (eq to eq')

  test₁ = 5 < 3
  test₂ = eq 5 3
  test₃ = eq' true false
  test₄ : {A : Set} → {eqA : Eq A} → {{ ordA : Ord₄ eqA }} → A → A → Bool
  test₄ a b = a < b ∨ eq a b

module test₄′ where
  open Ord₄ {{...}} hiding (eq)
  open Eq {{...}}

  eqNat : Eq ℕ
  eqNat = record { eq = primEqNat }

  test₁ = 5 < 3
  test₂ = eq 5 3
  test₃ = eq true false
  test₄ : {A : Set} → {eqA : Eq A} → {{ ordA : Ord₄ eqA }} → A → A → Bool
  test₄ {eqA = _} a b = a < b ∨ eq a b

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Field.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.SIP
open import Cubical.Relation.Nullary

open import Cubical.Data.Sigma
open import Cubical.Data.Unit
open import Cubical.Data.Empty

open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Ring
  hiding (_$_)
open import Cubical.Algebra.CommRing

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open import Cubical.Reflection.RecordEquiv

open Iso

private
  variable
    ℓ ℓ' : Level

record IsField {R : Type ℓ}
                  (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R) : Type ℓ where

  constructor isfield

  field
    isCommRing : IsCommRing 0r 1r _+_ _·_ -_
    hasInverse : (x : R) → ¬ x ≡ 0r → Σ[ y ∈ R ] x · y ≡ 1r
    0≢1        : ¬ 0r ≡ 1r

  open IsCommRing isCommRing public

  _[_]⁻¹ : (x : R) → ¬ x ≡ 0r → R
  x [ ¬x≡0 ]⁻¹ = hasInverse x ¬x≡0 .fst

  ·⁻¹≡1 : (x : R) (≢0 : ¬ x ≡ 0r) → x · (x [ ≢0 ]⁻¹) ≡ 1r
  ·⁻¹≡1 x ¬x≡0 = hasInverse x ¬x≡0 .snd

record FieldStr (A : Type ℓ) : Type (ℓ-suc ℓ) where

  constructor fieldstr

  field
    0r         : A
    1r         : A
    _+_        : A → A → A
    _·_        : A → A → A
    -_         : A → A
    isField    : IsField 0r 1r _+_ _·_ -_

  infix  8 -_
  infixl 7 _·_
  infixl 6 _+_

  open IsField isField public

Field : ∀ ℓ → Type (ℓ-suc ℓ)
Field ℓ = TypeWithStr ℓ FieldStr

isSetField : (R : Field ℓ) → isSet ⟨ R ⟩
isSetField R = R .snd .FieldStr.isField .IsField.·IsMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set

makeIsField : {R : Type ℓ} {0r 1r : R} {_+_ _·_ : R → R → R} { -_ : R → R}
                 {_[_]⁻¹ : (x : R) → ¬ (x ≡ 0r) → R}
                 (is-setR : isSet R)
                 (+-assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
                 (+-rid : (x : R) → x + 0r ≡ x)
                 (+-rinv : (x : R) → x + (- x) ≡ 0r)
                 (+-comm : (x y : R) → x + y ≡ y + x)
                 (·-assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
                 (·-rid : (x : R) → x · 1r ≡ x)
                 (·-rdist-+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
                 (·-comm : (x y : R) → x · y ≡ y · x)
                 (·⁻¹≡1 : (x : R) (≢0 : ¬ (x ≡ 0r)) → x · (x [ ≢0 ]⁻¹) ≡ 1r)
                 (0≢1 : ¬ (0r ≡ 1r))
               → IsField 0r 1r _+_ _·_ -_
makeIsField {R = R} {0r = 0r} {1r = 1r} {_+_ = _+_} {_·_ = _·_} {_[_]⁻¹ = _[_]⁻¹}
  is-setR +-assoc +-rid +-rinv +-comm ·-assoc ·-rid ·-rdist-+ ·-comm ·⁻¹≡1 0≢1 =
  isfield (makeIsCommRing is-setR +-assoc +-rid +-rinv +-comm ·-assoc ·-rid ·-rdist-+ ·-comm) ·-inv 0≢1
    where
    ·-inv : (x : R) → ¬ x ≡ 0r → Σ[ y ∈ R ] x · y ≡ 1r
    ·-inv x ¬x≡0 = x [ ¬x≡0 ]⁻¹ , ·⁻¹≡1 x ¬x≡0

makeField : {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R) (_[_]⁻¹ : (x : R) → ¬ (x ≡ 0r) → R)
                 (is-setR : isSet R)
                 (+-assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
                 (+-rid : (x : R) → x + 0r ≡ x)
                 (+-rinv : (x : R) → x + (- x) ≡ 0r)
                 (+-comm : (x y : R) → x + y ≡ y + x)
                 (·-assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
                 (·-rid : (x : R) → x · 1r ≡ x)
                 (·-rdist-+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
                 (·-comm : (x y : R) → x · y ≡ y · x)
                 (·⁻¹≡1 : (x : R) (≢0 : ¬ (x ≡ 0r)) → x · (x [ ≢0 ]⁻¹) ≡ 1r)
                 (0≢1 : ¬ (0r ≡ 1r))
               → Field ℓ
makeField 0r 1r _+_ _·_ -_ _[_]⁻¹ is-setR +-assoc +-rid +-rinv +-comm ·-assoc ·-rid ·-rdist-+ ·-comm ·⁻¹≡1 0≢1 =
  _ , fieldstr _ _ _ _ _ (makeIsField is-setR +-assoc +-rid +-rinv +-comm ·-assoc ·-rid ·-rdist-+ ·-comm ·⁻¹≡1 0≢1)

module _ (R : CommRing ℓ) where

  open CommRingStr (R .snd)

  makeFieldFromCommRing :
    (hasInv : (x : R .fst) → ¬ x ≡ 0r → Σ[ y ∈ R .fst ] x · y ≡ 1r)
    (0≢1 : ¬ 0r ≡ 1r)
    → Field ℓ
  makeFieldFromCommRing hasInv 0≢1 .fst = R .fst
  makeFieldFromCommRing hasInv 0≢1 .snd = fieldstr _ _ _ _ _ (isfield isCommRing hasInv 0≢1)

FieldStr→CommRingStr : {A : Type ℓ} → FieldStr A → CommRingStr A
FieldStr→CommRingStr (fieldstr _ _ _ _ _ H) = commringstr _ _ _ _ _ (IsField.isCommRing H)

Field→CommRing : Field ℓ → CommRing ℓ
Field→CommRing (_ , fieldstr _ _ _ _ _ H) = _ , commringstr _ _ _ _ _ (IsField.isCommRing H)

record IsFieldHom {A : Type ℓ} {B : Type ℓ'} (R : FieldStr A) (f : A → B) (S : FieldStr B)
  : Type (ℓ-max ℓ ℓ')
  where

  -- Shorter qualified names
  private
    module R = FieldStr R
    module S = FieldStr S

  field
    pres0  : f R.0r ≡ S.0r
    pres1  : f R.1r ≡ S.1r
    pres+  : (x y : A) → f (x R.+ y) ≡ f x S.+ f y
    pres·  : (x y : A) → f (x R.· y) ≡ f x S.· f y
    pres-  : (x : A) → f (R.- x) ≡ S.- (f x)

unquoteDecl IsFieldHomIsoΣ = declareRecordIsoΣ IsFieldHomIsoΣ (quote IsFieldHom)

FieldHom : (R : Field ℓ) (S : Field ℓ') → Type (ℓ-max ℓ ℓ')
FieldHom R S = Σ[ f ∈ (⟨ R ⟩ → ⟨ S ⟩) ] IsFieldHom (R .snd) f (S .snd)

IsFieldEquiv : {A : Type ℓ} {B : Type ℓ'}
  (R : FieldStr A) (e : A ≃ B) (S : FieldStr B) → Type (ℓ-max ℓ ℓ')
IsFieldEquiv R e S = IsFieldHom R (e .fst) S

FieldEquiv : (R : Field ℓ) (S : Field ℓ') → Type (ℓ-max ℓ ℓ')
FieldEquiv R S = Σ[ e ∈ (R .fst ≃ S .fst) ] IsFieldEquiv (R .snd) e (S .snd)

_$_ : {R S : Field ℓ} → (φ : FieldHom R S) → (x : ⟨ R ⟩) → ⟨ S ⟩
φ $ x = φ .fst x

FieldEquiv→FieldHom : {A B : Field ℓ} → FieldEquiv A B → FieldHom A B
FieldEquiv→FieldHom (e , eIsHom) = e .fst , eIsHom

isPropIsField : {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R)
             → isProp (IsField 0r 1r _+_ _·_ -_)
isPropIsField {R = R} 0r 1r _+_ _·_ -_ H@(isfield RR RC RD) (isfield SR SC SD) =
  λ i → isfield (isPropIsCommRing _ _ _ _ _ RR SR i)
                   (isPropInv RC SC i) (isProp¬ _ RD SD i)
  where
  isSetR : isSet _
  isSetR =  RR .IsCommRing.·IsMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set

  isPropInv : isProp ((x : _) → ¬ x ≡ 0r → Σ[ y ∈ R ] x · y ≡ 1r)
  isPropInv = isPropΠ2 (λ x _ → Units.inverseUniqueness (Field→CommRing (_ , fieldstr _ _ _ _ _ H)) x)

𝒮ᴰ-Field : DUARel (𝒮-Univ ℓ) FieldStr ℓ
𝒮ᴰ-Field =
  𝒮ᴰ-Record (𝒮-Univ _) IsFieldEquiv
    (fields:
      data[ 0r ∣ null ∣ pres0 ]
      data[ 1r ∣ null ∣ pres1 ]
      data[ _+_ ∣ bin ∣ pres+ ]
      data[ _·_ ∣ bin ∣ pres· ]
      data[ -_ ∣ autoDUARel _ _ ∣ pres- ]
      prop[ isField ∣ (λ _ _ → isPropIsField _ _ _ _ _) ])
  where
  open FieldStr
  open IsFieldHom

  -- faster with some sharing
  null = autoDUARel (𝒮-Univ _) (λ A → A)
  bin = autoDUARel (𝒮-Univ _) (λ A → A → A → A)

FieldPath : (R S : Field ℓ) → FieldEquiv R S ≃ (R ≡ S)
FieldPath = ∫ 𝒮ᴰ-Field .UARel.ua

uaField : {A B : Field ℓ} → FieldEquiv A B → A ≡ B
uaField {A = A} {B = B} = equivFun (FieldPath A B)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

open import Agda.Builtin.Bool
open import Data.Maybe.Base using (Maybe; just; nothing)
open import Relation.Nullary
open import Data.Rational.Unnormalised.Base using (ℚᵘ; 0ℚᵘ; _≃_)
open import Data.Rational.Unnormalised.Properties using (+-*-commutativeRing; _≃?_)

isZero? : ∀ (p : ℚᵘ) -> Maybe (0ℚᵘ ≃ p)
isZero? p with 0ℚᵘ ≃? p
... | .true because ofʸ p₁ = just p₁
... | .false because ofⁿ ¬p = nothing

open import Tactic.RingSolver.Core.AlmostCommutativeRing using (fromCommutativeRing)
open import Tactic.RingSolver.NonReflective (fromCommutativeRing +-*-commutativeRing isZero?) public

max_stars_repo_name: z-murray/AnalysisAgda

max_issues_repo_name: z-murray/AnalysisAgda

max_forks_repo_name: z-murray/AnalysisAgda