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

open import LogicalFormulae
open import Groups.Definition
open import Setoids.Setoids
open import Functions.Definition
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Lists.Lists

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

open Ring R
open Group additiveGroup
open import Groups.Polynomials.Definition additiveGroup
open import Groups.Polynomials.Group additiveGroup
open Setoid S
open Equivalence eq

_*P_ : NaivePoly → NaivePoly → NaivePoly
[] *P b = []
(x :: a) *P [] = []
(x :: a) *P (y :: b) = (x * y) :: (((map (x *_) b) +P (map (y *_) a)) +P (0R :: (a *P b)))

abstract
  +PCommutative : {x y : NaivePoly} → polysEqual (x +P y) (y +P x)
  +PCommutative {x} {y} = comm (record { commutative = groupIsAbelian }) {x} {y}

  p*Commutative : {a b : NaivePoly} → polysEqual (a *P b) (b *P a)
  p*Commutative {[]} {[]} = record {}
  p*Commutative {[]} {x :: b} = record {}
  p*Commutative {x :: a} {[]} = record {}
  p*Commutative {x :: xs} {y :: ys} = *Commutative ,, +PwellDefined (+PCommutative {map (_*_ x) ys} {map (_*_ y) xs}) (reflexive ,, p*Commutative {xs} {ys})

  zeroTimes1 : {a : NaivePoly} (c : A) → (c ∼ 0G) → polysEqual (map (_*_ c) a) []
  zeroTimes1 {[]} c c=0 = record {}
  zeroTimes1 {x :: a} c c=0 = transitive (transitive *Commutative (*WellDefined reflexive c=0)) (timesZero {x}) ,, zeroTimes1 {a} c c=0

  zeroTimes2 : {a : NaivePoly} (c : A) → polysEqual a [] → polysEqual (map (_*_ c) a) []
  zeroTimes2 {[]} c a=0 = record {}
  zeroTimes2 {x :: a} c (fst ,, snd) = transitive (*WellDefined reflexive fst) (timesZero {c}) ,, zeroTimes2 {a} c snd

  mapWellDefined : (a c : A) (bs : NaivePoly) → (a ∼ c) → polysEqual (map (_*_ a) bs) (map (_*_ c) bs)
  mapWellDefined a c [] a=c = record {}
  mapWellDefined a c (x :: bs) a=c = *WellDefined a=c reflexive ,, mapWellDefined a c bs a=c

  mapWellDefined' : (a : A) (bs cs : NaivePoly) → polysEqual bs cs → polysEqual (map (_*_ a) bs) (map (_*_ a) cs)
  mapWellDefined' a [] [] bs=cs = record {}
  mapWellDefined' a [] (x :: cs) (fst ,, snd) = transitive (*WellDefined reflexive fst) (timesZero {a}) ,, Equivalence.symmetric (Setoid.eq naivePolySetoid) (zeroTimes2 {cs} a (Equivalence.symmetric (Setoid.eq naivePolySetoid) snd))
  mapWellDefined' a (x :: bs) [] (fst ,, snd) = transitive (*WellDefined reflexive fst) (timesZero {a}) ,, zeroTimes2 {bs} a snd
  mapWellDefined' a (b :: bs) (c :: cs) (fst ,, snd) = *WellDefined reflexive fst ,, mapWellDefined' a bs cs snd

  *PwellDefinedL : {a b c : NaivePoly} → polysEqual a c → polysEqual (a *P b) (c *P b)
  *PwellDefinedL {[]} {[]} {[]} a=c = record {}
  *PwellDefinedL {[]} {[]} {x :: c} a=c = record {}
  *PwellDefinedL {[]} {x :: b} {[]} a=c = record {}
  *PwellDefinedL {[]} {b :: bs} {c :: cs} (fst ,, snd) = transitive (transitive *Commutative (*WellDefined reflexive fst)) (timesZero {b}) ,, Equivalence.transitive (Setoid.eq naivePolySetoid) (Equivalence.transitive (Setoid.eq naivePolySetoid) {_} {(map (_*_ c) bs) +P (0G :: (cs *P bs))} (Equivalence.transitive (Setoid.eq naivePolySetoid) {_} {[] +P (0G :: (cs *P bs))} (reflexive ,, ans) (+PwellDefined (Equivalence.symmetric (Setoid.eq naivePolySetoid) (zeroTimes1 {bs} c fst)) (Equivalence.reflexive (Setoid.eq naivePolySetoid) {0G :: (cs *P bs)}))) (+PwellDefined (Equivalence.symmetric (Setoid.eq naivePolySetoid) (Group.identRight polyGroup {map (_*_ c) bs})) (Equivalence.reflexive (Setoid.eq naivePolySetoid) {0G :: (cs *P bs)}))) (+PwellDefined {(map (_*_ c) bs +P [])} {0G :: (cs *P bs)} {(map (_*_ c) bs) +P map (_*_ b) cs} (+PwellDefined (Equivalence.reflexive (Setoid.eq naivePolySetoid) {map (_*_ c) bs}) (Equivalence.symmetric (Setoid.eq naivePolySetoid) (zeroTimes2 {cs} b (Equivalence.symmetric (Setoid.eq naivePolySetoid) snd)))) (Equivalence.reflexive (Setoid.eq naivePolySetoid) {0G :: (cs *P bs)}))
    where
      ans : polysEqual [] (map id (cs *P bs))
      ans rewrite mapId (cs *P bs) = *PwellDefinedL snd
  *PwellDefinedL {a :: as} {[]} {[]} a=c = record {}
  *PwellDefinedL {a :: as} {[]} {x :: c} a=c = record {}
  *PwellDefinedL {a :: as} {b :: bs} {[]} (fst ,, snd) = transitive (transitive *Commutative (*WellDefined reflexive fst)) (timesZero {b}) ,, Equivalence.transitive (Setoid.eq naivePolySetoid) (+PwellDefined {(map (_*_ a) bs +P map (_*_ b) as)} {0G :: (as *P bs)} {[] +P []} {[]} (+PwellDefined {map (_*_ a) bs} {map (_*_ b) as} {[]} {[]} (zeroTimes1 {bs} a fst) (zeroTimes2 {as} b snd)) (reflexive ,, *PwellDefinedL {as} {bs} {[]} snd)) (record {})
  *PwellDefinedL {a :: as} {b :: bs} {c :: cs} (fst ,, snd) = *WellDefined fst reflexive ,, +PwellDefined {(map (_*_ a) bs) +P (map (_*_ b) as)} {0G :: (as *P bs)} {map (_*_ c) bs +P map (_*_ b) cs} {0G :: (cs *P bs)} (+PwellDefined {map (_*_ a) bs} {map (_*_ b) as} {map (_*_ c) bs} {map (_*_ b) cs} (mapWellDefined a c bs fst) (mapWellDefined' b as cs snd)) (reflexive ,, *PwellDefinedL {as} {bs} {cs} snd)

  *PwellDefinedR : {a b c : NaivePoly} → polysEqual b c → polysEqual (a *P b) (a *P c)
  *PwellDefinedR {a} {b} {c} b=c = Equivalence.transitive (Setoid.eq naivePolySetoid) (p*Commutative {a} {b}) (Equivalence.transitive (Setoid.eq naivePolySetoid) (*PwellDefinedL b=c) (p*Commutative {c} {a}))

  *PwellDefined : {a b c d : NaivePoly} → polysEqual a c → polysEqual b d → polysEqual (a *P b) (c *P d)
  *PwellDefined {a}{b}{c}{d} a=c b=d = Equivalence.transitive (Setoid.eq naivePolySetoid) (*PwellDefinedL a=c) (*PwellDefinedR b=d)

  private
    *1 : (a : NaivePoly) → polysEqual (map (_*_ 1R) a) a
    *1 [] = record {}
    *1 (x :: a) = Ring.identIsIdent R ,, *1 a

  *Pident : {a : NaivePoly} → polysEqual ((1R :: []) *P a) a
  *Pident {[]} = record {}
  *Pident {x :: a} = Ring.identIsIdent R ,, Equivalence.transitive (Setoid.eq naivePolySetoid) (+PwellDefined {map (_*_ 1R) a +P []} {0G :: []} {map (_*_ 1R) a} {[]} (Group.identRight polyGroup) (reflexive ,, record {})) (Equivalence.transitive (Setoid.eq naivePolySetoid) (Group.identRight polyGroup {map (_*_ 1R) a}) (*1 a))

  private
    mapMap' : (f g : A → A) (xs : NaivePoly) → map f (map g xs) ≡ map (λ x → f (g x)) xs
    mapMap' f g [] = refl
    mapMap' f g (x :: xs) rewrite mapMap' f g xs = refl

    mapMap'' : (f g : A → A) (xs : NaivePoly) → Setoid._∼_ naivePolySetoid (map f (map g xs)) (map (λ x → f (g x)) xs)
    mapMap'' f g xs rewrite mapMap' f g xs = Equivalence.reflexive (Setoid.eq naivePolySetoid)

    mapWd : (f g : A → A) (xs : NaivePoly) → ((x : A) → (f x) ∼ (g x)) → polysEqual (map f xs) (map g xs)
    mapWd f g [] ext = record {}
    mapWd f g (x :: xs) ext = ext x ,, mapWd f g xs ext

    mapDist' : (b c : A) → (as : NaivePoly) → polysEqual (map (_*_ (b + c)) as) (map (_*_ c) as +P map (_*_ b) as)
    mapDist' b c [] = record {}
    mapDist' b c (x :: as) = transitive (Ring.*DistributesOver+' R {b} {c} {x}) groupIsAbelian ,, mapDist' b c as

    mapTimes : (a b : NaivePoly) (c : A) → polysEqual (a *P (map (_*_ c) b)) (map (_*_ c) (a *P b))
    mapTimes [] b c = record {}
    mapTimes (a :: as) [] c = record {}
    mapTimes (a :: as) (x :: b) c = transitive *Associative (transitive (*WellDefined *Commutative reflexive) (symmetric *Associative)) ,, trans (+PwellDefined {(map (_*_ a) (map (_*_ c) b)) +P map (_*_ (c * x)) as} {0G :: (as *P map (_*_ c) b)} {map (_*_ c) (map (_*_ a) b +P map (_*_ x) as)} (trans (+PwellDefined {map (_*_ a) (map (_*_ c) b)} {map (_*_ (c * x)) as} {map (_*_ c) (map (_*_ a) b)} (trans (mapMap'' (_*_ a) (_*_ c) b) (trans (mapWd (λ x → a * (c * x)) (λ x → c * (a * x)) b (λ x → transitive *Associative (transitive (*WellDefined *Commutative reflexive) (symmetric *Associative)))) (sym (mapMap'' (_*_ c) (_*_ a) b)))) (trans (mapWd (_*_ (c * x)) (λ y → c * (x * y)) as λ y → symmetric *Associative) (sym (mapMap'' (_*_ c) (_*_ x) as)))) (sym (mapDist (_*_ c) *DistributesOver+ (map (_*_ a) b) (map (_*_ x) as)))) (symmetric timesZero ,, mapTimes as b c)) (sym (mapDist (_*_ c) *DistributesOver+ (map (_*_ a) b +P map (_*_ x) as) (0G :: (as *P b))))
      where
        open Equivalence (Setoid.eq naivePolySetoid) renaming (transitive to trans ; symmetric to sym ; reflexive to ref)

    mapTimes' : (a b : NaivePoly) (c : A) → polysEqual (map (_*_ c) (a *P b)) ((map (_*_ c) a) *P b)
    mapTimes' a b c = trans (trans (mapWellDefined' c (a *P b) (b *P a) (p*Commutative {a} {b})) (sym (mapTimes b a c))) (p*Commutative {b} {map (_*_ c) a})
      where
        open Equivalence (Setoid.eq naivePolySetoid) renaming (transitive to trans ; symmetric to sym ; reflexive to ref)

  bumpTimes' : (a bs : NaivePoly) (b : A) → polysEqual (a *P (b :: bs)) (map (_*_ b) a +P (0G :: (a *P bs)))
  bumpTimes' [] bs b = reflexive ,, record {}
  bumpTimes' (x :: a) bs b = transitive *Commutative (symmetric identRight) ,, trans (+PwellDefined {map (_*_ x) bs +P map (_*_ b) a} {0G :: (a *P bs)} {_} {0G :: (a *P bs)} (+PCommutative {map (_*_ x) bs} {map (_*_ b) a}) (ref {0G :: (a *P bs)})) (trans (sym (Group.+Associative polyGroup {map (_*_ b) a})) (+PwellDefined {map (_*_ b) a} {_} {map (_*_ b) a} {_} (ref {map (_*_ b) a}) (trans (trans (+PwellDefined {map (_*_ x) bs} {_} {map (_*_ x) bs} (ref {map (_*_ x) bs}) (reflexive ,, p*Commutative {a})) (sym (bumpTimes' bs a x))) (p*Commutative {bs}))))
    where
      open Equivalence (Setoid.eq naivePolySetoid) renaming (transitive to trans ; symmetric to sym ; reflexive to ref)

  bumpTimes : {a b : NaivePoly} → polysEqual (a *P (0G :: b)) (0G :: (a *P b))
  bumpTimes {[]} {b} = reflexive ,, record {}
  bumpTimes {x :: a} {[]} = timesZero ,, trans (sym (Group.+Associative polyGroup {[]} {map (_*_ 0G) a})) ans
    where
      open Equivalence (Setoid.eq naivePolySetoid) renaming (transitive to trans ; symmetric to sym ; reflexive to ref)
      ans : polysEqual (map id (map (_*_ 0G) a +P (0G :: (a *P [])))) []
      ans rewrite mapId (map (_*_ 0G) a +P (0G :: (a *P []))) = (+PwellDefined {map (_*_ 0G) a} {0G :: (a *P [])} {[]} {[]} (zeroTimes1 0G reflexive) (reflexive ,, p*Commutative {a}))
  bumpTimes {x :: a} {b :: bs} = timesZero ,, trans (+PwellDefined {((x * b) :: map (_*_ x) bs) +P map (_*_ 0G) a} {0G :: (a *P (b :: bs))} {(x * b) :: map (_*_ x) bs} {0G :: (a *P (b :: bs))} (trans (+PwellDefined {(x * b) :: map (_*_ x) bs} {map (_*_ 0G) a} {(x * b) :: map (_*_ x) bs} {[]} (ref {(x * b) :: map (_*_ x) bs}) (zeroTimes1 0G reflexive)) (Group.identRight polyGroup {(x * b) :: map (_*_ x) bs})) (ref {0G :: (a *P (b :: bs))})) (identRight ,, trans (+PwellDefined {map (_*_ x) bs} {_} {map (_*_ x) bs} ref (bumpTimes' a bs b)) (Group.+Associative polyGroup {map (_*_ x) bs} {map (_*_ b) a} {0G :: (a *P bs)}))
    where
      open Equivalence (Setoid.eq naivePolySetoid) renaming (transitive to trans ; symmetric to sym ; reflexive to ref)

  *Pdistrib : {a b c : NaivePoly} → polysEqual (a *P (b +P c)) ((a *P b) +P (a *P c))
  *Pdistrib {[]} {b} {c} = record {}
  *Pdistrib {a :: as} {[]} {[]} = record {}
  *Pdistrib {a :: as} {[]} {c :: cs} rewrite mapId cs | mapId ((map (_*_ a) cs +P map (_*_ c) as) +P (0G :: (as *P cs))) = reflexive ,, +PwellDefined {(map (_*_ a) cs) +P (map (_*_ c) as)} {_} {(map (_*_ a) cs) +P (map (_*_ c) as)} (Equivalence.reflexive (Setoid.eq naivePolySetoid)) (Equivalence.reflexive (Setoid.eq naivePolySetoid) {0G :: (as *P cs)})
  *Pdistrib {a :: as} {b :: bs} {[]} rewrite mapId bs | mapId ((map (_*_ a) bs +P map (_*_ b) as) +P (0G :: (as *P bs))) = reflexive ,, +PwellDefined {(map (_*_ a) bs) +P (map (_*_ b) as)} {_} {(map (_*_ a) bs) +P (map (_*_ b) as)} (Equivalence.reflexive (Setoid.eq naivePolySetoid)) (Equivalence.reflexive (Setoid.eq naivePolySetoid) {0G :: (as *P bs)})
  *Pdistrib {a :: as} {b :: bs} {c :: cs} = *DistributesOver+ ,, trans (+PwellDefined {(map (_*_ a) (bs +P cs)) +P (map (_*_ (b + c)) as)} {0G :: (as *P (bs +P cs))} {(map (_*_ a) bs +P map (_*_ b) as) +P ((map (_*_ a) cs) +P (map (_*_ c) as))} {0G :: ((as *P bs) +P (as *P cs))} (trans (+PwellDefined (mapDist (_*_ a) *DistributesOver+ bs cs) (mapDist' b c as)) (trans (sym (+Assoc {map (_*_ a) bs} {map (_*_ a) cs})) (trans (+PwellDefined (ref {map (_*_ a) bs}) (trans (trans (+Assoc {map (_*_ a) cs} {map (_*_ c) as}) ref) (+PCommutative {map (_*_ a) cs +P map (_*_ c) as} {map (_*_ b) as}))) (+Assoc {map (_*_ a) bs} {map (_*_ b) as})))) (reflexive ,, *Pdistrib {as} {bs} {cs})) (trans (sym (+Assoc {(map (_*_ a) bs +P map (_*_ b) as)} {(map (_*_ a) cs +P map (_*_ c) as)} {0G :: ((as *P bs) +P (as *P cs))})) (trans (+PwellDefined (ref {map (_*_ a) bs +P map (_*_ b) as}) (trans (trans (+PwellDefined (ref {map (_*_ a) cs +P map (_*_ c) as}) (symmetric identLeft ,, +PCommutative {as *P bs})) (+Assoc {map (_*_ a) cs +P (map (_*_ c) as)} {0G :: (as *P cs)} {0G :: (as *P bs)})) (+PCommutative {(map (_*_ a) cs +P map (_*_ c) as) +P (0G :: (as *P cs))} {0G :: (as *P bs)}))) (+Assoc {map (_*_ a) bs +P map (_*_ b) as} {0G :: (as *P bs)})))
    where
      open Equivalence (Setoid.eq naivePolySetoid) renaming (transitive to trans ; symmetric to sym ; reflexive to ref)
      open Group polyGroup renaming (+Associative to +Assoc ; 0G to 0P) hiding (identLeft)

*Passoc : {a b c : NaivePoly} → polysEqual (a *P (b *P c)) ((a *P b) *P c)
*Passoc {[]} {b} {c} = record {}
*Passoc {a :: as} {[]} {c} = record {}
*Passoc {a :: as} {b :: bs} {[]} = record {}
*Passoc {a :: as} {b :: bs} {c :: cs} = *Associative ,, trans (+PwellDefined {(map (_*_ a) ((map (_*_ b) cs +P map (_*_ c) bs) +P (0G :: (bs *P cs))) +P map (_*_ (b * c)) as)} {0G :: (as *P ((map (_*_ b) cs +P map (_*_ c) bs) +P (0G :: (bs *P cs))))} {(((map (_*_ (a * b)) cs) +P (map (_*_ (a * c)) bs)) +P (map (_*_ a) (0G :: (bs *P cs)))) +P (map (_*_ (b * c)) as)} {0G :: (((map (_*_ b) (as *P cs)) +P (map (_*_ c) (as *P bs))) +P (as *P (0G :: (bs *P cs))))} (+PwellDefined {map (_*_ a) ((map (_*_ b) cs +P map (_*_ c) bs) +P (0G :: (bs *P cs)))} {map (_*_ (b * c)) as} {((map (_*_ (a * b)) cs +P map (_*_ (a * c)) bs) +P ((a * 0G) :: map (_*_ a) (bs *P cs)))} {map (_*_ (b * c)) as} (trans (mapDist (_*_ a) *DistributesOver+ (map (_*_ b) cs +P map (_*_ c) bs) (0G :: (bs *P cs))) (+PwellDefined {map (_*_ a) (map (_*_ b) cs +P map (_*_ c) bs)} {(a * 0G) :: map (_*_ a) (bs *P cs)} {map (_*_ (a * b)) cs +P map (_*_ (a * c)) bs} (trans (mapDist (_*_ a) *DistributesOver+ (map (_*_ b) cs) (map (_*_ c) bs)) (+PwellDefined {map (_*_ a) (map (_*_ b) cs)} {map (_*_ a) (map (_*_ c) bs)} {map (_*_ (a * b)) cs} (trans (mapMap'' (_*_ a) (_*_ b) cs) (mapWd (λ x → a * (b * x)) (_*_ (a * b)) cs (λ x → *Associative))) (trans (mapMap'' (_*_ a) (_*_ c) bs) (mapWd (λ x → a * (c * x)) (_*_ (a * c)) bs λ x → *Associative)))) (ref {(a * 0G) :: map (_*_ a) (bs *P cs)}))) (ref {map (_*_ (b * c)) as})) (reflexive ,, trans (*Pdistrib {as} {(map (_*_ b) cs +P map (_*_ c) bs)} {0G :: (bs *P cs)}) (+PwellDefined {(as *P (map (_*_ b) cs +P map (_*_ c) bs))} {as *P (0G :: (bs *P cs))} {(map (_*_ b) (as *P cs) +P map (_*_ c) (as *P bs))} (trans (*Pdistrib {as} {map (_*_ b) cs} {map (_*_ c) bs}) (+PwellDefined {as *P map (_*_ b) cs} {as *P map (_*_ c) bs} {map (_*_ b) (as *P cs)} (mapTimes as cs b) (mapTimes as bs c))) (ref {as *P (0G :: (bs *P cs))})))) (trans (trans (sym (Group.+Associative polyGroup {((map (_*_ (a * b)) cs) +P (map (_*_ (a * c)) bs)) +P ((a * 0G) :: map (_*_ a) (bs *P cs))})) (trans (sym (Group.+Associative polyGroup {(map (_*_ (a * b)) cs) +P (map (_*_ (a * c)) bs)})) (trans (sym (Group.+Associative polyGroup {map (_*_ (a * b)) cs})) (+PwellDefined {map (_*_ (a * b)) cs} (ref {map (_*_ (a * b)) cs}) (trans (trans ans (Group.+Associative polyGroup {map (_*_ c) (map (_*_ a) bs +P map (_*_ b) as)})) (+PwellDefined {_} {0G :: (((map (_*_ a) bs +P map (_*_ b) as) +P (0G :: (as *P bs))) *P cs)} {map (_*_ c) ((map (_*_ a) bs +P map (_*_ b) as) +P (0G :: (as *P bs)))} (sym (mapDist (_*_ c) *DistributesOver+ ((map (_*_ a) bs +P map (_*_ b) as)) (0G :: (as *P bs)))) (ref {0G :: (((map (_*_ a) bs +P map (_*_ b) as) +P (0G :: (as *P bs))) *P cs)}))))))) (Group.+Associative polyGroup {map (_*_ (a * b)) cs} {map (_*_ c) ((map (_*_ a) bs +P map (_*_ b) as) +P (0G :: (as *P bs)))}))
  where
    open Equivalence (Setoid.eq naivePolySetoid) renaming (transitive to trans ; symmetric to sym ; reflexive to ref)
    open Group polyGroup renaming (+Associative to +Assoc ; 0G to 0P) hiding (identLeft ; identRight)
    ans2 : polysEqual ((map (_*_ a) (bs *P cs) +P (map (_*_ b) (as *P cs) +P map (_*_ c) (as *P bs))) +P (as *P (0G :: (bs *P cs)))) (map (_*_ c) (as *P bs) +P (((map (_*_ a) bs +P map (_*_ b) as) +P (0G :: (as *P bs))) *P cs))
    ans2 = trans (+PwellDefined {_} {as *P (0G :: (bs *P cs))} {_} {as *P (0G :: (bs *P cs))} (trans (+Assoc {map (_*_ a) (bs *P cs)} {map (_*_ b) (as *P cs)} {map (_*_ c) (as *P bs)}) (+PCommutative {map (_*_ a) (bs *P cs) +P map (_*_ b) (as *P cs)} {map (_*_ c) (as *P bs)})) ref) (trans (sym (+Assoc {map (_*_ c) (as *P bs)} {_} {as *P (0G :: (bs *P cs))}) ) (+PwellDefined {map (_*_ c) (as *P bs)} {_} {map (_*_ c) (as *P bs)} ref (trans (+PwellDefined {map (_*_ a) (bs *P cs) +P map (_*_ b) (as *P cs)} {as *P (0G :: (bs *P cs))} {((map (_*_ a) bs) *P cs) +P ((map (_*_ b) as) *P cs)} {0G :: (as *P (bs *P cs))} (+PwellDefined {map (_*_ a) (bs *P cs)} {map (_*_ b) (as *P cs)} {map (_*_ a) bs *P cs} {map (_*_ b) as *P cs} (mapTimes' bs cs a) (mapTimes' as cs b)) (bumpTimes {as} {bs *P cs})) (trans (trans (+PwellDefined {(map (_*_ a) bs *P cs) +P (map (_*_ b) as *P cs)} {0G :: (as *P (bs *P cs))} {cs *P (map (_*_ a) bs +P map (_*_ b) as)} {cs *P (0G :: (as *P bs))} (trans (+PwellDefined {map (_*_ a) bs *P cs} {map (_*_ b) as *P cs} {cs *P map (_*_ a) bs} {cs *P map (_*_ b) as} (p*Commutative {_} {cs}) (p*Commutative {_} {cs})) (sym (*Pdistrib {cs} {map (_*_ a) bs} {map (_*_ b) as}))) (trans (reflexive ,, trans (*Passoc {as} {bs} {cs}) (p*Commutative {_} {cs})) (sym (bumpTimes {cs} {as *P bs})))) (sym (*Pdistrib {cs} {(map (_*_ a) bs) +P (map (_*_ b) as)} {0G :: (as *P bs)}))) (p*Commutative {cs} {(map (_*_ a) bs +P map (_*_ b) as) +P (0G :: (as *P bs))})))))
    ans :
      polysEqual
        ((map (_*_ (a * c)) bs) +P (((a * 0G) :: map (_*_ a) (bs *P cs)) +P (map (_*_ (b * c)) as +P (0G :: ((map (_*_ b) (as *P cs) +P map (_*_ c) (as *P bs)) +P (as *P (0G :: (bs *P cs))))))))
        ((map (_*_ c) ((map (_*_ a) bs) +P (map (_*_ b) as))) +P (((c * 0G) :: map (_*_ c) (as *P bs)) +P (0G :: (((map (_*_ a) bs +P map (_*_ b) as) +P (0G :: (as *P bs))) *P cs))))
    ans = trans (trans (+PwellDefined {map (_*_ (a * c)) bs} {_} {map (_*_ c) (map (_*_ a) bs)} (trans (mapWd (_*_ (a * c)) (λ x → c * (a * x)) bs (λ x → transitive (*WellDefined *Commutative reflexive) (symmetric *Associative))) (sym (mapMap'' (_*_ c) (_*_ a) bs))) (trans (+PCommutative {(a * 0G) :: map (_*_ a) (bs *P cs)} {map (_*_ (b * c)) as +P (0G :: ((map (_*_ b) (as *P cs) +P map (_*_ c) (as *P bs)) +P (as *P (0G :: bs *P cs))))}) (trans (sym (+Assoc {map (_*_ (b * c)) as})) (+PwellDefined {map (_*_ (b * c)) as} {_} {map (_*_ c) (map (_*_ b) as)} (trans (mapWd (_*_ (b * c)) (λ x → c * (b * x)) as λ x → transitive (*WellDefined *Commutative reflexive) (symmetric *Associative)) (sym (mapMap'' (_*_ c) (_*_ b) as))) (transitive identLeft (transitive (transitive timesZero (symmetric timesZero)) (symmetric identRight)) ,, trans (+PCommutative {(map (_*_ b) (as *P cs) +P map (_*_ c) (as *P bs)) +P (as *P (0G :: (bs *P cs)))} {map (_*_ a) (bs *P cs)}) (trans (+Assoc {map (_*_ a) (bs *P cs)} {(map (_*_ b) (as *P cs)) +P (map (_*_ c) (as *P bs))} {as *P (0G :: (bs *P cs))}) ans2)))))) (+Assoc {map (_*_ c) (map (_*_ a) bs)})) (+PwellDefined {(map (_*_ c) (map (_*_ a) bs)) +P (map (_*_ c) (map (_*_ b) as))} {(((c * 0G) :: map (_*_ c) (as *P bs)) +P (0G :: (((map (_*_ a) bs +P map (_*_ b) as) +P (0G :: (as *P bs))) *P cs)))} {map (_*_ c) ((map (_*_ a) bs) +P (map (_*_ b) as))} {(((c * 0G) :: map (_*_ c) (as *P bs)) +P (0G :: (((map (_*_ a) bs +P map (_*_ b) as) +P (0G :: (as *P bs))) *P cs)))} (sym (mapDist (_*_ c) (*DistributesOver+) (map (_*_ a) bs) (map (_*_ b) as))) (ref {(((c * 0G) :: map (_*_ c) (as *P bs)) +P (0G :: (((map (_*_ a) bs +P map (_*_ b) as) +P (0G :: (as *P bs))) *P cs)))}))


text:
module Relation.Binary.Lattice.Residuated where

open import Level
open import Algebra.FunctionProperties using (Op₂)
open import Algebra.Structures using (IsMonoid)
open import Algebra using (Monoid)
open import Relation.Binary
open import Relation.Binary.Core
open import Relation.Binary.Lattice using (Lattice; IsLattice)
open import Data.Product

LeftResidual : ∀ {c ℓ₂} {L : Set c}
                → (_≤_ : Rel L ℓ₂) -- The partial order.
                → (_∙_ : Op₂ L)    -- The monoid operation.
                → (_◁_ : Op₂ L)    -- The left residual.
                → Set (c ⊔ ℓ₂)
LeftResidual _≤_ _∙_ _◁_ = ∀ y z → (((z ◁ y) ∙ y) ≤ z) × (Maximum _≤_ (z ◁ y))

RightResidual : ∀ {c ℓ₂} {L : Set c}
                → (_≤_ : Rel L ℓ₂) -- The partial order.
                → (_∙_ : Op₂ L)    -- The monoid operation.
                → (_▷_ : Op₂ L)    -- The right residual.
                → Set (c ⊔ ℓ₂)
RightResidual _≤_ _∙_ _▷_ = ∀ x z → ((x ∙ (x ▷ z)) ≤ z) × (Maximum _≤_ (x ▷ z))

record IsResiduated {c ℓ₁ ℓ₂} {L : Set c}
                    (_≈_ : Rel L ℓ₁) -- The underlying equality.
                    (_≤_ : Rel L ℓ₂) -- The partial order.
                    (_∨_ : Op₂ L)    -- The join operation.
                    (_∧_ : Op₂ L)    -- The meet operation.
                    (_∙_ : Op₂ L)    -- The monoid operation.
                    (ε   : L)        -- The identity element.
                    (_▷_ : Op₂ L)    -- The right residual.
                    (_◁_ : Op₂ L)    -- The left residual.
                    : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
    field
        isLattice : IsLattice _≈_ _≤_ _∨_ _∧_
        isMonoid  : IsMonoid _≈_ _∙_ ε
        isLeftResidual : LeftResidual _≤_ _∙_ _◁_
        isRightResidual : RightResidual _≤_ _∙_ _▷_
        ∙-monotonic : _∙_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_

    -- ∀ x y x
    --           y ≤ x ▷ z
    --     ⇔ x ∙ y ≤     z
    --     ⇔ x     ≤     z ◁ y

    module Pre = IsPreorder (IsPartialOrder.isPreorder (IsLattice.isPartialOrder isLattice))

    -- theorems about the residuals, requires _∙_ to be monotonic
    ∙-at-left : ∀ x y z
        → y ≤ (x ▷ z)
        → (x ∙ y) ≤ z
    ∙-at-left x y z P = Pre.trans (∙-monotonic Pre.refl P) (proj₁ (isRightResidual x z))

    ∙-at-right : ∀ x y z
        → x ≤ (z ◁ y)
        → (x ∙ y) ≤ z
    ∙-at-right x y z P = Pre.trans (∙-monotonic P Pre.refl) (proj₁ (isLeftResidual y z))

    apply-▷ : ∀ x y z
        → (x ∙ y) ≤ z
        → y ≤ (x ▷ z)
    apply-▷ x y z P = proj₂ (isRightResidual x z) y

    apply-◁ : ∀ x y z
        → (x ∙ y) ≤ z
        → x ≤ (z ◁ y)
    apply-◁ x y z P = proj₂ (isLeftResidual y z) x

    -- other modules

    monoid : Monoid c ℓ₁
    monoid = record { isMonoid = isMonoid }

    lattice : Lattice c ℓ₁ ℓ₂
    lattice = record { isLattice = isLattice }

record Residuated c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
    infix  4 _≈_ _≤_
    infixr 6 _∨_
    infixr 7 _∧_
    infixr 5 _∙_
    infixr 8 _▷_ _◁_

    field
        Carrier   : Set c
        _≈_       : Rel Carrier ℓ₁  -- The underlying equality.
        _≤_       : Rel Carrier ℓ₂  -- The partial order.
        _∨_       : Op₂ Carrier     -- The join operation.
        _∧_       : Op₂ Carrier     -- The meet operation.
        _∙_       : Op₂ Carrier     -- The monoid operation.
        ε         : Carrier         -- The identity element.

        _▷_      : Op₂ Carrier      -- The right residual.
        _◁_      : Op₂ Carrier      -- The left residual.
        isResiduated : IsResiduated _≈_ _≤_ _∨_ _∧_ _∙_ ε _▷_ _◁_

ext: agda

max_stars_repo_name: banacorn/relalg

max_issues_repo_name: banacorn/relalg

max_forks_repo_name: banacorn/relalg


text:
{-

An induction principle for paths in a pushout, described in
Kraus and von Raumer, "Path Spaces of Higher Inductive Types in Homotopy Type Theory"
https://arxiv.org/abs/1901.06022

-}

{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Pushout.KrausVonRaumer where

open import Cubical.Foundations.Everything
open import Cubical.Data.Sigma
open import Cubical.HITs.Pushout.Base

private
  interpolate : ∀ {ℓ} {A : Type ℓ} {x y z : A} (q : y ≡ z)
    → PathP (λ i → x ≡ q i → x ≡ z) (_∙ q) (idfun _)
  interpolate q i p j =
    hcomp
      (λ k → λ
        { (j = i0) → p i0
        ; (j = i1) → q (i ∨ k)
        ; (i = i1) → p j
        })
      (p j)

  interpolateCompPath : ∀ {ℓ} {A : Type ℓ} {x y : A} (p : x ≡ y) {z : A} (q : y ≡ z)
   → (λ i → interpolate q i (λ j → compPath-filler p q i j)) ≡ refl
  interpolateCompPath p =
    J (λ z q → (λ i → interpolate q i (λ j → compPath-filler p q i j)) ≡ refl)
      (homotopySymInv (λ p i j → compPath-filler p refl (~ i) j) p)

module ElimL {ℓ ℓ' ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
  {f : A → B} {g : A → C} {b₀ : B}
  (P : ∀ b → Path (Pushout f g) (inl b₀) (inl b) → Type ℓ''')
  (Q : ∀ c → Path (Pushout f g) (inl b₀) (inr c) → Type ℓ''')
  (r : P b₀ refl)
  (e : (a : A) (q : inl b₀ ≡ inl (f a)) → P (f a) q ≃ Q (g a) (q ∙ push a))
  where

  Codes : (d : Pushout f g) (q : inl b₀ ≡ d) → Type ℓ'''
  Codes (inl b) q = P b q
  Codes (inr c) q = Q c q
  Codes (push a i) q =
    Glue
      (Q (g a) (interpolate (push a) i q))
      (λ
        { (i = i0) → _ , e a q
        ; (i = i1) → _ , idEquiv (Q (g a) q)
        })

  elimL : ∀ b q → P b q
  elimL _ = J Codes r

  elimR : ∀ c q → Q c q
  elimR _ = J Codes r

  refl-β : elimL b₀ refl ≡ r
  refl-β = transportRefl _

  push-β : (a : A) (q : inl b₀ ≡ inl (f a))
    → elimR (g a) (q ∙ push a) ≡ e a q .fst (elimL (f a) q)
  push-β a q =
    J-∙ Codes r q (push a)
    ∙ fromPathP
      (subst
       (λ α → PathP (λ i → Q (g a) (α i)) (e a q .fst (elimL (f a) q)) (e a q .fst (elimL (f a) q)))
       (interpolateCompPath q (push a) ⁻¹)
       refl)

module ElimR {ℓ ℓ' ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
  {f : A → B} {g : A → C} {c₀ : C}
  (P : ∀ b → Path (Pushout f g) (inr c₀) (inl b) → Type ℓ''')
  (Q : ∀ c → Path (Pushout f g) (inr c₀) (inr c) → Type ℓ''')
  (r : Q c₀ refl)
  (e : (a : A) (q : inr c₀ ≡ inl (f a)) → P (f a) q ≃ Q (g a) (q ∙ push a))
  where

  Codes : (d : Pushout f g) (q : inr c₀ ≡ d) → Type ℓ'''
  Codes (inl b) q = P b q
  Codes (inr c) q = Q c q
  Codes (push a i) q =
    Glue
      (Q (g a) (interpolate (push a) i q))
      (λ
        { (i = i0) → _ , e a q
        ; (i = i1) → _ , idEquiv (Q (g a) q)
        })

  elimL : ∀ b q → P b q
  elimL _ = J Codes r

  elimR : ∀ c q → Q c q
  elimR _ = J Codes r

  refl-β : elimR c₀ refl ≡ r
  refl-β = transportRefl _

  push-β : (a : A) (q : inr c₀ ≡ inl (f a))
    → elimR (g a) (q ∙ push a) ≡ e a q .fst (elimL (f a) q)
  push-β a q =
    J-∙ Codes r q (push a)
    ∙ fromPathP
      (subst
       (λ α → PathP (λ i → Q (g a) (α i)) (e a q .fst (elimL (f a) q)) (e a q .fst (elimL (f a) q)))
       (interpolateCompPath q (push a) ⁻¹)
       refl)

-- Example application: pushouts preserve embeddings

isEmbeddingInr : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
  {f : A → B} (g : A → C)
  → isEmbedding f → isEmbedding (inr {f = f} {g = g})
isEmbeddingInr {f = f} g fEmb c₀ c₁ =
  isoToIsEquiv (iso _ (fst ∘ bwd c₁) (snd ∘ bwd c₁) bwdCong)
  where
  Q : ∀ c → inr c₀ ≡ inr c → Type _
  Q _ q = fiber (cong inr) q

  P : ∀ b → inr c₀ ≡ inl b → Type _
  P b p = Σ[ u ∈ fiber f b ] Q _ (p ∙ cong inl (u .snd ⁻¹) ∙ push (u .fst))

  module Bwd = ElimR P Q
    (refl , refl)
    (λ a p →
      subst
        (P (f a) p  ≃_)
        (cong (λ w → fiber (cong inr) (p ∙ w)) (lUnit (push a) ⁻¹))
        (Σ-contractFst (inhProp→isContr (a , refl) (isEmbedding→hasPropFibers fEmb (f a)))))

  bwd : ∀ c → (t : inr c₀ ≡ inr c) → fiber (cong inr) t
  bwd = Bwd.elimR

  bwdCong : ∀ {c} → (r : c₀ ≡ c) → bwd c (cong inr r) .fst ≡ r
  bwdCong = J (λ c r → bwd c (cong inr r) .fst ≡ r) (cong fst Bwd.refl-β)

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
record R₁ : Set₂ where
  field
    _≡_ : {A : Set₁} → A → A → Set

postulate
  A B : Set

record R₂ (r₁ : R₁) : Set₂ where
  open R₁ r₁
  field
    cong  : (A : Set₁) (x y : A) (F : A → Set) → x ≡ y → F x ≡ F y
    subst : (P : Set → Set₁) → A ≡ B → P A → P B

postulate
  _≡_ : {A : Set₁} → A → A → Set

r₁ : R₁
r₁ .R₁._≡_ = _≡_

postulate
  r₂ : ∀ r₁ → R₂ r₁

open R₂ (r₂ r₁)

record R₃ (@0 A : Set₁) : Set₁ where
  constructor [_]
  field
    f : A

postulate
  r₃            : R₃ Set
  push-subst-[] :
    (P : Set → Set₁) (p : P A) (eq : A ≡ B) →
    subst (λ A → R₃ (P A)) eq [ p ] ≡ [ subst P eq p ]

_ :
  (eq : A ≡ B) →
  (subst (λ _ → R₃ Set) eq r₃ ≡ r₃) ≡
  ([ subst (λ _ → Set) eq (r₃ .R₃.f) ] ≡ r₃)
_ = λ eq → cong _ _ _ (_≡ _) (push-subst-[] _ _ _)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import lib.Basics
open import lib.types.Paths

module lib.types.Unit where

pattern tt = unit

⊙Unit : Ptd₀
⊙Unit = ⊙[ Unit , unit ]

abstract
  -- Unit is contractible
  Unit-is-contr : is-contr Unit
  Unit-is-contr = (unit , λ y → idp)

  Unit-is-prop : is-prop Unit
  Unit-is-prop = raise-level -2 Unit-is-contr

  Unit-is-set : is-set Unit
  Unit-is-set = raise-level -1 Unit-is-prop

  Unit-level = Unit-is-contr
  ⊤-is-contr = Unit-is-contr
  ⊤-level = Unit-is-contr
  ⊤-is-prop = Unit-is-prop
  ⊤-is-set = Unit-is-set

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
open import Syntax

module Categories.Category.Construction.Renaming {ℓ₁ ℓ₂} (Sg : Signature ℓ₁ ℓ₂) where

open import Relation.Binary using (Rel)
open import Data.List using (List; []; [_]; _∷_; length; _++_)
open import Level using (zero; _⊔_)

open import Categories.Category

open Signature Sg

data ren : Rel Context ℓ₁ where
  id : forall {Γ} -> ren Γ Γ
  _∙_ : forall {Γ₁ Γ₂ Γ₃} -> ren Γ₂ Γ₃ -> ren Γ₁ Γ₂ -> ren Γ₁ Γ₃
  ! : forall {Γ} -> ren Γ []
  ⟪_,_⟫ : forall {Γ Γ₁ Γ₂} -> ren Γ Γ₁ -> ren Γ Γ₂ -> ren Γ (Γ₂ ++ Γ₁)
  p : forall {Γ Γ′} -> ren (Γ′ ++ Γ) Γ
  q : forall {Γ Γ′} -> ren (Γ′ ++ Γ) Γ′

data _≐_ : forall {Γ Γ′} -> Rel (ren Γ Γ′) ℓ₁ where
  refl : forall {Γ Γ′} {f : ren Γ Γ′} -> f ≐ f
  sym : forall {Γ Γ′} {f g : ren Γ Γ′} -> f ≐ g -> g ≐ f
  trans : forall {Γ Γ′} {f g h : ren Γ Γ′} -> f ≐ g -> g ≐ h -> f ≐ h

  identityˡ : forall {Γ Γ′} {f : ren Γ Γ′} -> (id ∙ f) ≐ f
  identityʳ : forall {Γ Γ′} {f : ren Γ Γ′} -> (f ∙ id) ≐ f
  assoc : forall {Γ Γ′ Γ″ Γ‴} {h : ren Γ Γ′} {g : ren Γ′ Γ″} {f : ren Γ″ Γ‴}
    -> ((f ∙ g) ∙ h) ≐ (f ∙ (g ∙ h))

  !-unique : forall {Γ} {f : ren Γ []} -> ! ≐ f

  β₁/⟪⟫ : forall {Γ Γ₁ Γ₂} {f : ren Γ Γ₁} {g : ren Γ Γ₂} -> (p ∙ ⟪ f , g ⟫) ≐ f
  β₂/⟪⟫ : forall {Γ Γ₁ Γ₂} {f : ren Γ Γ₁} {g : ren Γ Γ₂} -> (q ∙ ⟪ f , g ⟫) ≐ g
  η/⟪⟫ : forall {Γ Γ₁ Γ₂} {f : ren Γ (Γ₂ ++ Γ₁)} -> ⟪ p {Γ = Γ₁} ∙ f , q {Γ′ = Γ₂} ∙ f ⟫ ≐ f

  cong/∙ : forall {Γ₁ Γ₂ Γ₃} {g i : ren Γ₁ Γ₂} {f h : ren Γ₂ Γ₃} -> f ≐ h -> g ≐ i -> (f ∙ g) ≐ (h ∙ i)
  cong/⟪⟫ : forall {Γ Γ₁ Γ₂} {f h : ren Γ Γ₁} {g i : ren Γ Γ₂} -> f ≐ h -> g ≐ i -> ⟪ f , g ⟫ ≐ ⟪ h , i ⟫

Ren : Category ℓ₁ ℓ₁ ℓ₁
Ren = record
        { Obj = Context
        ; _⇒_ = ren
        ; _≈_ = _≐_
        ; id = id
        ; _∘_ = _∙_
        ; assoc = assoc
        ; sym-assoc = sym assoc
        ; identityˡ = identityˡ
        ; identityʳ = identityʳ
        ; identity² = identityˡ
        ; equiv = record { refl = refl ; sym = sym ; trans = trans }
        ; ∘-resp-≈ = cong/∙
        }

open import Categories.Category.Cartesian Ren
open import Categories.Category.BinaryProducts Ren
open import Categories.Object.Product Ren
open import Categories.Object.Terminal Ren

private
  P : forall {Γ₁ Γ₂} -> Product Γ₁ Γ₂
  P {Γ₁} {Γ₂} = record
         { A×B = Γ₂ ++ Γ₁
         ; π₁ = p
         ; π₂ = q
         ; ⟨_,_⟩ = ⟪_,_⟫
         ; project₁ = β₁/⟪⟫
         ; project₂ = β₂/⟪⟫
         ; unique = λ x x₁ →
             begin
               ⟪ _ , _ ⟫
             ≈˘⟨ cong/⟪⟫ x x₁ ⟩
               ⟪ _ , _ ⟫
             ≈⟨ η/⟪⟫ ⟩
               _
             ∎
         }
    where open Category.HomReasoning Ren

C : Cartesian
C = record { terminal = T ; products = record { product = P } }
  where
    T : Terminal
    T = record { ⊤ = [] ; ⊤-is-terminal = record { ! = ! ; !-unique = λ f → !-unique {f = f} } }

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 #-}
module NTypes.Unit where

open import Equivalence
open import NTypes
open import PathStructure.Unit
open import Types

1-isProp : isProp ⊤
1-isProp _ _ = merge-path _

1-isSet : isSet ⊤
1-isSet _ _ =
  prop-eq (sym-equiv split-merge-eq) 1-isProp

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
-- Andreas, 2018-03-12
-- The fix for #2963 introduced a change in the quotation behavior
-- of method definitions inside a record.

open import Agda.Builtin.Float
open import Agda.Builtin.Reflection
open import Agda.Builtin.List
open import Agda.Builtin.Unit
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

infixl 6 _>>=_
_>>=_ = bindTC

macro
  getDef : Name → Term → TC ⊤
  getDef x a = getDefinition x >>= quoteTC >>= unify a

record Foo (A : Set) : Set where
  constructor mkFoo
  field foo : A
  foo₁ : A
  foo₁ = foo

open module FooI = Foo {{...}}

postulate
  A : Set
  instance FooA : Foo A

-- Projection-like
foo₂ : {A : Set} {r : Foo A} → A
foo₂ {r = mkFoo x} = x

bar : A
bar = foo

bar₁ : A
bar₁ = foo₁

bar₂ : A
bar₂ = foo₂ {r = FooA}

pattern rArg v x = arg (arg-info v relevant) x
pattern vArg x = rArg visible x
pattern hArg x = rArg hidden  x
pattern iArg x = rArg instance′ x
pattern `? = hArg unknown

pattern fun₀ b = function (clause [] [] b ∷ [])
pattern fun₁ tel p b = function (clause tel (p ∷ []) b ∷ [])
pattern fun₂ tel p q b = function (clause tel (p ∷ q ∷ []) b ∷ [])

-- foo {{r}} = Foo.foo {_} r
foo-def : getDef foo ≡ fun₁
            (("r" , iArg (def (quote Foo) (vArg (var 0 []) ∷ []))) ∷ [])
            (iArg (var 0))
            (def (quote Foo.foo) (`? ∷ vArg (var 0 []) ∷ []))
foo-def = refl

-- Andreas, 2018-03-12: Behavior before fix of #2963:
-- foo₁ {{r}} = Foo.foo₁ {_} r
-- foo₁-def : getDef foo₁ ≡ fun₁ (iArg (var "r")) (def (quote Foo.foo₁) (`? ∷ vArg (var 0 []) ∷ []))
-- NOW:
-- foo₁ {A} {{r}} = Foo.foo₁ {A} r
foo₁-def : getDef foo₁ ≡ fun₂
             (("A" , hArg (agda-sort (lit 0))) ∷ ("r" , iArg (def (quote Foo) (vArg (var 0 []) ∷ []))) ∷ [])
             (hArg (var 1)) (iArg (var 0))
             (def (quote Foo.foo₁) (hArg (var 1 []) ∷ vArg (var 0 []) ∷ []))
foo₁-def = refl

-- bar = foo {_} FooA
bar-def : getDef bar ≡ fun₀ (def (quote Foo.foo) (`? ∷ vArg (def (quote FooA) []) ∷ []))
bar-def = refl

-- bar₁ = Foo.foo₁ {A} FooA
bar₁-def : getDef bar₁ ≡ fun₀ (def (quote Foo.foo₁) (hArg (def (quote A) [])  ∷ vArg (def (quote FooA) []) ∷ []))
bar₁-def =  refl

-- bar₂ = foo₂ {_} {FooA}
bar₂-def : getDef bar₂ ≡ fun₀ (def (quote foo₂) (`? ∷ hArg (def (quote FooA) []) ∷ []))
bar₂-def =  refl

--- Originally reported test case ---

defToTerm : Name → Definition → List (Arg Term) → Term
defToTerm _ (function cs) as = pat-lam cs as
defToTerm _ (data-cons d) as = con d as
defToTerm _ _ _ = unknown

derefImmediate : Term → TC Term
derefImmediate (def f args) = getDefinition f >>= λ f' → returnTC (defToTerm f f' args)
derefImmediate x = returnTC x

reflectTerm : Name → TC Term
reflectTerm n = getType n >>= λ ty → getDefinition n >>= λ x →
                derefImmediate (defToTerm n x []) >>= λ x → checkType x ty

macro
  reflect : Name → Term → TC ⊤
  reflect n a = reflectTerm n >>= quoteTC >>= unify a

{- Define typeclass Semigroup a => Plus a -}

record SemigroupLaws {ℓ} (t : Set ℓ) : Set ℓ where
  infixr 5 _++_
  field
    _++_ : t → t → t
    -- associative : ∀ {a b c} → (a ++ b) ++ c ≡ a ++ b ++ c

record PlusOp {ℓ} (t : Set ℓ) : Set ℓ where
  field
    semigroup : SemigroupLaws t

  infixr 6 _+_
  _+_ = SemigroupLaws._++_ semigroup

instance
  floatPlus : PlusOp Float
  floatPlus = record { semigroup = record { _++_ = Agda.Builtin.Float.primFloatPlus } }

open PlusOp {{...}}

-- The issue:

works : Float
works = PlusOp._+_ floatPlus 3.0 5.0

resultWorks : Term
resultWorks = reflect works

fails : Float
fails = 3.0 + 5.0

resultFails : Term
resultFails = reflect fails

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
module Issue586 where

{-# NO_TERMINATION_CHECK #-}
Foo : Set
Foo = Foo

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --without-K --safe #-}
module Categories.NaturalTransformation.Dinatural where

open import Level
open import Data.Product
open import Relation.Binary using (Rel; IsEquivalence; Setoid)

open import Categories.Category
open import Categories.NaturalTransformation as NT hiding (_∘ʳ_)
open import Categories.Functor
open import Categories.Functor.Construction.Constant
open import Categories.Functor.Bifunctor
open import Categories.Category.Product
import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e : Level
    C D E : Category o ℓ e

record DinaturalTransformation (F G : Bifunctor (Category.op C) C D) : Set (levelOfTerm F) where
  eta-equality
  private
    module C = Category C
    module D = Category D
    module F = Functor F
    module G = Functor G

  open D hiding (op)
  open Commutation

  field
    α          : ∀ X → D [ F.F₀ (X , X) , G.F₀ (X , X) ]
    commute    : ∀ {X Y} (f : C [ X , Y ]) →
                [ F.F₀ (Y , X) ⇒ G.F₀ (X , Y) ]⟨
                  F.F₁ (f , C.id)             ⇒⟨ F.F₀ (X , X) ⟩
                  α X                         ⇒⟨ G.F₀ (X , X) ⟩
                  G.F₁ (C.id , f)
                ≈ F.F₁ (C.id , f)             ⇒⟨ F.F₀ (Y , Y) ⟩
                  α Y                         ⇒⟨ G.F₀ (Y , Y) ⟩
                  G.F₁ (f , C.id)
                ⟩
    -- We add this extra proof, because, again, we want to ensure the opposite of the
    -- opposite of dinatural transformation is definitionally equal to itself.
    op-commute : ∀ {X Y} (f : C [ X , Y ]) →
                [ F.F₀ (Y , X) ⇒ G.F₀ (X , Y) ]⟨
                  F.F₁ (C.id , f)             ⇒⟨ F.F₀ (Y , Y) ⟩
                  (α Y                         ⇒⟨ G.F₀ (Y , Y) ⟩
                  G.F₁ (f , C.id))
                ≈ F.F₁ (f , C.id)             ⇒⟨ F.F₀ (X , X) ⟩
                  (α X                         ⇒⟨ G.F₀ (X , X) ⟩
                  G.F₁ (C.id , f))
                ⟩

  op : DinaturalTransformation G.op F.op
  op = record
    { α          = α
    ; commute    = op-commute
    ; op-commute = commute
    }

-- to reduce the burden of constructing a DinaturalTransformation, we introduce
-- another helper.
record DTHelper (F G : Bifunctor (Category.op C) C D) : Set (levelOfTerm F) where
  private
    module C = Category C
    module D = Category D
    module F = Functor F
    module G = Functor G
  open D hiding (op)
  open Commutation

  field
    α          : ∀ X → D [ F.F₀ (X , X) , G.F₀ (X , X) ]
    commute    : ∀ {X Y} (f : C [ X , Y ]) →
                [ F.F₀ (Y , X) ⇒ G.F₀ (X , Y) ]⟨
                  F.F₁ (f , C.id)             ⇒⟨ F.F₀ (X , X) ⟩
                  α X                         ⇒⟨ G.F₀ (X , X) ⟩
                  G.F₁ (C.id , f)
                ≈ F.F₁ (C.id , f)             ⇒⟨ F.F₀ (Y , Y) ⟩
                  α Y                         ⇒⟨ G.F₀ (Y , Y) ⟩
                  G.F₁ (f , C.id)
                ⟩

dtHelper : ∀ {F G : Bifunctor (Category.op C) C D} → DTHelper F G → DinaturalTransformation F G
dtHelper {D = D} θ = record
  { α          = α
  ; commute    = commute
  ; op-commute = λ f → assoc ○ ⟺ (commute f) ○ sym-assoc
  }
  where open DTHelper θ
        open Category D
        open HomReasoning

module _ {F G H : Bifunctor (Category.op C) C D} where
  private
    module C = Category C
  open Category D
  open HomReasoning
  open Functor
  open MR D

  infixr 9 _<∘_
  infixl 9 _∘>_

  _<∘_ : NaturalTransformation G H → DinaturalTransformation F G → DinaturalTransformation F H
  θ <∘ β = dtHelper record
    { α       = λ X → η (X , X) ∘ α X
    ; commute = λ {X Y} f → begin
      F₁ H (C.id , f) ∘ (η (X , X) ∘ α X) ∘ F₁ F (f , C.id)   ≈˘⟨ pushˡ (pushˡ (θ.commute (C.id , f))) ⟩
      ((η (X , Y) ∘ F₁ G (C.id , f)) ∘ α X) ∘ F₁ F (f , C.id) ≈⟨ assoc ○ pullʳ (β.commute f) ⟩
      η (X , Y) ∘ F₁ G (f , C.id) ∘ α Y ∘ F₁ F (C.id , f)     ≈⟨ pullˡ (θ.commute (f , C.id)) ○ pullʳ (⟺ assoc) ⟩
      F₁ H (f , C.id) ∘ (η (Y , Y) ∘ α Y) ∘ F₁ F (C.id , f)   ∎
    }
    where module θ = NaturalTransformation θ
          module β = DinaturalTransformation β
          open θ
          open β

  _∘>_ : DinaturalTransformation G H → NaturalTransformation F G → DinaturalTransformation F H
  β ∘> θ = dtHelper record
    { α       = λ X → α X ∘ η (X , X)
    ; commute = λ {X Y} f → begin
      F₁ H (C.id , f) ∘ (α X ∘ η (X , X)) ∘ F₁ F (f , C.id) ≈⟨ refl⟩∘⟨ pullʳ (θ.commute (f , C.id)) ⟩
      F₁ H (C.id , f) ∘ α X ∘ F₁ G (f , C.id) ∘ η (Y , X)   ≈˘⟨ assoc ○ ∘-resp-≈ʳ assoc ⟩
      (F₁ H (C.id , f) ∘ α X ∘ F₁ G (f , C.id)) ∘ η (Y , X) ≈⟨ β.commute f ⟩∘⟨refl ⟩
      (F₁ H (f , C.id) ∘ α Y ∘ F₁ G (C.id , f)) ∘ η (Y , X) ≈˘⟨ pushʳ (assoc ○ pushʳ (θ.commute (C.id , f))) ⟩
      F₁ H (f , C.id) ∘ (α Y ∘ η (Y , Y)) ∘ F₁ F (C.id , f) ∎
    }
    where module θ = NaturalTransformation θ
          module β = DinaturalTransformation β
          open θ
          open β

module _ {F G : Bifunctor (Category.op C) C D} where
  private
    module C = Category C
  open Category D
  open HomReasoning
  open Functor
  open MR D

  infixl 9 _∘ʳ_

  _∘ʳ_ : ∀ {E : Category o ℓ e} →
           DinaturalTransformation F G → (K : Functor E C) → DinaturalTransformation (F ∘F ((Functor.op K) ⁂ K)) (G ∘F ((Functor.op K) ⁂ K))
  _∘ʳ_ {E = E} β K = dtHelper record
    { α       = λ X → α (F₀ K X)
    ; commute = λ {X Y} f → begin
      F₁ G (F₁ K E.id , F₁ K f) ∘ α (F₀ K X) ∘ F₁ F (F₁ K f , F₁ K E.id)
        ≈⟨ F-resp-≈ G (identity K , C.Equiv.refl) ⟩∘⟨ refl ⟩∘⟨ F-resp-≈ F (C.Equiv.refl , identity K) ⟩
      F₁ G (C.id , F₁ K f) ∘ α (F₀ K X) ∘ F₁ F (F₁ K f , C.id)
        ≈⟨ commute (F₁ K f) ⟩
      F₁ G (F₁ K f , C.id) ∘ α (F₀ K Y) ∘ F₁ F (C.id , F₁ K f)
        ≈˘⟨ F-resp-≈ G (C.Equiv.refl , identity K) ⟩∘⟨ refl ⟩∘⟨ F-resp-≈ F (identity K , C.Equiv.refl) ⟩
      F₁ G (F₁ K f , F₁ K E.id) ∘ α (F₀ K Y) ∘ F₁ F (F₁ K E.id , F₁ K f)
        ∎
    }
    where module β = DinaturalTransformation β
          module E = Category E
          open β

  infix 4 _≃_

  _≃_ : Rel (DinaturalTransformation F G) _
  β ≃ δ = ∀ {X} → α β X ≈ α δ X
    where open DinaturalTransformation

  ≃-isEquivalence : IsEquivalence _≃_
  ≃-isEquivalence = record
    { refl  = refl
    ; sym   = λ eq → sym eq
    ; trans = λ eq eq′ → trans eq eq′
    }

  ≃-setoid : Setoid _ _
  ≃-setoid = record
    { Carrier       = DinaturalTransformation F G
    ; _≈_           = _≃_
    ; isEquivalence = ≃-isEquivalence
    }

-- for convenience, the following are some helpers for the cases
-- in which the bifunctor on the right is extranatural.
Extranaturalʳ : ∀ {C : Category o ℓ e} → Category.Obj D → (F : Bifunctor (Category.op C) C D) → Set _
Extranaturalʳ A F = DinaturalTransformation (const A) F

Extranaturalˡ : ∀ {C : Category o ℓ e} → (F : Bifunctor (Category.op C) C D) → Category.Obj D → Set _
Extranaturalˡ F A = DinaturalTransformation F (const A)

module _ {F : Bifunctor (Category.op C) C D} where
  open Category D
  private
    module C = Category C
    variable
      A : Obj
      X Y : C.Obj
      f : X C.⇒ Y
  open Functor F
  open HomReasoning
  open MR D

  extranaturalʳ : (a : ∀ X → A ⇒ F₀ (X , X)) →
                  (∀ {X X′ f} → F₁ (C.id , f) ∘ a X ≈ F₁ (f , C.id) ∘ a X′) →
                  Extranaturalʳ A F
  extranaturalʳ a comm = dtHelper record
    { α       = a
    ; commute = λ f → ∘-resp-≈ʳ identityʳ ○ comm ○ ∘-resp-≈ʳ (⟺ identityʳ)
    }

  open DinaturalTransformation

  extranatural-commʳ : (β : DinaturalTransformation (const A) F) →
                       F₁ (C.id , f) ∘ α β X ≈ F₁ (f , C.id) ∘ α β Y
  extranatural-commʳ {f = f} β = ∘-resp-≈ʳ (⟺ identityʳ) ○ commute β f ○ ∘-resp-≈ʳ identityʳ

  -- the dual case, the bifunctor on the left is extranatural.

  extranaturalˡ : (a : ∀ X → F₀ (X , X) ⇒ A) →
                  (∀ {X X′ f} → a X ∘ F₁ (f , C.id) ≈ a X′ ∘ F₁ (C.id , f)) →
                  Extranaturalˡ F A
  extranaturalˡ a comm = dtHelper record
    { α       = a
    ; commute = λ f → pullˡ identityˡ ○ comm ○ ⟺ (pullˡ identityˡ)
    }

  extranatural-commˡ : (β : DinaturalTransformation F (const A)) →
                       α β X ∘ F₁ (f , C.id) ≈ α β Y ∘ F₁ (C.id , f)
  extranatural-commˡ {f = f} β = ⟺ (pullˡ identityˡ) ○ commute β f ○ pullˡ identityˡ

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
open import Spire.Type
module Spire.Hybrid where

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

data Context : Set₁
Environment : Context → Set

ScopedType : Context → Set₁
ScopedType Γ = Environment Γ → Set

data Context where
  ∅ : Context
  _,_ : (Γ : Context) (A : ScopedType Γ) → Context

Environment ∅ = ⊤
Environment (Γ , A) = Σ (Environment Γ) A

data Var :  (Γ : Context) (A : ScopedType Γ) → Set₁ where
 here : ∀{Γ A} → Var (Γ , A) (λ vs → A (proj₁ vs))
 there : ∀{Γ A} {B : ScopedType Γ}
   → Var Γ A → Var (Γ , B) (λ vs → A (proj₁ vs))

lookup : ∀{Γ A} → Var Γ A → (vs : Environment Γ) → A vs
lookup here (vs , v) = v
lookup (there i) (vs , v) = lookup i vs

ScopedType₂ : (Γ : Context) → ScopedType Γ → Set₁
ScopedType₂ Γ A = (vs : Environment Γ) → A vs → Set

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

data Term (Γ : Context) : ScopedType Γ → Set₁
eval : ∀{Γ A} → Term Γ A → (vs : Environment Γ) → A vs

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

data Term Γ where
  {- Type introduction -}
  `⊥ `⊤ `Bool `ℕ `Type : ∀{ℓ}
    → Term Γ (const (Type ℓ))
  `Π `Σ : ∀{ℓ}
    (A : Term Γ (const (Type ℓ)))
    (B : Term (Γ , λ vs → ⟦ ℓ ∣ eval A vs ⟧) (const (Type ℓ)))
    → Term Γ (λ _ → Type ℓ)
  `⟦_⟧ : ∀{ℓ}
    (A : Term Γ (const (Type ℓ)))
    → Term Γ (const (Type (suc ℓ)))

  {- Value introduction -}
  `tt : Term Γ (const ⊤)
  `true `false : Term Γ (const Bool)
  `zero : Term Γ (const ℕ)
  `suc : Term Γ (const ℕ) → Term Γ (const ℕ)
  `λ : ∀{A} {B : ScopedType₂ Γ A}
    (f : Term (Γ , A) (λ vs → B (proj₁ vs) (proj₂ vs)))
    → Term Γ (λ vs → (v : A vs) → (B vs v))
  _`,_ : ∀{A} {B : ScopedType₂ Γ A}
    (a : Term Γ A)
    (b : Term Γ (λ vs → B vs (eval a vs)))
    → Term Γ (λ vs → Σ (A vs) (λ v → B vs v))

  {- Value elimination -}
  `var : ∀{A} (a : Var Γ A) → Term Γ A
  `elim⊥ : ∀{A ℓ}
    (P : Term Γ (const (Type ℓ)))
    (x : Term Γ (const ⊥))
    → Term Γ A
  `elimBool : ∀{ℓ}
    (P : Term (Γ , const Bool) (const (Type ℓ)))
    (pt : Term Γ (λ vs → ⟦ ℓ ∣ eval P (vs , true) ⟧))
    (pf : Term Γ (λ vs → ⟦ ℓ ∣ eval P (vs , false) ⟧))
    (b : Term Γ (const Bool))
    → Term Γ (λ vs → ⟦ ℓ ∣ eval P (vs , eval b vs) ⟧)
  `elimℕ : ∀{ℓ}
    (P : Term (Γ , (const ℕ)) (const (Type ℓ)))
    (pz : Term Γ (λ vs → ⟦ ℓ ∣ eval P (vs , zero) ⟧))
    (ps : Term ((Γ , const ℕ) , (λ { (vs , n)  → ⟦ ℓ ∣ eval P (vs , n) ⟧ }))
            (λ { ((vs , n) , p) → ⟦ ℓ ∣ eval P (vs , suc n) ⟧ }))
    (n : Term Γ (const ℕ))
    → Term Γ (λ vs → ⟦ ℓ ∣ eval P (vs , eval n vs) ⟧)
  _`$_ : ∀{A} {B : ScopedType₂ Γ A}
    (f : Term Γ (λ vs → (v : A vs) → (B vs v)))
    (a : Term Γ A)
    → Term Γ (λ vs → B vs (eval a vs))
  `proj₁ : ∀{A} {B : ScopedType₂ Γ A}
    (ab : Term Γ (λ vs → Σ (A vs) (B vs)))
    → Term Γ A
  `proj₂ : ∀{A} {B : ScopedType₂ Γ A}
    (ab : Term Γ (λ vs → Σ (A vs) (B vs)))
    → Term Γ (λ vs → B vs (proj₁ (eval ab vs)))

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

{- Type introduction -}
eval `⊥ vs = `⊥
eval `⊤ vs = `⊤
eval `Bool vs = `Bool
eval `ℕ vs = `ℕ
eval `Type vs = `Type
eval (`Π A B) vs = `Π (eval A vs) λ v → eval B (vs , v)
eval (`Σ A B) vs = `Σ (eval A vs) λ v → eval B (vs , v)
eval `⟦ A ⟧ vs = `⟦ eval A vs ⟧

{- Value introduction -}
eval `tt vs = tt
eval `true vs = true
eval `false vs = false
eval `zero vs = zero
eval (`suc n) vs = suc (eval n vs)
eval (`λ f) vs = λ v → eval f (vs , v)
eval (a `, b) vs = eval a vs , eval b vs

{- Value elimination -}
eval (`var i) vs = lookup i vs
eval (`elim⊥ P x) vs = elim⊥ (eval x vs)
eval (`elimBool {ℓ} P pt pf b) vs =
  elimBool (λ v → ⟦ ℓ ∣ eval P (vs , v) ⟧)
    (eval pt vs)
    (eval pf vs)
    (eval b vs)
eval (`elimℕ {ℓ} P pz ps n) vs =
  elimℕ (λ v → ⟦ ℓ ∣ eval P (vs , v) ⟧)
    (eval pz vs)
    (λ n rec → eval ps ((vs , n) , rec))
    (eval n vs)
eval (f `$ a) vs = (eval f vs) (eval a vs)
eval (`proj₁ ab) vs = proj₁ (eval ab vs)
eval (`proj₂ ab) vs = proj₂ (eval ab vs)

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

max_stars_repo_name: spire/spire

max_issues_repo_name: spire/spire

max_forks_repo_name: spire/spire


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

module Mixfix.Cyclic.Example where

open import Codata.Musical.Notation
open import Data.Vec using ([]; _∷_; [_])
open import Data.List as List
  using (List; []; _∷_) renaming ([_] to L[_])
open import Data.List.Relation.Unary.Any as Any using (here; there)
import Codata.Musical.Colist as Colist
open import Data.Product using (∃₂; -,_)
open import Data.Unit.Polymorphic using (⊤)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Fin using (Fin; #_; zero; suc)
import Data.List.Relation.Binary.Pointwise as ListEq
import Data.String as String
open String using (String; _++_)
import Data.String.Properties as String
open import Relation.Binary
open DecSetoid (ListEq.decSetoid String.≡-decSetoid) using (_≟_)
open import Function using (_∘_)
open import Data.Bool using (Bool; if_then_else_)
open import Relation.Nullary.Decidable using (⌊_⌋)
import Relation.Binary.PropositionalEquality as P
open import IO
import Level

open import Mixfix.Fixity hiding (_≟_)
open import Mixfix.Operator
open import Mixfix.Expr
open import Mixfix.Cyclic.PrecedenceGraph
  hiding (module PrecedenceGraph)
import Mixfix.Cyclic.Grammar as Grammar
import Mixfix.Cyclic.Show as Show
import TotalParserCombinators.BreadthFirst as BreadthFirst

------------------------------------------------------------------------
-- Operators

atom : Operator closed 0
atom = record { nameParts = "•" ∷ [] }

plus : Operator (infx left) 0
plus = record { nameParts = "+" ∷ [] }

ifThen : Operator prefx 1
ifThen = record { nameParts = "i" ∷ "t" ∷ [] }

ifThenElse : Operator prefx 2
ifThenElse = record { nameParts = "i" ∷ "t" ∷ "e" ∷ [] }

comma : Operator (infx left) 0
comma = record { nameParts = "," ∷ [] }

wellTyped : Operator postfx 1
wellTyped = record { nameParts = "⊢" ∷ "∶" ∷ [] }

------------------------------------------------------------------------
-- Precedence graph

mutual

  private

    levels : ℕ
    levels = 5

    a  = # 0
    pl = # 1
    ii = # 2
    c  = # 3
    wt = #_ 4 {n = levels}

  g : PrecedenceGraph
  g = record
    { levels = levels
    ; ops    = λ p fix → List.mapMaybe (hasFixity fix) (ops p)
    ; ↑      = ↑
    }
    where
    Precedence : Set
    Precedence = Fin levels

    ops : Precedence → List (∃₂ Operator)
    ops zero                             = (-, -, atom)       ∷ []
    ops (suc zero)                       = (-, -, plus)       ∷ []
    ops (suc (suc zero))                 = (-, -, ifThen)     ∷
                                           (-, -, ifThenElse) ∷ []
    ops (suc (suc (suc zero)))           = (-, -, comma)      ∷ []
    ops (suc (suc (suc (suc zero))))     = (-, -, wellTyped)  ∷ []
    ops (suc (suc (suc (suc (suc ())))))

    ↑ : Precedence → List (Precedence)
    ↑ zero                             = []
    ↑ (suc zero)                       = a ∷ []
    ↑ (suc (suc zero))                 = pl ∷ a ∷ []
    ↑ (suc (suc (suc zero)))           = ii ∷ pl ∷ a ∷ []
    ↑ (suc (suc (suc (suc zero))))     = c ∷ a ∷ []
    ↑ (suc (suc (suc (suc (suc ())))))

------------------------------------------------------------------------
-- Expressions

open PrecedenceCorrect cyclic g

• : ExprIn a non
• = ⟪ here P.refl ∙ [] ⟫

_+_ : Outer pl left → Expr (a ∷ []) → ExprIn pl left
e₁ + e₂ = e₁ ⟨ here P.refl ∙ [] ⟩ˡ e₂

i_t_ : Expr anyPrecedence → Outer ii right → ExprIn ii right
i e₁ t e₂ = ⟪ here P.refl ∙ e₁ ∷ [] ⟩ e₂

i_t_e_ : Expr anyPrecedence → Expr anyPrecedence → Outer ii right →
         ExprIn ii right
i e₁ t e₂ e e₃ = ⟪ there (here P.refl) ∙ e₁ ∷ e₂ ∷ [] ⟩ e₃

_,_ : Outer c left → Expr (ii ∷ pl ∷ a ∷ []) → ExprIn c left
e₁ , e₂ = e₁ ⟨ here P.refl ∙ [] ⟩ˡ e₂

_⊢_∶ : Outer wt left → Expr anyPrecedence → ExprIn wt left
e₁ ⊢ e₂ ∶ = e₁ ⟨ here P.refl ∙ [ e₂ ] ⟫

------------------------------------------------------------------------
-- Some tests

open Show cyclic g

fromNameParts : List NamePart → String
fromNameParts = List.foldr _++_ ""

toNameParts : String → List NamePart
toNameParts = List.map (String.fromList ∘ L[_]) ∘ String.toList

parseExpr : String → List String
parseExpr = List.map (fromNameParts ∘ show) ∘
            BreadthFirst.parse (Grammar.expression cyclic g) ∘
            toNameParts

runTest : String → List String → IO (⊤ {ℓ = Level.zero})
runTest s₁ s₂ = do
  putStrLn ("Testing: " ++ s₁)
  Colist.mapM′ putStrLn (Colist.fromList p₁)
  putStrLn (if ⌊ p₁ ≟ s₂ ⌋ then "Passed" else "Failed")
  where p₁ = parseExpr s₁

main = run do
  runTest "•+•⊢•∶"      []
  runTest "•,•⊢∶"       []
  runTest "•⊢•∶"        L[ "•⊢•∶" ]
  runTest "•,i•t•+•⊢•∶" L[ "•,i•t•+•⊢•∶" ]
  runTest "i•ti•t•e•"   ("i•ti•t•e•" ∷ "i•ti•t•e•" ∷ [])

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module Prelude where

infixr 90 _∘_
infixr 50 _∧_
infix  20 _⟸⇒_
infixl 3  _from_

_from_ : (A : Set) -> A -> A
A from a = a

_∘_ : {A B C : Set} -> (A -> B) -> (C -> A) -> C -> B
(f ∘ g) x = f (g x)

record _∧_ (A B : Set) : Set where
  field
    p₁ : A
    p₂ : B

open _∧_ public renaming (p₁ to fst; p₂ to snd)

_,_ : {A B : Set} -> A -> B -> A ∧ B
x , y = record { p₁ = x; p₂ = y }

swap : {A B : Set} -> A ∧ B -> B ∧ A
swap p = (snd p , fst p)

_⇐⇒_ : Set -> Set -> Set
A ⇐⇒ B = (A -> B) ∧ (B -> A)


text:
-- Andreas, 2020-02-18, issue #4450 raised by Nisse
--
-- ETA pragma should be considered unsafe, since type-checking may loop.

{-# OPTIONS --safe --guardedness #-}

open import Agda.Builtin.Equality

record R : Set where
 coinductive
 field
   force : R
open R

{-# ETA R #-}

foo : R
foo .force .force = foo

-- test : foo .force ≡ foo
-- test = refl

-- test makes type checker loop;
-- ETA with --safe is a soft error and only raised after
-- the whole file is processed.


text:
open import Relation.Binary.Core

module PLRTree.Order {A : Set} where

open import Data.Nat
open import Data.Sum
open import PLRTree {A}
open import Relation.Binary

open DecTotalOrder decTotalOrder hiding (refl)

height : PLRTree → ℕ
height leaf = zero
height (node t x l r)
    with total (height l) (height r)
... | inj₁ hl≤hr = suc (height r)
... | inj₂ hr≤hl = suc (height l)

_≺_ : PLRTree → PLRTree → Set
t ≺ t' = height t <′ height t'

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-# OPTIONS --without-K #-}
module well-typed-quoted-syntax where
open import common
open import well-typed-syntax
open import well-typed-syntax-helpers public
open import well-typed-quoted-syntax-defs public
open import well-typed-syntax-context-helpers public
open import well-typed-syntax-eq-dec public

infixr 2 _‘‘∘’’_

quote-sigma : (Γv : Σ Context Typ) → Term {ε} (‘Σ’ ‘Context’ ‘Typ’)
quote-sigma (Γ , v) = ‘existT’ ⌜ Γ ⌝c ⌜ v ⌝T

_‘‘∘’’_ : ∀ {A B C}
    → □ (‘□’ ‘’ (C ‘‘→'’’ B))
    → □ (‘□’ ‘’ (A ‘‘→'’’ C))
    → □ (‘□’ ‘’ (A ‘‘→'’’ B))
g ‘‘∘’’ f = (‘‘fcomp-nd’’ ‘'’ₐ f ‘'’ₐ g)

Conv0 : ∀ {qH0 qX} →
    Term {Γ = (ε ▻ ‘□’ ‘’ qH0)}
          (W (‘□’ ‘’ ⌜ ‘□’ ‘’ qH0 ‘→'’ qX ⌝T))
    → Term {Γ = (ε ▻ ‘□’ ‘’ qH0)}
             (W
                (‘□’ ‘’ (⌜ ‘□’ ‘’ qH0 ⌝T ‘‘→'’’ ⌜ qX ⌝T)))
Conv0 {qH0} {qX} x = w→ ⌜→'⌝ ‘'’ₐ x

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob


text:
open import Relation.Binary using (Preorder)
open import Relation.Binary.PropositionalEquality
open import Relation.Unary

module Category.Monad.Monotone.Reader {ℓ}(pre : Preorder ℓ ℓ ℓ) where

open Preorder pre renaming (Carrier to I; _∼_ to _≤_; refl to ≤-refl)

open import Relation.Unary.Monotone pre
open import Relation.Unary.PredicateTransformer using (Pt)
open import Data.Product
open import Function
open import Level hiding (lift)
open import Category.Monad
open import Category.Monad.Monotone.Identity pre
open import Category.Monad.Monotone pre

ReaderT : Pred I ℓ → Pt I ℓ → Pt I ℓ
ReaderT E M P = λ i → E i → M P i

Reader : (Pred I ℓ) → Pt I ℓ
Reader E = ReaderT E Identity

record ReaderMonad E (M : Pred I ℓ → Pt I ℓ) : Set (suc ℓ) where
  field
    ask    : ∀ {i} → M E E i
    reader : ∀ {P} → (E ⇒ P) ⊆ M E P
    local  : ∀ {P E'} → (E ⇒ E') ⊆ (M E' P ⇒ M E P)

  asks : ∀ {A} → (E ⇒ A) ⊆ M E A
  asks = reader

module _ {M : Pt I ℓ}⦃ Mon : RawMPMonad M ⦄ where
  private module M = RawMPMonad Mon

  module _ {E}⦃ mono : Monotone E ⦄ where
    instance
      open RawMPMonad
      reader-monad : RawMPMonad (ReaderT E M)
      return reader-monad x e = M.return x
      _≥=_  reader-monad m f e = m e M.≥= λ i≤j px → f i≤j px (wk i≤j e)

      open ReaderMonad
      reader-monad-ops : ReaderMonad E (λ E → ReaderT E M)
      ask reader-monad-ops e = M.return e
      reader reader-monad-ops f e = M.return (f e)
      local reader-monad-ops f c e = c (f e)

  lift-reader : ∀ {P} E → M P ⊆ ReaderT E M P
  lift-reader _ z _ = z


text:
open import Nat
open import Prelude
open import List
open import core
open import judgemental-erase
open import checks
open import moveerase

module aasubsume-min where
  -- this predicate on derivations of actions bans the cases that induce
  -- non-determinism.
  mutual
    aasubmin-synth : ∀{Γ e t α e' t'} → (Γ ⊢ e => t ~ α ~> e' => t') → Set
    aasubmin-synth (SAZipAsc1 x) = aasubmin-ana x
    aasubmin-synth (SAZipApArr x x₁ x₂ d x₃) = aasubmin-synth d
    aasubmin-synth (SAZipApAna x x₁ x₂) = aasubmin-ana x₂
    aasubmin-synth (SAZipPlus1 x) = aasubmin-ana x
    aasubmin-synth (SAZipPlus2 x) = aasubmin-ana x
    aasubmin-synth (SAZipHole x x₁ d) = aasubmin-synth d
    aasubmin-synth _ = ⊤

    aasubmin-ana : ∀{Γ e α e' t} → (Γ ⊢ e ~ α ~> e' ⇐ t) → Set
    aasubmin-ana (AASubsume x x₁ SAConAsc x₃) = ⊥
    aasubmin-ana (AASubsume x x₁ (SAConLam x₃) x₄) = ⊥
    aasubmin-ana (AASubsume x x₁ s x₃) = aasubmin-synth s
    aasubmin-ana (AAZipLam x₁ x₂ d) = aasubmin-ana d
    aasubmin-ana _ = ⊤

  -- the minimization predicate propagates through subsumption rules
  min-ana-lem : ∀{e e' e◆ Γ t t' t'' α}
                 {a : erase-e e e◆}
                 {b : Γ ⊢ e◆ => t'}
                 {c : t ~ t''} →
                 (d : Γ ⊢ e => t' ~ α ~> e' => t'')
                → aasubmin-ana (AASubsume a b d c) → aasubmin-synth d
  min-ana-lem (SAMove x) min = <>
  min-ana-lem (SADel) min = <>
  min-ana-lem (SAConAsc) min = <>
  min-ana-lem (SAConVar p) min = <>
  min-ana-lem (SAConLam x₁) min = <>
  min-ana-lem (SAConApArr x) min = <>
  min-ana-lem (SAConApOtw x) min = <>
  min-ana-lem (SAConNumlit) min = <>
  min-ana-lem (SAConPlus1 x) min = <>
  min-ana-lem (SAConPlus2 x) min = <>
  min-ana-lem (SAConNEHole) min = <>
  min-ana-lem (SAFinish x) min = <>
  min-ana-lem (SAZipAsc1 x) min = min
  min-ana-lem (SAZipAsc2 x x₁ x₂ x₃) min = <>
  min-ana-lem (SAZipApArr x x₁ x₂ c x₃) min = min
  min-ana-lem (SAZipApAna x x₁ x₂) min = min
  min-ana-lem (SAZipPlus1 x) min = min
  min-ana-lem (SAZipPlus2 x) min = min
  min-ana-lem (SAZipHole x x₁ c) min = min

  -- any derivation of an action can be minimized to avoid this cases that
  -- induce non-determinism.
  mutual
    min-synth : ∀{Γ e t α e' t'} → (d : Γ ⊢ e => t ~ α ~> e' => t') →
                        Σ[ e'' ∈ ê ] Σ[ d' ∈ Γ ⊢ e => t ~ α ~> e'' => t' ] aasubmin-synth d'
    min-synth (SAMove x) = _ , SAMove x , <>
    min-synth SADel = _ , SADel , <>
    min-synth SAConAsc = _ , SAConAsc , <>
    min-synth (SAConVar p) = _ , SAConVar p , <>
    min-synth (SAConLam x₁) = _ , SAConLam x₁ , <>
    min-synth (SAConApArr x) = _ , SAConApArr x , <>
    min-synth (SAConApOtw x) = _ , SAConApOtw x , <>
    min-synth SAConNumlit = _ , SAConNumlit , <>
    min-synth (SAConPlus1 x) = _ , SAConPlus1 x , <>
    min-synth (SAConPlus2 x) = _ , SAConPlus2 x , <>
    min-synth SAConNEHole = _ , SAConNEHole , <>
    min-synth (SAFinish x) = _ , SAFinish x , <>
    min-synth (SAZipAsc2 x x₁ x₂ x₃) = _ , SAZipAsc2 x x₁ x₂ x₃ , <>
    min-synth (SAZipAsc1 x) with min-ana x
    ... | _ , a , b = _ ,  SAZipAsc1 a , b
    min-synth (SAZipApArr x x₁ x₂ d x₃) with min-synth d
    ... | _ , a , b = _ , (SAZipApArr x x₁ x₂ a x₃) , b
    min-synth (SAZipApAna x x₁ x₂) with min-ana x₂
    ... | _ , a , b = _ , SAZipApAna x x₁ a , b
    min-synth (SAZipPlus1 x) with min-ana x
    ... | _ , a , b = _ , SAZipPlus1 a , b
    min-synth (SAZipPlus2 x) with min-ana x
    ... | _ , a , b = _ , SAZipPlus2 a , b
    min-synth (SAZipHole x x₁ d) with min-synth d
    ... | _ , a , b = _ , SAZipHole x x₁ a , b

    min-ana : ∀{Γ e α e' t} → (d : Γ ⊢ e ~ α ~> e' ⇐ t) → Σ[ e'' ∈ ê ] Σ[ d' ∈  Γ ⊢ e ~ α ~> e'' ⇐ t ] aasubmin-ana d'
    min-ana (AASubsume {Γ = Γ} x x₁ (SAMove x₂) x₃) = _ , AAMove x₂ , <>
    min-ana (AASubsume x x₁ SADel x₃) = _ , AADel , <>
    min-ana (AASubsume {Γ = Γ}  {t = t} {t' = t'}  x x₁ SAConAsc x₃) = _ , AAConAsc {Γ = Γ} {t = t} , <>
    min-ana (AASubsume x x₁ (SAConVar p) x₃) = _ , AASubsume x x₁ (SAConVar p) x₃ , <>
    min-ana (AASubsume EETop SEHole (SAConLam x₃) TCRefl)        = _ , AAConLam1 x₃ MAArr , <>
    min-ana (AASubsume EETop SEHole (SAConLam x₃) TCHole2)       = _ , AAConLam1 x₃ MAHole , <>
    min-ana (AASubsume EETop SEHole (SAConLam x₃) (TCArr x₄ x₅)) = _ , AAConLam1 x₃ MAArr , <>
    min-ana (AASubsume x x₁ (SAConApArr x₂) x₃) = _ , AASubsume x x₁ (SAConApArr x₂) x₃ , <>
    min-ana (AASubsume x x₁ (SAConApOtw x₂) x₃) = _ , AASubsume x x₁ (SAConApOtw x₂) x₃ , <>
    min-ana (AASubsume x x₁ SAConNumlit x₃) = _ , AASubsume x x₁ SAConNumlit x₃ , <>
    min-ana (AASubsume x x₁ (SAConPlus1 x₂) x₃) = _ , AASubsume x x₁ (SAConPlus1 x₂) x₃ , <>
    min-ana (AASubsume x x₁ (SAConPlus2 x₂) x₃) = _ , AASubsume x x₁ (SAConPlus2 x₂) x₃ , <>
    min-ana (AASubsume x x₁ SAConNEHole x₃) = _ , AASubsume x x₁ SAConNEHole x₃ , <>
    min-ana (AASubsume x x₁ (SAFinish x₂) x₃) = _ ,  AASubsume x x₁ (SAFinish x₂) x₃ , <>
    min-ana (AASubsume x x₁ (SAZipAsc2 x₂ x₃ x₄ x₅) x₆) = _ , AASubsume x x₁ (SAZipAsc2 x₂ x₃ x₄ x₅) x₆ , <>
    min-ana (AASubsume x x₁ (SAZipAsc1 x₂) x₃) with min-ana x₂
    ... | a , b , c = _ , AASubsume x x₁ (SAZipAsc1 b) x₃ , c
    min-ana (AASubsume x x₁ (SAZipApArr x₂ x₃ x₄ x₅ x₆) x₇) with min-synth x₅
    ... | a , b , c = _ , AASubsume x x₁ (SAZipApArr x₂ x₃ x₄ b x₆) x₇ , c
    min-ana (AASubsume x x₁ (SAZipApAna x₂ x₃ x₄) x₅) with min-ana x₄
    ... | a , b , c = _ , AASubsume x x₁ (SAZipApAna x₂ x₃ b) x₅ , c
    min-ana (AASubsume x x₁ (SAZipPlus1 x₂) x₃) with min-ana x₂
    ... | a , b , c = _ , AASubsume x x₁ (SAZipPlus1 b) x₃ , c
    min-ana (AASubsume x x₁ (SAZipPlus2 x₂) x₃) with min-ana x₂
    ... | a , b , c = _ , AASubsume x x₁ (SAZipPlus2 b) x₃ , c
    min-ana (AASubsume x x₁ (SAZipHole x₂ x₃ x₄) x₅) with min-synth x₄
    ... | a , b , c = _ , AASubsume x x₁ (SAZipHole x₂ x₃ b) x₅ , c
    min-ana (AAMove x) = _ , AAMove x , <>
    min-ana AADel = _ , AADel , <>
    min-ana AAConAsc = _ , AAConAsc , <>
    min-ana (AAConVar x₁ p) = _ , AAConVar x₁ p , <>
    min-ana (AAConLam1 x₁ x₂) = _ , AAConLam1 x₁ x₂ , <>
    min-ana (AAConLam2 x₁ x₂) = _ , AAConLam2 x₁ x₂ , <>
    min-ana (AAConNumlit x) = _ , AAConNumlit x , <>
    min-ana (AAFinish x) = _ , AAFinish x , <>
    min-ana (AAZipLam x₁ x₂ d) with min-ana d
    ... | a , b , c = _ , AAZipLam x₁ x₂ b , c

  -- these theorems argue that if a derivation is already subsumption
  -- minimal than the minimzer does not change the resultant
  -- expression--that it's conservative in this sense. they do not argue
  -- that the derivation that's computer is itself the same as the input
  -- derivation.
  mutual
    min-fixed-synth : ∀ {Γ e t α e' t'} →
                         (d : Γ ⊢ e => t ~ α ~> e' => t') →
                         aasubmin-synth d →
                         e' == π1 (min-synth d)
    min-fixed-synth (SAMove x) min = refl
    min-fixed-synth SADel min = refl
    min-fixed-synth SAConAsc min = refl
    min-fixed-synth (SAConVar p) min = refl
    min-fixed-synth (SAConLam x₁) min = refl
    min-fixed-synth (SAConApArr x) min = refl
    min-fixed-synth (SAConApOtw x) min = refl
    min-fixed-synth SAConNumlit min = refl
    min-fixed-synth (SAConPlus1 x) min = refl
    min-fixed-synth (SAConPlus2 x) min = refl
    min-fixed-synth SAConNEHole min = refl
    min-fixed-synth (SAFinish x) min = refl
    min-fixed-synth (SAZipAsc1 x) min with min-fixed-ana x min
    ... | qq with min-ana x
    ... | (e'' , d' , min') = ap1 (λ q → q ·:₁ _) qq
    min-fixed-synth (SAZipAsc2 x x₁ x₂ x₃) min = refl
    min-fixed-synth (SAZipApArr x x₁ x₂ d x₃) min with min-fixed-synth d min
    ... | qq with min-synth d
    ... | (e'' , d' , min') = ap1 (λ q → q ∘₁ _) qq
    min-fixed-synth (SAZipApAna x x₁ x₂) min with min-fixed-ana x₂ min
    ... | qq with min-ana x₂
    ... | (e'' , _ , _) = ap1 (λ q → _ ∘₂ q) qq
    min-fixed-synth (SAZipPlus1 x) min with min-fixed-ana x min
    ... | qq with min-ana x
    ... | (e'' , _ , _) = ap1 (λ q → q ·+₁ _) qq
    min-fixed-synth (SAZipPlus2 x) min with min-fixed-ana x min
    ... | qq with min-ana x
    ... | (e'' , _ , _) = ap1 (λ q → _ ·+₂ q) qq
    min-fixed-synth (SAZipHole x x₁ d) min with min-fixed-synth d min
    ... | qq with min-synth d
    ... | (e'' , _ , _) = ap1 ⦇⌜_⌟⦈ qq

    min-fixed-ana : ∀ {Γ e t α e' } →
                         (d : Γ ⊢ e ~ α ~> e' ⇐ t) →
                         aasubmin-ana d →
                         e' == π1 (min-ana d)
    min-fixed-ana (AASubsume x x₁ (SAMove x₂) x₃) min = refl
    min-fixed-ana (AASubsume x x₁ SADel x₃) min = refl
    min-fixed-ana (AASubsume x x₁ SAConAsc x₃) min = abort min
    min-fixed-ana (AASubsume x₁ x₂ (SAConVar p) x₃) min = refl
    min-fixed-ana (AASubsume x₁ x₂ (SAConLam x₃) x₄) min = abort min
    min-fixed-ana (AASubsume x x₁ (SAConApArr x₂) x₃) min = refl
    min-fixed-ana (AASubsume x x₁ (SAConApOtw x₂) x₃) min = refl
    min-fixed-ana (AASubsume x x₁ SAConNumlit x₃) min = refl
    min-fixed-ana (AASubsume x x₁ (SAConPlus1 x₂) x₃) min = refl
    min-fixed-ana (AASubsume x x₁ (SAConPlus2 x₂) x₃) min = refl
    min-fixed-ana (AASubsume x x₁ SAConNEHole x₃) min = refl
    min-fixed-ana (AASubsume x x₁ (SAFinish x₂) x₃) min = refl
    min-fixed-ana (AASubsume x x₁ (SAZipAsc1 x₂) x₃) min with min-fixed-ana x₂ min
    ... | qq with min-ana x₂
    ... | (e'' , _ , _) = ap1 (λ q → q ·:₁ _) qq
    min-fixed-ana (AASubsume x x₁ (SAZipAsc2 x₂ x₃ x₄ x₅) x₆) min = refl
    min-fixed-ana (AASubsume x x₁ (SAZipApArr x₂ x₃ x₄ x₅ x₆) x₇) min with min-fixed-synth x₅ min
    ... | qq with min-synth x₅
    ... | (e'' , d' , min') = ap1 (λ q → q ∘₁ _) qq
    min-fixed-ana (AASubsume x x₁ (SAZipApAna x₂ x₃ x₄) x₅) min with min-fixed-ana x₄ min
    ... | qq with min-ana x₄
    ... | (e'' , _ , _) = ap1 (λ q → _ ∘₂ q) qq
    min-fixed-ana (AASubsume x x₁ (SAZipPlus1 x₂) x₃) min with min-fixed-ana x₂ min
    ... | qq with min-ana x₂
    ... | (e'' , _ , _) = ap1 (λ q → q ·+₁ _) qq
    min-fixed-ana (AASubsume x x₁ (SAZipPlus2 x₂) x₃) min with min-fixed-ana x₂ min
    ... | qq with min-ana x₂
    ... | (e'' , _ , _) = ap1 (λ q → _ ·+₂ q) qq
    min-fixed-ana (AASubsume x x₁ (SAZipHole x₂ x₃ x₄) x₅) min with min-fixed-synth x₄ min
    ... | qq with min-synth x₄
    ... | (e'' , _ , _) = ap1 ⦇⌜_⌟⦈ qq
    min-fixed-ana (AAMove x) min = refl
    min-fixed-ana AADel min = refl
    min-fixed-ana AAConAsc min = refl
    min-fixed-ana (AAConVar x₁ p) min = refl
    min-fixed-ana (AAConLam1 x₁ x₂) min = refl
    min-fixed-ana (AAConLam2 x₁ x₂) min = refl
    min-fixed-ana (AAConNumlit x) min = refl
    min-fixed-ana (AAFinish x) min = refl
    min-fixed-ana (AAZipLam x₁ x₂ d) min with min-fixed-ana d min
    ... | qq with min-ana d
    ... | (e'' , _ , _) = ap1 (λ q → ·λ _ q) qq


text:
module Basic.Compiler.Test where

open import Basic.AST
open import Basic.Compiler.Code
open import Basic.Compiler.Machine
open import Basic.BigStep

open import Data.Fin
open import Data.Nat
open import Data.Vec
open import Data.Product
open import Data.Bool
open import Data.List

open Basic.BigStep.Fac

{- Just a sandbox for testing the interpreters in Compiler.Machine -}

fac' : Code 3
fac' = 𝓒⟦ fac ⟧ˢ

test = trace fac' [] (1 ∷ 0 ∷ 0 ∷ []) 1000

-- normal form of "test"

-- (PUSH 0 ∷
--  STORE (suc zero) ∷
--  PUSH 1 ∷
--  STORE (suc (suc zero)) ∷
--  LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--  ∷ []
--  , [] , 1 ∷ 0 ∷ 0 ∷ [])
-- ∷
-- (STORE (suc zero) ∷
--  PUSH 1 ∷
--  STORE (suc (suc zero)) ∷
--  LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--  ∷ []
--  , nat 0 ∷ [] , 1 ∷ 0 ∷ 0 ∷ [])
-- ∷
-- (PUSH 1 ∷
--  STORE (suc (suc zero)) ∷
--  LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--  ∷ []
--  , [] , 1 ∷ 0 ∷ 0 ∷ [])
-- ∷
-- (STORE (suc (suc zero)) ∷
--  LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--  ∷ []
--  , nat 1 ∷ [] , 1 ∷ 0 ∷ 0 ∷ [])
-- ∷
-- (LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--  ∷ []
--  , [] , 1 ∷ 0 ∷ 1 ∷ [])
-- ∷
-- (FETCH zero ∷
--  FETCH (suc zero) ∷
--  LT ∷
--  BRANCH
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷
--   MUL ∷
--   STORE (suc (suc zero)) ∷
--   LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--   (FETCH (suc zero) ∷
--    PUSH 1 ∷
--    ADD ∷
--    STORE (suc zero) ∷
--    FETCH (suc (suc zero)) ∷
--    FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--   ∷ [])
--  (NOOP ∷ [])
--  ∷ []
--  , [] , 1 ∷ 0 ∷ 1 ∷ [])
-- ∷
-- (FETCH (suc zero) ∷
--  LT ∷
--  BRANCH
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷
--   MUL ∷
--   STORE (suc (suc zero)) ∷
--   LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--   (FETCH (suc zero) ∷
--    PUSH 1 ∷
--    ADD ∷
--    STORE (suc zero) ∷
--    FETCH (suc (suc zero)) ∷
--    FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--   ∷ [])
--  (NOOP ∷ [])
--  ∷ []
--  , nat 1 ∷ [] , 1 ∷ 0 ∷ 1 ∷ [])
-- ∷
-- (LT ∷
--  BRANCH
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷
--   MUL ∷
--   STORE (suc (suc zero)) ∷
--   LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--   (FETCH (suc zero) ∷
--    PUSH 1 ∷
--    ADD ∷
--    STORE (suc zero) ∷
--    FETCH (suc (suc zero)) ∷
--    FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--   ∷ [])
--  (NOOP ∷ [])
--  ∷ []
--  , nat 0 ∷ nat 1 ∷ [] , 1 ∷ 0 ∷ 1 ∷ [])
-- ∷
-- (BRANCH
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷
--   MUL ∷
--   STORE (suc (suc zero)) ∷
--   LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--   (FETCH (suc zero) ∷
--    PUSH 1 ∷
--    ADD ∷
--    STORE (suc zero) ∷
--    FETCH (suc (suc zero)) ∷
--    FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--   ∷ [])
--  (NOOP ∷ [])
--  ∷ []
--  , bool true ∷ [] , 1 ∷ 0 ∷ 1 ∷ [])
-- ∷
-- (FETCH (suc zero) ∷
--  PUSH 1 ∷
--  ADD ∷
--  STORE (suc zero) ∷
--  FETCH (suc (suc zero)) ∷
--  FETCH (suc zero) ∷
--  MUL ∷
--  STORE (suc (suc zero)) ∷
--  LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--  ∷ []
--  , [] , 1 ∷ 0 ∷ 1 ∷ [])
-- ∷
-- (PUSH 1 ∷
--  ADD ∷
--  STORE (suc zero) ∷
--  FETCH (suc (suc zero)) ∷
--  FETCH (suc zero) ∷
--  MUL ∷
--  STORE (suc (suc zero)) ∷
--  LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--  ∷ []
--  , nat 0 ∷ [] , 1 ∷ 0 ∷ 1 ∷ [])
-- ∷
-- (ADD ∷
--  STORE (suc zero) ∷
--  FETCH (suc (suc zero)) ∷
--  FETCH (suc zero) ∷
--  MUL ∷
--  STORE (suc (suc zero)) ∷
--  LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--  ∷ []
--  , nat 1 ∷ nat 0 ∷ [] , 1 ∷ 0 ∷ 1 ∷ [])
-- ∷
-- (STORE (suc zero) ∷
--  FETCH (suc (suc zero)) ∷
--  FETCH (suc zero) ∷
--  MUL ∷
--  STORE (suc (suc zero)) ∷
--  LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--  ∷ []
--  , nat 1 ∷ [] , 1 ∷ 0 ∷ 1 ∷ [])
-- ∷
-- (FETCH (suc (suc zero)) ∷
--  FETCH (suc zero) ∷
--  MUL ∷
--  STORE (suc (suc zero)) ∷
--  LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--  ∷ []
--  , [] , 1 ∷ 1 ∷ 1 ∷ [])
-- ∷
-- (FETCH (suc zero) ∷
--  MUL ∷
--  STORE (suc (suc zero)) ∷
--  LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--  ∷ []
--  , nat 1 ∷ [] , 1 ∷ 1 ∷ 1 ∷ [])
-- ∷
-- (MUL ∷
--  STORE (suc (suc zero)) ∷
--  LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--  ∷ []
--  , nat 1 ∷ nat 1 ∷ [] , 1 ∷ 1 ∷ 1 ∷ [])
-- ∷
-- (STORE (suc (suc zero)) ∷
--  LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--  ∷ []
--  , nat 1 ∷ [] , 1 ∷ 1 ∷ 1 ∷ [])
-- ∷
-- (LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--  ∷ []
--  , [] , 1 ∷ 1 ∷ 1 ∷ [])
-- ∷
-- (FETCH zero ∷
--  FETCH (suc zero) ∷
--  LT ∷
--  BRANCH
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷
--   MUL ∷
--   STORE (suc (suc zero)) ∷
--   LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--   (FETCH (suc zero) ∷
--    PUSH 1 ∷
--    ADD ∷
--    STORE (suc zero) ∷
--    FETCH (suc (suc zero)) ∷
--    FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--   ∷ [])
--  (NOOP ∷ [])
--  ∷ []
--  , [] , 1 ∷ 1 ∷ 1 ∷ [])
-- ∷
-- (FETCH (suc zero) ∷
--  LT ∷
--  BRANCH
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷
--   MUL ∷
--   STORE (suc (suc zero)) ∷
--   LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--   (FETCH (suc zero) ∷
--    PUSH 1 ∷
--    ADD ∷
--    STORE (suc zero) ∷
--    FETCH (suc (suc zero)) ∷
--    FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--   ∷ [])
--  (NOOP ∷ [])
--  ∷ []
--  , nat 1 ∷ [] , 1 ∷ 1 ∷ 1 ∷ [])
-- ∷
-- (LT ∷
--  BRANCH
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷
--   MUL ∷
--   STORE (suc (suc zero)) ∷
--   LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--   (FETCH (suc zero) ∷
--    PUSH 1 ∷
--    ADD ∷
--    STORE (suc zero) ∷
--    FETCH (suc (suc zero)) ∷
--    FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--   ∷ [])
--  (NOOP ∷ [])
--  ∷ []
--  , nat 1 ∷ nat 1 ∷ [] , 1 ∷ 1 ∷ 1 ∷ [])
-- ∷
-- (BRANCH
--  (FETCH (suc zero) ∷
--   PUSH 1 ∷
--   ADD ∷
--   STORE (suc zero) ∷
--   FETCH (suc (suc zero)) ∷
--   FETCH (suc zero) ∷
--   MUL ∷
--   STORE (suc (suc zero)) ∷
--   LOOP (FETCH zero ∷ FETCH (suc zero) ∷ LT ∷ [])
--   (FETCH (suc zero) ∷
--    PUSH 1 ∷
--    ADD ∷
--    STORE (suc zero) ∷
--    FETCH (suc (suc zero)) ∷
--    FETCH (suc zero) ∷ MUL ∷ STORE (suc (suc zero)) ∷ [])
--   ∷ [])
--  (NOOP ∷ [])
--  ∷ []
--  , bool false ∷ [] , 1 ∷ 1 ∷ 1 ∷ [])
-- ∷
-- (NOOP ∷ [] , [] , 1 ∷ 1 ∷ 1 ∷ []) ∷ ([] , [] , 1 ∷ 1 ∷ 1 ∷ []) ∷ []

max_stars_repo_name: AndrasKovacs/SemanticsWithApplications

max_issues_repo_name: AndrasKovacs/SemanticsWithApplications

max_forks_repo_name: AndrasKovacs/SemanticsWithApplications


text:
module List.Permutation.Base.Preorder (A : Set) where

open import List.Permutation.Base A
open import List.Permutation.Base.Equivalence A
open import Data.List
open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding ([_])

∼-preorder : Preorder _ _ _
∼-preorder =  record {
                Carrier = List A;
                _≈_ = _≡_;
                _∼_ = _∼_;
                isPreorder =  record {
                                  isEquivalence = Relation.Binary.Setoid.isEquivalence (setoid (List A)) ;
                                  reflexive = reflexive-aux;
                                  trans = trans∼
                               }
                }
           where
             reflexive-aux : {i j : List A} → i ≡ j → i ∼ j
             reflexive-aux {i = i} {j = .i} refl = refl∼


text:
-- div shouldn't termination check, but it also shouldn't make the termination
-- checker loop.
module Issue503 where

data Bool : Set where
  true : Bool
  false : Bool

if_then_else_ : {C : Set} -> Bool -> C -> C -> C
if true then a else b = a
if false then a else b = b

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

pred : Nat -> Nat
pred zero = zero
pred (succ n) = n

_+_ : Nat -> Nat -> Nat
zero + b = b
succ a + b = succ (a + b)

_*_ : Nat -> Nat -> Nat
zero * _ = zero
succ a * b = (a * b) + b

{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC succ #-}
{-# BUILTIN NATPLUS _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}

_-_ : Nat -> Nat -> Nat
a - zero = a
a - succ b = pred (a - b)

_<_ : Nat -> Nat -> Bool
a < zero = false
zero < succ b = true
succ a < succ b = a < b

div : Nat -> Nat -> Nat
div m n = if (m < n) then zero else succ (div (m - n) n)

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module rewriting where

open import lib

open import cedille-types
open import conversion
open import ctxt
open import general-util
open import is-free
open import lift
open import rename
open import subst
open import syntax-util

private

  mk-phi : var → (eq t t' : term) → term
  mk-phi x eq t t' =
    Phi posinfo-gen
      (Rho posinfo-gen RhoPlain NoNums eq
        (Guide posinfo-gen x (TpEq posinfo-gen t t' posinfo-gen))
        (Beta posinfo-gen (SomeTerm t posinfo-gen) (SomeTerm id-term posinfo-gen)))
      t t' posinfo-gen

  head-types-match : ctxt → trie term → (complete partial : type) → 𝔹
  head-types-match Γ σ (TpApp T _) (TpApp T' _) = conv-type Γ T (substs Γ σ T')
  head-types-match Γ σ (TpAppt T _) (TpAppt T' _) = conv-type Γ T (substs Γ σ T')
  head-types-match Γ σ T T' = tt

rewrite-t : Set → Set
rewrite-t T = ctxt → (is-plus : 𝔹) → (nums : maybe stringset) →
              (eq left : term) → (right : var) → (total-matches : ℕ) →
              T {- Returned value -} ×
              ℕ {- Number of rewrites actually performed -} ×
              ℕ {- Total number of matches, including skipped ones -}

infixl 4 _≫rewrite_

_≫rewrite_ : ∀ {A B : Set} → rewrite-t (A → B) → rewrite-t A → rewrite-t B
(f ≫rewrite a) Γ op on eq t₁ t₂ n with f Γ op on eq t₁ t₂ n
...| f' , n' , sn with a Γ op on eq t₁ t₂ sn
...| b , n'' , sn' = f' b , n' + n'' , sn'

rewriteR : ∀ {A : Set} → A → rewrite-t A
rewriteR a Γ op on eq t₁ t₂ n = a , 0 , n

{-# TERMINATING #-}
rewrite-term        : term        → rewrite-t term
rewrite-terma       : term        → rewrite-t term
rewrite-termh       : term        → rewrite-t term
rewrite-type        : type        → rewrite-t type
rewrite-typeh       : type        → rewrite-t type
rewrite-kind        : kind        → rewrite-t kind
rewrite-tk          : tk          → rewrite-t tk
rewrite-liftingType : liftingType → rewrite-t liftingType

rewrite-rename-var : ∀ {A} → var → (var → rewrite-t A) → rewrite-t A
rewrite-rename-var x r Γ op on eq t₁ t₂ n =
  let x' = rename-var-if Γ (renamectxt-insert empty-renamectxt t₂ t₂) x t₁ in
  r x' Γ op on eq t₁ t₂ n

rewrite-abs : ∀ {ed} → var → var → (⟦ ed ⟧ → rewrite-t ⟦ ed ⟧) → ⟦ ed ⟧ → rewrite-t ⟦ ed ⟧
rewrite-abs x x' g a Γ = let Γ = ctxt-var-decl x' Γ in g (rename-var Γ x x' a) Γ

rewrite-term t Γ op on eq t₁ t₂ sn =
  case rewrite-terma (erase-term t) Γ op on eq t₁ t₂ sn of λ where
    (t' , 0 , sn') → t , 0 , sn'
    (t' , n , sn') → mk-phi t₂ eq t t' , n , sn'

rewrite-terma t Γ op on eq t₁ t₂ sn =
  case conv-term Γ t₁ t of λ where
  tt → case on of λ where
    (just ns) → case trie-contains ns (ℕ-to-string (suc sn)) of λ where
      tt → Var posinfo-gen t₂ , 1 , suc sn -- ρ nums contains n
      ff → t , 0 , suc sn -- ρ nums does not contain n
    nothing → Var posinfo-gen t₂ , 1 , suc sn
  ff → case op of λ where
    tt → case rewrite-termh (hnf Γ unfold-head t tt) Γ op on eq t₁ t₂ sn of λ where
      (t' , 0 , sn') → t , 0 , sn' -- if no rewrites were performed, return the pre-hnf t
      (t' , n' , sn') → t' , n' , sn'
    ff → rewrite-termh t Γ op on eq t₁ t₂ sn

rewrite-termh (App t e t') =
  rewriteR App ≫rewrite rewrite-terma t ≫rewrite rewriteR e ≫rewrite rewrite-terma t'
rewrite-termh (Lam pi NotErased pi' y NoClass t) =
  rewrite-rename-var y λ y' → rewriteR (Lam pi NotErased pi' y' NoClass) ≫rewrite
  rewrite-abs y y' rewrite-terma t
rewrite-termh (Var pi x) = rewriteR (Var pi x)
rewrite-termh = rewriteR

rewrite-type T Γ tt on eq t₁ t₂ sn
  with rewrite-typeh (hnf Γ unfold-head-no-lift T tt) Γ tt on eq t₁ t₂ sn
...| T' , 0 , sn' = T  , 0 , sn'
...| T' , n , sn' = T' , n , sn'
rewrite-type = rewrite-typeh

rewrite-typeh (Abs pi b pi' x atk T) =
  rewrite-rename-var x λ x' →
  rewriteR (Abs pi b pi' x') ≫rewrite rewrite-tk atk ≫rewrite
  rewrite-abs x x' rewrite-type T
rewrite-typeh (Iota pi pi' x T T') =
  rewrite-rename-var x λ x' →
  rewriteR (Iota pi pi' x') ≫rewrite rewrite-type T ≫rewrite
  rewrite-abs x x' rewrite-type T'
rewrite-typeh (Lft pi pi' x t l) =
  rewrite-rename-var x λ x' →
  rewriteR (Lft pi pi' x') ≫rewrite
  rewrite-abs x x' rewrite-term t ≫rewrite
  rewrite-liftingType l
rewrite-typeh (TpApp T T') =
  rewriteR TpApp ≫rewrite rewrite-typeh T ≫rewrite rewrite-type T'
rewrite-typeh (TpAppt T t) =
  rewriteR TpAppt ≫rewrite rewrite-typeh T ≫rewrite rewrite-term t
rewrite-typeh (TpEq pi t₁ t₂ pi') =
  rewriteR (TpEq pi) ≫rewrite rewrite-term t₁ ≫rewrite
  rewrite-term t₂ ≫rewrite rewriteR pi'
rewrite-typeh (TpLambda pi pi' x atk T) =
  rewrite-rename-var x λ x' →
  rewriteR (TpLambda pi pi' x') ≫rewrite rewrite-tk atk ≫rewrite
  rewrite-abs x x' rewrite-type T
rewrite-typeh (TpArrow T a T') =
  rewriteR TpArrow ≫rewrite rewrite-type T ≫rewrite rewriteR a ≫rewrite rewrite-type T'
rewrite-typeh (TpLet pi (DefTerm pi' x T t) T') Γ =
  rewrite-type (subst Γ (Chi posinfo-gen T t) x T') Γ
rewrite-typeh (TpLet pi (DefType pi' x k T) T') Γ =
  rewrite-type (subst Γ T x T') Γ
rewrite-typeh (TpParens _ T _) = rewrite-type T
rewrite-typeh (NoSpans T _) = rewrite-type T
rewrite-typeh (TpHole pi) = rewriteR (TpHole pi)
rewrite-typeh (TpVar pi x) = rewriteR (TpVar pi x)

-- If we ever implement kind-level rewriting, we will need to go through
-- all the types of kind pi binding a term or type-to-kind arrow
-- if the right-hand side variable is free in the types of the bound variable,
-- and substitute each occurence of the term variable (eta-expanding if necessary)
-- in the body of the type with itself surrounded by a rewrite back the original
-- expected type (unless we lifted a term, then it gets really tricky because
-- we may not want to rewrite back?).
rewrite-kind = rewriteR
rewrite-liftingType = rewriteR

rewrite-tk (Tkt T) = rewriteR Tkt ≫rewrite rewrite-type T
rewrite-tk (Tkk k) = rewriteR Tkk ≫rewrite rewrite-kind k

post-rewriteh : ctxt → var → term → (ctxt → var → term → tk → tk) → (var → tk → ctxt → ctxt) → type → type × kind

post-rewriteh Γ x eq prtk tk-decl (Abs pi b pi' x' atk T) =
  let atk' = prtk Γ x eq atk in
  Abs pi b pi' x' atk' (fst (post-rewriteh (tk-decl x' atk' Γ) x eq prtk tk-decl T)) , star
post-rewriteh Γ x eq prtk tk-decl (Iota pi pi' x' T T') =
  let T = fst (post-rewriteh Γ x eq prtk tk-decl T) in
  Iota pi pi' x' T (fst (post-rewriteh (tk-decl x' (Tkt T) Γ) x eq prtk tk-decl T')) , star
post-rewriteh Γ x eq prtk tk-decl (Lft pi pi' x' t lT) =
  Lft pi pi' x' t lT , liftingType-to-kind lT
post-rewriteh Γ x eq prtk tk-decl (TpApp T T') =
  flip uncurry (post-rewriteh Γ x eq prtk tk-decl T') λ T' k' →
  flip uncurry (post-rewriteh Γ x eq prtk tk-decl T) λ where
    T (KndPi pi pi' x' atk k) → TpApp T T' , hnf Γ unfold-head-no-lift (subst Γ T' x' k) tt
    T (KndArrow k k'') → TpApp T T' , hnf Γ unfold-head-no-lift k'' tt
    T k → TpApp T T' , k
post-rewriteh Γ x eq prtk tk-decl (TpAppt T t) =
  let t2 T' = if is-free-in check-erased x T' then Rho posinfo-gen RhoPlain NoNums eq (Guide posinfo-gen x T') t else t in
  flip uncurry (post-rewriteh Γ x eq prtk tk-decl T) λ where
    T (KndPi pi pi' x' (Tkt T') k) →
      let t3 = t2 T' in TpAppt T t3 , hnf Γ unfold-head-no-lift (subst Γ t3 x' k) tt
    T (KndTpArrow T' k) → TpAppt T (t2 T') , hnf Γ unfold-head-no-lift k tt
    T k → TpAppt T t , k
post-rewriteh Γ x eq prtk tk-decl (TpArrow T a T') = TpArrow (fst (post-rewriteh Γ x eq prtk tk-decl T)) a (fst (post-rewriteh Γ x eq prtk tk-decl T')) , star
post-rewriteh Γ x eq prtk tk-decl (TpLambda pi pi' x' atk T) =
  let atk' = prtk Γ x eq atk in
  flip uncurry (post-rewriteh (tk-decl x' atk' Γ) x eq prtk tk-decl T) λ T k →
  TpLambda pi pi' x' atk' T , KndPi pi pi' x' atk' k
post-rewriteh Γ x eq prtk tk-decl (TpParens pi T pi') = post-rewriteh Γ x eq prtk tk-decl T
post-rewriteh Γ x eq prtk tk-decl (TpVar pi x') with env-lookup Γ x'
...| just (type-decl k , _) = mtpvar x' , hnf Γ unfold-head-no-lift k tt
...| just (type-def nothing _ T k , _) = mtpvar x' , hnf Γ unfold-head-no-lift k tt
...| just (type-def (just ps) _ T k , _) = mtpvar x' , abs-expand-kind ps (hnf Γ unfold-head-no-lift k tt)
...| _ = mtpvar x' , star
post-rewriteh Γ x eq prtk tk-decl T = T , star

{-# TERMINATING #-}
post-rewrite : ctxt → var → (eq t₂ : term) → type → type
post-rewrite Γ x eq t₂ T = subst Γ t₂ x (fst (post-rewriteh Γ x eq prtk tk-decl T)) where
  prtk : ctxt → var → term → tk → tk
  tk-decl : var → tk → ctxt → ctxt
  prtk Γ x t (Tkt T) = Tkt (fst (post-rewriteh Γ x t prtk tk-decl T))
  prtk Γ x t (Tkk k) = Tkk (hnf Γ unfold-head-no-lift k tt)
  tk-decl x atk (mk-ctxt mod ss is os d) =
    mk-ctxt mod ss (trie-insert is x (h atk , "" , "")) os d where
    h : tk → ctxt-info
    h (Tkt T) = term-decl T
    h (Tkk k) = type-decl k

-- Functions for substituting the type T in ρ e @ x . T - t
{-# TERMINATING #-}
rewrite-at : ctxt → var → term → 𝔹 → type → type → type
rewrite-ath : ctxt → var → term → 𝔹 → type → type → type
rewrite-at-tk : ctxt → var → term → 𝔹 → tk → tk → tk

rewrite-at-tk Γ x eq b (Tkt T) (Tkt T') = Tkt (rewrite-at Γ x eq b T T')
rewrite-at-tk Γ x eq b atk atk' = atk

rewrite-at Γ x eq b T T' =
  if ~ is-free-in tt x T'
    then T
    else if b && ~ head-types-match Γ (trie-single x (Hole posinfo-gen)) T T'
      then rewrite-ath Γ x eq ff (hnf Γ unfold-head-no-lift T tt) (hnf Γ unfold-head-no-lift T' tt)
      else rewrite-ath Γ x eq b T T'

rewrite-ath Γ x eq b (Abs pi1 b1 pi1' x1 atk1 T1) (Abs pi2 b2 pi2' x2 atk2 T2) =
  Abs pi1 b1 pi1' x1 (rewrite-at-tk Γ x eq tt atk1 atk2) (rewrite-at (ctxt-var-decl x1 Γ) x eq b T1 (rename-var Γ x2 x1 T2))
rewrite-ath Γ x eq b (Iota pi1 pi1' x1 T1 T1') (Iota pi2 pi2' x2 T2 T2') =
  Iota pi1 pi1' x1 (rewrite-at Γ x eq tt T1 T2) (rewrite-at (ctxt-var-decl x1 Γ) x eq b T1' (rename-var Γ x2 x1 T2'))
rewrite-ath Γ x eq b (Lft pi1 pi1' x1 t1 lT1) (Lft pi2 pi2' x2 t2 lT2) =
  Lft pi1 pi1' x1 (if is-free-in tt x (mlam x2 t2) then mk-phi x eq t1 t2 else t1) lT1
rewrite-ath Γ x eq b (TpApp T1 T1') (TpApp T2 T2') =
  TpApp (rewrite-at Γ x eq b T1 T2) (rewrite-at Γ x eq b T1' T2')
rewrite-ath Γ x eq b (TpAppt T1 t1) (TpAppt T2 t2) =
  TpAppt (rewrite-at Γ x eq b T1 T2) (if is-free-in tt x t2 then mk-phi x eq t1 t2 else t1)
rewrite-ath Γ x eq b (TpArrow T1 a1 T1') (TpArrow T2 a2 T2') =
  TpArrow (rewrite-at Γ x eq tt T1 T2) a1 (rewrite-at Γ x eq tt T1' T2')
rewrite-ath Γ x eq b (TpEq pi1 t1 t1' pi1') (TpEq pi2 t2 t2' pi2') =
  TpEq pi1 t2 t2' pi1'
rewrite-ath Γ x eq b (TpLambda pi1 pi1' x1 atk1 T1) (TpLambda pi2 pi2' x2 atk2 T2) =
  TpLambda pi1 pi1' x1 (rewrite-at-tk Γ x eq tt atk1 atk2) (rewrite-at (ctxt-var-decl x1 Γ) x eq b T1 (rename-var Γ x2 x1 T2))
rewrite-ath Γ x eq b (TpLet pi1 (DefTerm pi1' x1 oc1 t1) T1) T2 = rewrite-at Γ x eq b (subst Γ t1 x1 T1) T2
rewrite-ath Γ x eq b T1 (TpLet pi2 (DefTerm pi2' x2 oc2 t2) T2) = rewrite-at Γ x eq b T1 (subst Γ t2 x2 T2)
rewrite-ath Γ x eq b (TpLet pi1 (DefType pi1' x1 k1 T1ₗ) T1) T2 = rewrite-at Γ x eq b (subst Γ T1ₗ x1 T1) T2
rewrite-ath Γ x eq b T1 (TpLet pi2 (DefType pi2' x2 k2 T2ₗ) T2) = rewrite-at Γ x eq b T1 (subst Γ T2ₗ x2 T2)
rewrite-ath Γ x eq b (TpVar pi1 x1) (TpVar pi2 x2) = TpVar pi1 x1
rewrite-ath Γ x eq b (TpHole pi1) (TpHole pi2) = TpHole pi1
rewrite-ath Γ x eq b (TpParens pi1 T1 pi1') T2 = rewrite-at Γ x eq b T1 T2
rewrite-ath Γ x eq b T1 (TpParens pi2 T2 pi2') = rewrite-at Γ x eq b T1 T2
rewrite-ath Γ x eq b (NoSpans T1 pi1) T2 = rewrite-at Γ x eq b T1 T2
rewrite-ath Γ x eq b T1 (NoSpans T2 pi2) = rewrite-at Γ x eq b T1 T2
rewrite-ath Γ x eq tt T1 T2 = rewrite-at Γ x eq ff (hnf Γ unfold-head-no-lift T1 tt) (hnf Γ unfold-head-no-lift T2 tt)
rewrite-ath Γ x eq ff T1 T2 = T1

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


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

module Lens.Pair where

open import Prelude
open import Lens.Definition

⦅fst⦆ : Lens (A × B) A
⦅fst⦆ .fst (x , y) = lens-part x (_, y)
⦅fst⦆ .snd .get-set s v i = v
⦅fst⦆ .snd .set-get s i = s
⦅fst⦆ .snd .set-set s v₁ v₂ i = v₂ , s .snd

⦅snd⦆ : Lens (A × B) B
⦅snd⦆ .fst (x , y) = lens-part y (x ,_)
⦅snd⦆ .snd .get-set s v i = v
⦅snd⦆ .snd .set-get s i = s
⦅snd⦆ .snd .set-set s v₁ v₂ i = s .fst , v₂

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Instance.Rels where

open import Data.Product
open import Function hiding (_⇔_)
open import Level
open import Relation.Binary
open import Relation.Binary.Construct.Composition
open import Relation.Binary.PropositionalEquality

open import Categories.Category.Core

-- the category whose objects are sets and whose morphisms are binary relations.
Rels : ∀ o ℓ → Category (suc o) (suc (o ⊔ ℓ)) (o ⊔ ℓ)
Rels o ℓ = record
  { Obj = Set o
  ; _⇒_ = λ A B → REL A B (o ⊔ ℓ)
  ; _≈_ = λ L R → L ⇔ R
  ; id = λ x y → Lift ℓ (x ≡ y)
  ; _∘_ = λ L R → R ; L
  ; assoc = (λ { (b , fxb , c , gbc , hcy) → c , ((b , (fxb , gbc)) , hcy)})
           , λ { (c , (b , fxb , gbc) , hcy) → b , fxb , c , gbc , hcy}
  ; sym-assoc = (λ { (c , (b , fxb , gbc) , hcy) → b , fxb , c , gbc , hcy})
              , (λ { (b , fxb , c , gbc , hcy) → c , ((b , (fxb , gbc)) , hcy)})
  ; identityˡ = (λ { (b , fxb , lift refl) → fxb}) , λ {_} {y} fxy → y , fxy , lift refl
  ; identityʳ = (λ { (a , lift refl , fxy) → fxy}) , λ {x} {_} fxy → x , lift refl , fxy
  ; identity² = (λ { (_ , lift p , lift q) → lift (trans p q)}) , λ { (lift refl) → _ , lift refl , lift refl }
  ; equiv = record
    { refl = id , id
    ; sym = swap
    ; trans = λ { (p₁ , p₂) (q₁ , q₂) → (q₁ ∘′ p₁) , p₂ ∘′ q₂}
    }
  ; ∘-resp-≈ = λ f⇔h g⇔i →
    (λ { (b , gxb , fky) → b , proj₁ g⇔i gxb , proj₁ f⇔h fky }) ,
     λ { (b , ixb , hby) → b , proj₂ g⇔i ixb , proj₂ f⇔h hby }
  }

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:
open import Data.Nat using (ℕ; zero; suc)
open import Data.Bool using (Bool; true; false)

data even : ℕ → Set
data odd : ℕ → Set

data even where
  zero : even zero
  suc : ∀ {n : ℕ} → odd n → even (suc n)
data odd where
  suc : ∀ {n : ℕ} → even n → odd (suc n)

mutual
  data even′ : ℕ → Set where
    zero : even′ zero
    suc : ∀ {n : ℕ} → odd′ n → even′ (suc n)
  data odd′ : ℕ → Set where
    suc : ∀ {n : ℕ} → even′ n → odd′ (suc n)

{-
/Users/wadler/sf/src/extra/Mutual.agda:3,6-10
Missing definition for even
-}


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

module 03-natural-numbers where

import 02-pi
open 02-pi public

-- Section 3.1 The formal specification of the type of natural numbers

data ℕ : UU lzero where
  zero-ℕ : ℕ
  succ-ℕ : ℕ → ℕ

{- We define the numbers one-ℕ to ten-ℕ -}

one-ℕ : ℕ
one-ℕ = succ-ℕ zero-ℕ

two-ℕ : ℕ
two-ℕ = succ-ℕ one-ℕ

three-ℕ : ℕ
three-ℕ = succ-ℕ two-ℕ

four-ℕ : ℕ
four-ℕ = succ-ℕ three-ℕ

five-ℕ : ℕ
five-ℕ = succ-ℕ four-ℕ

six-ℕ : ℕ
six-ℕ = succ-ℕ five-ℕ

seven-ℕ : ℕ
seven-ℕ = succ-ℕ six-ℕ

eight-ℕ : ℕ
eight-ℕ = succ-ℕ seven-ℕ

nine-ℕ : ℕ
nine-ℕ = succ-ℕ eight-ℕ

ten-ℕ : ℕ
ten-ℕ = succ-ℕ nine-ℕ

-- Remark 3.1.2

ind-ℕ : {i : Level} {P : ℕ → UU i} → P zero-ℕ → ((n : ℕ) → P n → P(succ-ℕ n)) → ((n : ℕ) → P n)
ind-ℕ p0 pS zero-ℕ = p0
ind-ℕ p0 pS (succ-ℕ n) = pS n (ind-ℕ p0 pS n)

-- Section 3.2 Addition on the natural numbers

-- Definition 3.2.1

add-ℕ : ℕ → ℕ → ℕ
add-ℕ x zero-ℕ = x
add-ℕ x (succ-ℕ y) = succ-ℕ (add-ℕ x y)

add-ℕ' : ℕ → ℕ → ℕ
add-ℕ' m n = add-ℕ n m

-- Exercises

-- Exercise 3.1

min-ℕ : ℕ → (ℕ → ℕ)
min-ℕ zero-ℕ n = zero-ℕ
min-ℕ (succ-ℕ m) zero-ℕ = zero-ℕ
min-ℕ (succ-ℕ m) (succ-ℕ n) = succ-ℕ (min-ℕ m n)

max-ℕ : ℕ → (ℕ → ℕ)
max-ℕ zero-ℕ n = n
max-ℕ (succ-ℕ m) zero-ℕ = succ-ℕ m
max-ℕ (succ-ℕ m) (succ-ℕ n) = succ-ℕ (max-ℕ m n)

-- Exercise 3.2

mul-ℕ : ℕ → (ℕ → ℕ)
mul-ℕ zero-ℕ n = zero-ℕ
mul-ℕ (succ-ℕ m) n = add-ℕ (mul-ℕ m n) n

-- Exercise 3.3

pow-ℕ : ℕ → (ℕ → ℕ)
pow-ℕ m zero-ℕ = one-ℕ
pow-ℕ m (succ-ℕ n) = mul-ℕ m (pow-ℕ m n)

-- Exercise 3.4

factorial : ℕ → ℕ
factorial zero-ℕ = one-ℕ
factorial (succ-ℕ m) = mul-ℕ (succ-ℕ m) (factorial m)

-- Exercise 3.5

_choose_ : ℕ → ℕ → ℕ
zero-ℕ choose zero-ℕ = one-ℕ
zero-ℕ choose succ-ℕ k = zero-ℕ
(succ-ℕ n) choose zero-ℕ = one-ℕ
(succ-ℕ n) choose (succ-ℕ k) = add-ℕ (n choose k) (n choose (succ-ℕ k))

-- Exercise 3.6

Fibonacci : ℕ → ℕ
Fibonacci zero-ℕ = zero-ℕ
Fibonacci (succ-ℕ zero-ℕ) = one-ℕ
Fibonacci (succ-ℕ (succ-ℕ n)) = add-ℕ (Fibonacci n) (Fibonacci (succ-ℕ n))

{- The above definition of the Fibonacci sequence uses Agda's rather strong
   pattern matching definitions. Below, we will give a definition of the
   Fibonacci sequence in terms of ind-ℕ. In particular, the following is a
   solution that can be given in terms of the material in the book.

   The problem with defining the Fibonacci sequence using ind-ℕ, is that ind-ℕ
   doesn't give us a way to refer to both (F n) and (F (succ-ℕ n)). So, we have
   to give a workaround, where we store two values in the Fibonacci sequence
   at once.

   The basic idea is that we define a sequence of pairs of integers, which will
   be consecutive Fibonacci numbers. This would be a function of type

   ℕ → ℕ².

   Such a function is easy to give with induction, using the map ℕ² → ℕ² that
   takes a pair (m,n) to the pair (n,n+m). Starting the iteration with (0,1)
   we obtain the Fibonacci sequence by taking the first projection.

   However, we haven't defined cartesian products or booleans yet. Therefore
   we mimic the above idea, using ℕ → ℕ instead of ℕ². -}

shift-one : ℕ → (ℕ → ℕ) → (ℕ → ℕ)
shift-one n f = ind-ℕ n (λ x y → f x)

shift-two : ℕ → ℕ → (ℕ → ℕ) → (ℕ → ℕ)
shift-two m n f = shift-one m (shift-one n f)

Fibo-zero-ℕ : ℕ → ℕ
Fibo-zero-ℕ = shift-two zero-ℕ one-ℕ (const ℕ ℕ zero-ℕ)

Fibo-succ-ℕ : (ℕ → ℕ) → (ℕ → ℕ)
Fibo-succ-ℕ f =
  shift-two (f one-ℕ) (add-ℕ (f one-ℕ) (f zero-ℕ)) (λ x → f (succ-ℕ (succ-ℕ x)))

Fibo-function : ℕ → ℕ → ℕ
Fibo-function =
  ind-ℕ
    ( Fibo-zero-ℕ)
    ( λ n → Fibo-succ-ℕ)

Fibo : ℕ → ℕ
Fibo k = Fibo-function k zero-ℕ

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro