text:
module examples.Vec where
  {- Computed datatypes -}
  data One : Set where
    unit : One

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

  data _*_ (A B : Set) : Set where
    pair : A -> B -> A * B

  infixr 20 _=>_
  data _=>_ (A B : Set) : Set where
    lam : (A -> B) -> A => B

  lam2 : {A B C : Set} -> (A -> B -> C) -> (A => B => C)
  lam2 f = lam (\x -> lam (f x))

  app : {A B : Set} -> (A => B) -> A -> B
  app (lam f) x =  f x

  Vec : Nat -> Set -> Set
  Vec  zero   X = One
  Vec (suc n) X = X * Vec n X

  {- ... construct the vectors of a given length -}

  vHead : {X : Set} -> (n : Nat)-> Vec (suc n) X -> X
  vHead n (pair a b) = a

  vTail : {X : Set} -> (n : Nat)-> Vec (suc n) X -> Vec n X
  vTail n (pair a b) = b

  {- safe destructors for nonempty vectors -}

  {- useful vector programming operators -}

  vec : {X : Set} -> (n : Nat) -> X -> Vec n X
  vec zero    x = unit
  vec (suc n) x = pair x (vec n x)

  vapp : {S T : Set} -> (n : Nat) -> Vec n (S => T) -> Vec n S -> Vec n T
  vapp zero unit unit = unit
  vapp (suc n) (pair f fs) (pair s ss) = pair (app f s) (vapp n fs ss)

  {- mapping and zipping come from these -}

  vMap : {S T : Set} -> (n : Nat) -> (S -> T) -> Vec n S -> Vec n T
  vMap n f ss = vapp n (vec n (lam f)) ss

  {- transposition gets the type it deserves -}

  transpose : {X : Set} -> (m n : Nat)-> Vec m (Vec n X) -> Vec n (Vec m X)
  transpose zero n xss = vec n unit
  transpose (suc m) n (pair xs xss) =
    vapp n (vapp n (vec n (lam2 pair)) xs)
	   (transpose m n xss)

  {- Sets of a given finite size may be computed as follows... -}

  {- Resist the temptation to mention idioms. -}

  data Zero : Set where

  data _+_ (A B : Set) : Set where
    inl : A -> A + B
    inr : B -> A + B

  Fin : Nat -> Set
  Fin zero    = Zero
  Fin (suc n) = One + Fin n

  {- We can use these sets to index vectors safely. -}

  vProj : {X : Set} -> (n : Nat)-> Vec n X -> Fin n -> X
  -- vProj zero () we can pretend that there is an exhaustiveness check
  vProj (suc n) (pair x xs) (inl unit) = x
  vProj (suc n) (pair x xs) (inr i)    = vProj n xs i

  {- We can also tabulate a function as a vector. Resist
     the temptation to mention logarithms. -}

  vTab : {X : Set} -> (n : Nat)-> (Fin n -> X) -> Vec n X
  vTab zero    _ = unit
  vTab (suc n) f = pair (f (inl unit)) (vTab n (\x -> f (inr x)))

  {- Question to ponder in your own time:
     if we use functional vectors what are vec and vapp -}

  {- Answer: K and S -}

  {- Inductive datatypes of the unfocused variety -}

  {- Every constructor must target the whole family rather
     than focusing on specific indices. -}

  data Tm (n : Nat) : Set where
    evar : Fin n -> Tm n
    eapp : Tm n -> Tm n -> Tm n
    elam : Tm (suc n) -> Tm n

  {- Renamings -}

  Ren : Nat -> Nat -> Set
  Ren m n = Vec m (Fin n)

  _`Ren`_ = Ren

  {- identity and composition -}

  idR : (n : Nat) -> n `Ren` n
  idR n = vTab n (\i -> i)

  coR : (l m n : Nat) -> m `Ren` n -> l `Ren` m -> l `Ren` n
  coR l m n m2n l2m = vMap l (vProj m m2n) l2m

  {- what theorems should we prove -}

  {- the lifting functor for Ren -}

  liftR : (m n : Nat) -> m `Ren` n -> suc m `Ren` suc n
  liftR m n m2n = pair (inl unit) (vMap m inr m2n)

  {- what theorems should we prove -}

  {- the functor from Ren to Tm-arrows -}

  rename : {m n : Nat} -> (m `Ren` n) -> Tm m -> Tm n
  rename {m}{n} m2n (evar i)   = evar (vProj m m2n i)
  rename {m}{n} m2n (eapp f s) = eapp (rename m2n f) (rename m2n s)
  rename {m}{n} m2n (elam t)   = elam (rename (liftR m n m2n) t)

  {- Substitutions -}

  Sub : Nat -> Nat -> Set
  Sub m n = Vec m (Tm n)

  _`Sub`_ = Sub

  {- identity; composition must wait; why -}

  idS : (n : Nat) -> n `Sub` n
  idS n = vTab n (evar {n})

  {- functor from renamings to substitutions -}

  Ren2Sub : (m n : Nat) -> m `Ren` n -> m `Sub` n
  Ren2Sub m n m2n = vMap m evar m2n

  {- lifting functor for substitution -}

  liftS : (m n : Nat) -> m `Sub` n -> suc m `Sub` suc n
  liftS m n m2n = pair (evar (inl unit))
		       (vMap m (rename (vMap n inr (idR n))) m2n)

  {- functor from Sub to Tm-arrows -}

  subst : {m n : Nat} -> m `Sub` n -> Tm m -> Tm n
  subst {m}{n} m2n (evar i)   = vProj m m2n i
  subst {m}{n} m2n (eapp f s) = eapp (subst m2n f) (subst m2n s)
  subst {m}{n} m2n (elam t)   = elam (subst (liftS m n m2n) t)

  {- and now we can define composition -}

  coS : (l m n : Nat) -> m `Sub` n -> l `Sub` m -> l `Sub` n
  coS l m n m2n l2m = vMap l (subst m2n) l2m

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
open import Level
open import Ordinals
module OrdUtil {n : Level} (O : Ordinals {n} ) where

open import logic
open import nat
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
open import Data.Empty
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Binary hiding (_⇔_)

open Ordinals.Ordinals  O
open Ordinals.IsOrdinals isOrdinal
open Ordinals.IsNext isNext

o<-dom :   { x y : Ordinal } → x o< y → Ordinal
o<-dom  {x} _ = x

o<-cod :   { x y : Ordinal } → x o< y → Ordinal
o<-cod  {_} {y} _ = y

o<-subst : {Z X z x : Ordinal }  → Z o< X → Z ≡ z  →  X ≡ x  →  z o< x
o<-subst df refl refl = df

o<¬≡ :  { ox oy : Ordinal } → ox ≡ oy  → ox o< oy  → ⊥
o<¬≡ {ox} {oy} eq lt with trio< ox oy
o<¬≡ {ox} {oy} eq lt | tri< a ¬b ¬c = ¬b eq
o<¬≡ {ox} {oy} eq lt | tri≈ ¬a b ¬c = ¬a lt
o<¬≡ {ox} {oy} eq lt | tri> ¬a ¬b c = ¬b eq

o<> :   {x y : Ordinal   }  →  y o< x → x o< y → ⊥
o<> {ox} {oy} lt tl with trio< ox oy
o<> {ox} {oy} lt tl | tri< a ¬b ¬c = ¬c lt
o<> {ox} {oy} lt tl | tri≈ ¬a b ¬c = ¬a tl
o<> {ox} {oy} lt tl | tri> ¬a ¬b c = ¬a tl

osuc-< :  { x y : Ordinal  } → y o< osuc x  → x o< y → ⊥
osuc-< {x} {y} y<ox x<y with osuc-≡< y<ox
osuc-< {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y
osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x

osucc :  {ox oy : Ordinal } → oy o< ox  → osuc oy o< osuc ox
----   y < osuc y < x < osuc x
----   y < osuc y = x < osuc x
----   y < osuc y > x < osuc x   -> y = x ∨ x < y → ⊥
osucc {ox} {oy} oy<ox with trio< (osuc oy) ox
osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc
osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc
osucc {ox} {oy} oy<ox | tri> ¬a ¬b c with  osuc-≡< c
osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy<ox)
osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy<ox)

osucprev :  {ox oy : Ordinal } → osuc oy o< osuc ox  → oy o< ox
osucprev {ox} {oy} oy<ox with trio< oy ox
osucprev {ox} {oy} oy<ox | tri< a ¬b ¬c = a
osucprev {ox} {oy} oy<ox | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (cong (λ k → osuc k) b) oy<ox )
osucprev {ox} {oy} oy<ox | tri> ¬a ¬b c = ⊥-elim (o<> (osucc c) oy<ox )

open _∧_

osuc2 :  ( x y : Ordinal  ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
proj2 (osuc2 x y) lt = osucc lt
proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy
proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy
proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy

_o≤_ :  Ordinal → Ordinal → Set  n
a o≤ b  = a o< osuc b -- (a ≡ b)  ∨ ( a o< b )

xo<ab :  {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa  → ox o< ob ) → oa o< osuc ob
xo<ab   {oa} {ob} a→b with trio< oa ob
xo<ab   {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc
xo<ab   {oa} {ob} a→b | tri≈ ¬a refl ¬c = <-osuc
xo<ab   {oa} {ob} a→b | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c )  )

maxα :   Ordinal  →  Ordinal  → Ordinal
maxα x y with trio< x y
maxα x y | tri< a ¬b ¬c = y
maxα x y | tri> ¬a ¬b c = x
maxα x y | tri≈ ¬a refl ¬c = x

omin :    Ordinal  →  Ordinal  → Ordinal
omin  x y with trio<  x  y
omin x y | tri< a ¬b ¬c = x
omin x y | tri> ¬a ¬b c = y
omin x y | tri≈ ¬a refl ¬c = x

min1 :   {x y z : Ordinal  } → z o< x → z o< y → z o< omin x y
min1  {x} {y} {z} z<x z<y with trio<  x y
min1  {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x
min1  {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x
min1  {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y

--
--  max ( osuc x , osuc y )
--

omax :  ( x y : Ordinal  ) → Ordinal
omax  x y with trio< x y
omax  x y | tri< a ¬b ¬c = osuc y
omax  x y | tri> ¬a ¬b c = osuc x
omax  x y | tri≈ ¬a refl ¬c  = osuc x

omax< :  ( x y : Ordinal  ) → x o< y → osuc y ≡ omax x y
omax<  x y lt with trio< x y
omax<  x y lt | tri< a ¬b ¬c = refl
omax<  x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt )
omax<  x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt )

omax≤ :  ( x y : Ordinal  ) → x o≤ y → osuc y ≡ omax x y
omax≤  x y le with trio< x y
omax≤  x y le | tri< a ¬b ¬c = refl
omax≤  x y le | tri≈ ¬a refl ¬c = refl
omax≤  x y le | tri> ¬a ¬b c with osuc-≡< le
omax≤ x y le | tri> ¬a ¬b c | case1 eq = ⊥-elim (¬b eq)
omax≤ x y le | tri> ¬a ¬b c | case2 x<y = ⊥-elim (¬a x<y)

omax≡ :  ( x y : Ordinal  ) → x ≡ y → osuc y ≡ omax x y
omax≡  x y eq with trio< x y
omax≡  x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq )
omax≡  x y eq | tri≈ ¬a refl ¬c = refl
omax≡  x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq )

omax-x :  ( x y : Ordinal  ) → x o< omax x y
omax-x  x y with trio< x y
omax-x  x y | tri< a ¬b ¬c = ordtrans a <-osuc
omax-x  x y | tri> ¬a ¬b c = <-osuc
omax-x  x y | tri≈ ¬a refl ¬c = <-osuc

omax-y :  ( x y : Ordinal  ) → y o< omax x y
omax-y  x y with  trio< x y
omax-y  x y | tri< a ¬b ¬c = <-osuc
omax-y  x y | tri> ¬a ¬b c = ordtrans c <-osuc
omax-y  x y | tri≈ ¬a refl ¬c = <-osuc

omxx :  ( x : Ordinal  ) → omax x x ≡ osuc x
omxx  x with  trio< x x
omxx  x | tri< a ¬b ¬c = ⊥-elim (¬b refl )
omxx  x | tri> ¬a ¬b c = ⊥-elim (¬b refl )
omxx  x | tri≈ ¬a refl ¬c = refl

omxxx :  ( x : Ordinal  ) → omax x (omax x x ) ≡ osuc (osuc x)
omxxx  x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc ))

open _∧_

o≤-refl :  { i  j : Ordinal } → i ≡ j → i o≤ j
o≤-refl {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc
OrdTrans :  Transitive  _o≤_
OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c
OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc
OrdTrans a≤b b≤c | case1 refl | case2 a≤c = ordtrans a≤c <-osuc
OrdTrans a≤b b≤c | case2 a≤c | case1 refl = ordtrans a≤c <-osuc
OrdTrans a≤b b≤c | case2 a<b | case2 b<c = ordtrans (ordtrans a<b  b<c) <-osuc

OrdPreorder :   Preorder n n n
OrdPreorder  = record { Carrier = Ordinal
   ; _≈_  = _≡_
   ; _∼_   = _o≤_
   ; isPreorder   = record {
        isEquivalence = record { refl = refl  ; sym = sym ; trans = trans }
        ; reflexive     = o≤-refl
        ; trans         = OrdTrans
     }
 }

FExists : {m l : Level} → ( ψ : Ordinal  → Set m )
  → {p : Set l} ( P : { y : Ordinal  } →  ψ y → ¬ p )
  → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
  → ¬ p
FExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )

nexto∅ : {x : Ordinal} → o∅ o< next x
nexto∅ {x} with trio< o∅ x
nexto∅ {x} | tri< a ¬b ¬c = ordtrans a x<nx
nexto∅ {x} | tri≈ ¬a b ¬c = subst (λ k → k o< next x) (sym b) x<nx
nexto∅ {x} | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )

next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
next< {x} {y} {z} x<nz y<nx with trio< y (next z)
next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a
next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim (¬nx<nx x<nz (subst (λ k → k o< next x) b y<nx)
   (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc) ))))
next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (¬nx<nx x<nz (ordtrans c y<nx )
   (λ w nz=ow → o<¬≡ (sym nz=ow) (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc ))))

osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y
osuc< {x} {y} refl = <-osuc

nexto=n : {x y : Ordinal} → x o< next (osuc y)  → x o< next y
nexto=n {x} {y} x<noy = next< (osuc<nx x<nx) x<noy

nexto≡ : {x : Ordinal} → next x ≡ next (osuc x)
nexto≡ {x} with trio< (next x) (next (osuc x) )
--    next x o< next (osuc x ) ->  osuc x o< next x o< next (osuc x) -> next x ≡ osuc z -> z o o< next x -> osuc z o< next x -> next x o< next x
nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx<nx (osuc<nx  x<nx ) a
   (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
nexto≡ {x} | tri≈ ¬a b ¬c = b
--    next (osuc x) o< next x ->  osuc x o< next (osuc x) o< next x -> next (osuc x) ≡ osuc z -> z o o< next (osuc x) ...
nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) c
   (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))

next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y)
next-is-limit {x} {y} eq = o<¬≡ (sym eq) (osuc<nx y<nx) where
    y<nx : y o< next x
    y<nx = osuc< (sym eq)

omax<next : {x y : Ordinal} → x o< y → omax x y o< next y
omax<next {x} {y} x<y = subst (λ k → k o< next y ) (omax< _ _ x<y ) (osuc<nx x<nx)

x<ny→≡next : {x y : Ordinal} → x o< y → y o< next x → next x ≡ next y
x<ny→≡next {x} {y} x<y y<nx with trio< (next x) (next y)
x<ny→≡next {x} {y} x<y y<nx | tri< a ¬b ¬c =          -- x < y < next x <  next y ∧ next x = osuc z
     ⊥-elim ( ¬nx<nx y<nx a (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc ))))
x<ny→≡next {x} {y} x<y y<nx | tri≈ ¬a b ¬c = b
x<ny→≡next {x} {y} x<y y<nx | tri> ¬a ¬b c =          -- x < y < next y < next x
     ⊥-elim ( ¬nx<nx (ordtrans x<y x<nx) c (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc ))))

≤next : {x y : Ordinal} → x o≤ y → next x o≤ next y
≤next {x} {y} x≤y with trio< (next x) y
≤next {x} {y} x≤y | tri< a ¬b ¬c = ordtrans a (ordtrans x<nx <-osuc )
≤next {x} {y} x≤y | tri≈ ¬a refl ¬c = (ordtrans x<nx <-osuc )
≤next {x} {y} x≤y | tri> ¬a ¬b c with osuc-≡< x≤y
≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl refl   -- x = y < next x
≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl (x<ny→≡next x<y c) -- x ≤ y < next x

x<ny→≤next : {x y : Ordinal} → x o< next y → next x o≤ next y
x<ny→≤next {x} {y} x<ny with trio< x y
x<ny→≤next {x} {y} x<ny | tri< a ¬b ¬c =  ≤next (ordtrans a <-osuc )
x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c =  o≤-refl refl
x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl (sym ( x<ny→≡next c x<ny ))

omax<nomax : {x y : Ordinal} → omax x y o< next (omax x y )
omax<nomax {x} {y} with trio< x y
omax<nomax {x} {y} | tri< a ¬b ¬c    = subst (λ k → osuc y o< k ) nexto≡ (osuc<nx x<nx )
omax<nomax {x} {y} | tri≈ ¬a refl ¬c = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )
omax<nomax {x} {y} | tri> ¬a ¬b c    = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )

omax<nx : {x y z : Ordinal} → x o< next z → y o< next z → omax x y o< next z
omax<nx {x} {y} {z} x<nz y<nz with trio< x y
omax<nx {x} {y} {z} x<nz y<nz | tri< a ¬b ¬c = osuc<nx y<nz
omax<nx {x} {y} {z} x<nz y<nz | tri≈ ¬a refl ¬c = osuc<nx y<nz
omax<nx {x} {y} {z} x<nz y<nz | tri> ¬a ¬b c = osuc<nx x<nz

nn<omax : {x nx ny : Ordinal} → x o< next nx → x o< next ny → x o< next (omax nx ny)
nn<omax {x} {nx} {ny} xnx xny with trio< nx ny
nn<omax {x} {nx} {ny} xnx xny | tri< a ¬b ¬c = subst (λ k → x o< k ) nexto≡ xny
nn<omax {x} {nx} {ny} xnx xny | tri≈ ¬a refl ¬c = subst (λ k → x o< k ) nexto≡ xny
nn<omax {x} {nx} {ny} xnx xny | tri> ¬a ¬b c = subst (λ k → x o< k ) nexto≡ xnx

record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
  field
    os→ : (x : Ordinal) → x o< maxordinal → Ordinal
    os← : Ordinal → Ordinal
    os←limit : (x : Ordinal) → os← x o< maxordinal
    os-iso← : {x : Ordinal} →  os→  (os← x) (os←limit x) ≡ x
    os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) →  os← (os→ x lt) ≡ x

module o≤-Reasoning {n : Level}  (O : Ordinals {n} )  where

    -- open inOrdinal O

    resp-o< : _o<_ Respects₂ _≡_
    resp-o< =  resp₂ _o<_

    trans1 : {i j k : Ordinal} → i o< j → j o< osuc  k → i o< k
    trans1 {i} {j} {k} i<j j<ok with osuc-≡< j<ok
    trans1 {i} {j} {k} i<j j<ok | case1 refl = i<j
    trans1 {i} {j} {k} i<j j<ok | case2 j<k = ordtrans i<j j<k

    trans2 : {i j k : Ordinal} → i o< osuc j → j o<  k → i o< k
    trans2 {i} {j} {k} i<oj j<k with osuc-≡< i<oj
    trans2 {i} {j} {k} i<oj j<k | case1 refl = j<k
    trans2 {i} {j} {k} i<oj j<k | case2 i<j = ordtrans i<j j<k

    open import Relation.Binary.Reasoning.Base.Triple
      (Preorder.isPreorder OrdPreorder)
         ordtrans --<-trans
         (resp₂ _o<_) --(resp₂ _<_)
         (λ x → ordtrans x <-osuc ) --<⇒≤
         trans1 --<-transˡ
         trans2 --<-transʳ
         public
         -- hiding (_≈⟨_⟩_)

ext: agda

max_stars_repo_name: shinji-kono/zf-in-agda

max_issues_repo_name: shinji-kono/zf-in-agda

max_forks_repo_name: shinji-kono/zf-in-agda


text:
module Prelude where
  open import Agda.Primitive using (Level; lzero; lsuc) renaming (_⊔_ to lmax)
  open import Relation.Binary.PropositionalEquality as Eq

  open import Data.List
  open import Data.Nat.Properties

  open import Data.List.Membership.DecSetoid ≡-decSetoid

  open import Data.List.Relation.Unary.Any
  open import Data.Empty

  open import Data.List.Relation.Unary.All

  -- sums
  data _+̇_ (A B : Set) : Set where
    Inl : A → A +̇ B
    Inr : B → A +̇ B

 -- Basic properties of lists
  emptyListIsEmpty : ∀ {x}
                     → x ∉ []
  emptyListIsEmpty ()

  listNoncontainment : ∀ {x x' L}
                        → x ∉ L
                        → x' ∈ L
                        → x ≢ x'
  listNoncontainment {x} {x'} {L} xNotInL x'InL = λ xEqx' → xNotInL (Eq.subst (λ a → a ∈ L) (Eq.sym xEqx') x'InL)

  listConcatNoncontainment : ∀ {x x' L}
                             → x ≢ x'
                             → x ∉ L
                             → x ∉ (x' ∷ L)
  listConcatNoncontainment {x} {x'} {L} xNeqx' xNotInL (here xEqx') = xNeqx' xEqx'
  listConcatNoncontainment {x} {x'} {L} xNeqx' xNotInL (there xInConcat) = xNotInL xInConcat

  listConcatContainment : ∀ {x x' t}
                          → x ∈ (x' ∷ t)
                          → x' ≢ x
                          → x ∈ t

  listConcatContainment {x} {x'} {t} (here px) x'Neqx = ⊥-elim (x'Neqx (Eq.sym px))
  listConcatContainment {x} {x'} {t} (there xInCons) x'Neqx = xInCons

-- Basic properties of equality
  ≢-sym : ∀ {a} {A : Set a} → {x x' : A}
          → x ≢ x'
          → x' ≢ x
  ≢-sym xNeqx' = λ x'Eqx → xNeqx' (Eq.sym x'Eqx)

-- Congruence
  cong₃ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
        (f : A → B → C → D) {x y u v w t} → x ≡ y → u ≡ v → w ≡ t → f x u w ≡ f y v t
  cong₃ f refl refl refl = refl

-- All
  allInsideOut : {A : Set}
                 → {L L' : List A}
                 → {P : A → A → Set}
                 → (∀ {T T'} → P T T' → P T' T)
                 → All (λ T → All (λ T' → P T T') L) L'
                 → All (λ T → All (λ T' → P T T') L') L
  allInsideOut {A} {[]} {.[]} sym [] = []
  allInsideOut {A} {x ∷ L} {.[]} sym [] = [] ∷ allRelatedToEmpty
    where
      allRelatedToEmpty : {A : Set}
                          → {L : List A}
                          → {P : A → A → Set}
                          → All (λ T → All (P T) []) L
      allRelatedToEmpty {A} {[]} {P} = []
      allRelatedToEmpty {A} {x ∷ L} {P} = [] ∷ allRelatedToEmpty
  allInsideOut {A} {[]} {.(_ ∷ _)} sym (all₁ ∷ all₂) = []
  allInsideOut {A} {x ∷ L} {(x' ∷ L')} {P} sym (all₁ ∷ all₂) =
    ((sym (Data.List.Relation.Unary.All.head all₁)) ∷ unwrap L' all₂) ∷
      allInsideOut sym (Data.List.Relation.Unary.All.tail all₁ ∷  unwrap2 L' all₂)
    where
      unwrap : (M : List A)
               → All (λ T → All (P T) (x ∷ L)) M
               → All (λ T' → P x T') M
      unwrap .[] [] = []
      unwrap (x ∷ r) (h ∷ t) = (sym (Data.List.Relation.Unary.All.head h)) ∷ unwrap r t

      unwrap2 : (M : List A)
                → All (λ T → All (P T) (x ∷ L)) M
                → All (λ T → All (P T) L) M
      unwrap2 [] all = []
      unwrap2 (x ∷ M) (all₁ ∷ all₂) = (Data.List.Relation.Unary.All.tail all₁) ∷ unwrap2 M all₂

{-
-- equality of naturals is decidable. we represent this as computing a
  -- choice of units, with inl <> meaning that the naturals are indeed the
  -- same and inr <> that they are not.
  natEQ : (x y : ℕ) → ((x ≡ y) + ((x ≡ y) → ⊥))
  natEQ Z Z = Inl refl
  natEQ Z (1+ y) = Inr (λ ())
  natEQ (1+ x) Z = Inr (λ ())
  natEQ (1+ x) (1+ y) with natEQ x y
  natEQ (1+ x) (1+ .x) | Inl refl = Inl refl
  ... | Inr b = Inr (λ x₁ → b (1+inj x y x₁))

  -- nat equality as a predicate. this saves some very repetative casing.
  natEQp : (x y : ℕ) → Set
  natEQp x y with natEQ x y
  natEQp x .x | Inl refl = ⊥
  natEQp x y | Inr x₁ = ⊤
-}

{-

  -- equality
  data _≡_ {l : Level} {A : Set l} (M : A) : A → Set l where
    refl : M ≡ M

  infixr 9 _≡_

  {-# BUILTIN EQUALITY _≡_ #-}

  -- transitivity of equality
  _·_ : {l : Level} {α : Set l} {x y z : α} → x ≡ y → y ≡ z → x ≡ z
  refl · refl = refl

  -- symmetry of equality
  ! : {l : Level} {α : Set l} {x y : α} → x ≡ y → y ≡ x
  ! refl = refl

  -- ap, in the sense of HoTT, that all functions respect equality in their
  -- arguments. named in a slightly non-standard way to avoid naming
  -- clashes with hazelnut constructors.
  ap1 : {l1 l2 : Level} {α : Set l1} {β : Set l2} {x y : α} (F : α → β)
          → x ≡ y → F x ≡ F y
  ap1 F refl = refl

  -- transport, in the sense of HoTT, that fibrations respect equality
  tr : {l1 l2 : Level} {α : Set l1} {x y : α}
                    (B : α → Set l2)
                    → x ≡ y
                    → B x
                    → B y
  tr B refl x₁ = x₁

  -- options
  data Maybe (A : Set) : Set where
    Some : A → Maybe A
    None : Maybe A

  -- the some constructor is injective. perhaps unsurprisingly.
  someinj : {A : Set} {x y : A} → Some x ≡ Some y → x ≡ y
  someinj refl = refl

  --  some isn't none.
  somenotnone : {A : Set} {x : A} → Some x ≡ None → ⊥
  somenotnone ()

  -- function extensionality, used to reason about contexts as finite
  -- functions.
  postulate
     funext : {A : Set} {B : A → Set} {f g : (x : A) → (B x)} →
              ((x : A) → f x ≡ g x) → f ≡ g

  -- non-equality is commutative
  flip : {A : Set} {x y : A} → (x ≡ y → ⊥) → (y ≡ x → ⊥)
  flip neq eq = neq (! eq)

  -- two types are said to be equivalent, or isomorphic, if there is a pair
  -- of functions between them where both round-trips are stable up to ≡
  _≃_ : Set → Set → Set
  _≃_ A B = Σ[ f ∈ (A → B) ] Σ[ g ∈ (B → A) ]
             (((a : A) → g (f a) ≡ a) × (((b : B) → f (g b) ≡ b)))

 -}

max_stars_repo_name: ivoysey/Obsidian

max_issues_repo_name: ivoysey/Obsidian

max_forks_repo_name: ivoysey/Obsidian


text:
-- Andreas, 2020-02-06, issue #906, and #942 #2068 #3136 #3431 #4391 #4418
--
-- Termination checker now tries to reduce calls away
-- using non-recursive clauses.
--
-- This fixes the problem that for dependent copattern definitions
-- the earlier, non-recursive clauses get into non-guarded positions
-- in later clauses via Agda's constraint solver, and there confuse
-- the termination checker.

module Issue906EtAl where

module Issue906 where

  {- Globular types as a coinductive record -}
  record Glob : Set1 where
    coinductive
    field
      Ob : Set
      Hom : (a b : Ob) → Glob
  open Glob

  record Unit : Set where

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

  {- The terminal globular type -}
  Unit-glob : Glob
  Ob Unit-glob = Unit
  Hom Unit-glob _ _ = Unit-glob

  {- The tower of identity types -}
  Id-glob : (A : Set) → Glob
  Ob (Id-glob A) = A
  Hom (Id-glob A) a b = Id-glob (a == b)

module Issue907 where

  data _==_ {A : Set} (a : A) : A → Set where
    idp : a == a

  -- Coinductive equivalences
  record CoEq (A B : Set) : Set where
    coinductive
    constructor coEq
    field to : A → B
          from : B → A
          eq : (a : A) (b : B) → CoEq (a == from b) (to a == b)

  open CoEq public

  id-CoEq : (A : Set) → CoEq A A
  to   (id-CoEq A) a   = a
  from (id-CoEq A) b   = b
  eq   (id-CoEq A) a b = id-CoEq _ -- Keep underscore!
    -- Solution: (a == from (id-CoEq A) b)
    -- contains recursive call

module Issue942 where

  record Sigma (A : Set)(P : A → Set) : Set where
    constructor _,_
    field
      fst : A
      snd : P fst
  open Sigma

  postulate
    A : Set
    x : A
    P Q : A → Set
    Px : P x
    f  : ∀ {x} → P x → Q x

  ex : Sigma A Q
  ex = record
         { fst = x
         ; snd = f Px -- goal: P x
         }

  ex' : Sigma A Q
  ex' = x , f Px -- goal: P x

  ex'' : Sigma A Q
  fst ex'' = x
  snd ex'' = f Px -- goal: P (fst ex'')

module Issue2068-OP where

  data _==_ {A : Set} : A → A → Set where
    refl : {a : A} → a == a

  data Bool : Set where
    tt : Bool
    ff : Bool

  record TwoEqualFunctions : Set₁ where
    field
      A : Set
      B : Set
      f : A → B
      g : A → B
      p : f == g

  postulate
    funext : {A B : Set} {f g : A → B} → ((a : A) → f a == g a) → f == g

  identities : TwoEqualFunctions
  TwoEqualFunctions.A identities = Bool
  TwoEqualFunctions.B identities = Bool
  TwoEqualFunctions.f identities x = x
  TwoEqualFunctions.g identities = λ{tt → tt ; ff → ff}
  TwoEqualFunctions.p identities = funext (λ{tt → refl ; ff → refl})

module Issue2068b where

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

  data Unit : Set where
    unit : Unit

  record R : Set₁ where
    field
      f : Unit → Unit
      p : f == λ x → x

  postulate
    extId : (f : Unit → Unit) → (∀ a → f a == a) → f == λ x → x

  test : R
  R.f test = λ{ unit → unit }
  R.p test = extId _ λ{ unit → refl _ }
  -- R.p test = extId {! R.f test !} λ{unit → refl {! R.f test unit !}}

module Issue2068c where

  record _×_ (A B : Set) : Set where
    field fst : A
          snd : B
  open _×_

  test : ∀{A} (a : A) → (A → A) × (A → A)
  fst (test a) x = a
  snd (test a) x = fst (test a) (snd (test a) x)

module Issue3136 (A : Set) where

  -- Andreas, 2018-07-22, issue #3136
  -- WAS: Internal error when printing termination errors

  postulate
    any : {X : Set} → X
    x : A
    P : A → Set

  record C : Set where
    field
      a : A
      b : P a

  c : C
  c = λ where
    .C.a → x
    .C.b → λ where
      → any

  -- NOW: succeeds

module Issue3413 where

  open import Agda.Builtin.Sigma
  open import Agda.Builtin.Equality

  postulate
    A : Set
    P : ∀{X : Set} → X → Set

  record Bob : Set₁ where
    field
      RE : Set
      resp : RE → Set

  open Bob

  bob : Bob
  bob .RE     = A
  bob .resp e = Σ (P e) λ {x → A}

module Issue4391 where

  record GlobSet : Set₁ where
    coinductive
    field
      cells : Set
      morphisms : cells → cells → GlobSet

  open GlobSet public

  record GlobSetMorphism (G H : GlobSet) : Set where
    coinductive
    field
      func : cells G → cells H
      funcMorphisms : (x y : cells G)
                    → GlobSetMorphism (morphisms G x y)
                                      (morphisms H (func x) (func y))

  open GlobSetMorphism public

  gComp : {G H I : GlobSet} → GlobSetMorphism H I → GlobSetMorphism G H → GlobSetMorphism G I
  func (gComp ϕ ψ) x = func ϕ (func ψ x)
  funcMorphisms (gComp ϕ ψ) x y = gComp (funcMorphisms ϕ (func ψ x) (func ψ y)) (funcMorphisms ψ x y)

module Issue4391Nisse where

  record GlobSet : Set₁ where
    coinductive
    field
      cells     : Set
      morphisms : cells → cells → GlobSet

  open GlobSet public

  mutual

    record GlobSetMorphism (G H : GlobSet) : Set where
      inductive
      field
        func          : cells G → cells H
        funcMorphisms : (x y : cells G) →
                        GlobSetMorphism′
                          (morphisms G x y)
                          (morphisms H (func x) (func y))

    record GlobSetMorphism′ (G H : GlobSet) : Set where
      coinductive
      field
        force : GlobSetMorphism G H

  open GlobSetMorphism  public
  open GlobSetMorphism′ public

  works fails :
    {G H I : GlobSet} →
    GlobSetMorphism H I → GlobSetMorphism G H → GlobSetMorphism G I

  works ϕ ψ = record
    { func          = λ x → func ϕ (func ψ x)
    ; funcMorphisms = λ { x y .force →
        works (funcMorphisms ϕ (func ψ x) (func ψ y) .force)
              (funcMorphisms ψ x y .force) }
    }

  fails ϕ ψ .func          = λ x → func ϕ (func ψ x)
  fails ϕ ψ .funcMorphisms = λ { x y .force →
    fails (funcMorphisms ϕ (func ψ x) (func ψ y) .force)
          (funcMorphisms ψ x y .force) }

module Issue4418 {l}
  (Index : Set l)
  (Shape : Index → Set l)
  (Position : (i : Index) → Shape i → Set l)
  (index : (i : Index) → (s : Shape i) → Position i s → Index) where

  record M (i : Index) : Set l where
    coinductive
    field shape : Shape i
    field children : (p : Position i shape) → M (index i shape p)

  open M

  record MBase (Rec : Index → Set l) (i : Index) : Set l where
    coinductive
    field shapeB : Shape i
    field childrenB : (p : Position i shapeB) → Rec (index i shapeB p)

  open MBase

  module _ (S : Index → Set l) (u : ∀ {i} → S i → MBase S i) where

    unroll : ∀ i → S i → M i
    unroll i s .shape      = u s .shapeB
    unroll i s .children p = unroll _ (u s .childrenB p)
      -- Underscore solved as:  index i (u s .shapeB) p

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
open import Formalization.PredicateLogic.Signature

module Formalization.PredicateLogic.Syntax.Tree (𝔏 : Signature) where
open Signature(𝔏)

open import Data.DependentWidthTree as Tree hiding (height)
import      Functional.Dependent
import      Lvl
open import Formalization.PredicateLogic.Syntax(𝔏)
open import Formalization.PredicateLogic.Syntax.Substitution(𝔏)
open import Functional using (_∘_ ; _∘₂_ ; _∘₃_ ; _∘₄_ ; swap ; _←_ ; _on₂_)
open import Numeral.Finite
open import Numeral.Natural.Function.Proofs
open import Numeral.Natural.Inductions
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs
open import Numeral.Natural
open import Relator.Equals
open import Structure.Relator
open import Structure.Relator.Ordering
open import Structure.Relator.Ordering.Proofs
open import Type.Dependent
open import Type

private variable ℓ : Lvl.Level
private variable vars vars₁ vars₂ : ℕ
private variable φ ψ : Formula(vars)

tree : Formula(vars) → FiniteTreeStructure
tree (_ $ _) = Node 0 \()
tree ⊤       = Node 0 \()
tree ⊥       = Node 0 \()
tree (φ ∧ ψ) = Node 2 \{𝟎 → tree φ; (𝐒 𝟎) → tree ψ}
tree (φ ∨ ψ) = Node 2 \{𝟎 → tree φ; (𝐒 𝟎) → tree ψ}
tree (φ ⟶ ψ) = Node 2 \{𝟎 → tree φ; (𝐒 𝟎) → tree ψ}
tree (Ɐ φ)   = Node 1 \{𝟎 → tree φ}
tree (∃ φ)   = Node 1 \{𝟎 → tree φ}

height : Formula(vars) → ℕ
height = Tree.height ∘ tree

-- Ordering on formulas based on the height of their tree representation.
_<↑_ : (Σ ℕ Formula) → (Σ ℕ Formula) → Type
_<↑_ = (_<_) on₂ (height Functional.Dependent.∘ Σ.right)

substitute-height : ∀{t} → (height(substitute{vars₁ = vars₁}{vars₂ = vars₂} t φ) ≡ height φ)
substitute-height {φ = f $ x} = [≡]-intro
substitute-height {φ = ⊤}     = [≡]-intro
substitute-height {φ = ⊥}     = [≡]-intro
substitute-height {φ = φ ∧ ψ} {t} rewrite substitute-height {φ = φ}{t} rewrite substitute-height {φ = ψ}{t} = [≡]-intro
substitute-height {φ = φ ∨ ψ} {t} rewrite substitute-height {φ = φ}{t} rewrite substitute-height {φ = ψ}{t} = [≡]-intro
substitute-height {φ = φ ⟶ ψ} {t} rewrite substitute-height {φ = φ}{t} rewrite substitute-height {φ = ψ}{t} = [≡]-intro
substitute-height {φ = Ɐ φ}   {t} rewrite substitute-height {φ = φ}{termMapper𝐒 t} = [≡]-intro
substitute-height {φ = ∃ φ}   {t} rewrite substitute-height {φ = φ}{termMapper𝐒 t} = [≡]-intro

instance
  [<↑]-wellfounded : Strict.Properties.WellFounded(_<↑_)
  [<↑]-wellfounded = wellfounded-image-by-trans {f = height Functional.Dependent.∘ Σ.right}

induction-on-height : (P : ∀{vars} → Formula(vars) → Type{ℓ}) → (∀{vars}{φ : Formula(vars)} → (∀{vars}{ψ : Formula(vars)} → (height ψ < height φ) → P(ψ)) → P(φ)) → ∀{vars}{φ : Formula(vars)} → P(φ)
induction-on-height P step {vars}{φ} = Strict.Properties.wellfounded-induction(_<↑_) (\{ {intro vars φ} p → step{vars}{φ} \{vars}{ψ} ph → p{intro vars ψ} ⦃ ph ⦄}) {intro vars φ}

⊤-height-order : (height{vars} ⊤ ≤ height φ)
⊤-height-order = [≤]-minimum

⊥-height-order : (height{vars} ⊥ ≤ height φ)
⊥-height-order = [≤]-minimum

∧-height-orderₗ : (height φ < height(φ ∧ ψ))
∧-height-orderₗ = [≤]-with-[𝐒]

∧-height-orderᵣ : (height ψ < height(φ ∧ ψ))
∧-height-orderᵣ = [≤]-with-[𝐒]

∨-height-orderₗ : (height φ < height(φ ∨ ψ))
∨-height-orderₗ = [≤]-with-[𝐒]

∨-height-orderᵣ : (height ψ < height(φ ∨ ψ))
∨-height-orderᵣ = [≤]-with-[𝐒]

⟶-height-orderₗ : (height φ < height(φ ⟶ ψ))
⟶-height-orderₗ = [≤]-with-[𝐒]

⟶-height-orderᵣ : (height ψ < height(φ ⟶ ψ))
⟶-height-orderᵣ = [≤]-with-[𝐒]

Ɐ-height-order : (height φ < height(Ɐ φ))
Ɐ-height-order = [<]-of-[𝐒]

∃-height-order : (height φ < height(∃ φ))
∃-height-order = [<]-of-[𝐒]

-- induction-on-height : ∀{P : ∀{vars} → Formula(vars) → Type{ℓ}} → (∀{vars} → P{vars}(⊤)) → (∀{vars} → P{vars}(⊥)) → ((∀{vars}{ψ : Formula(vars)} → (height ψ < height φ) → P(ψ)) → P(φ)) → P(φ)
-- induction-on-height {φ = φ} base⊤ base⊥ step = step {!Strict.Properties.wellfounded-induction(_<↑_)!}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --sized-types #-}
open import Relation.Binary.Core

module Mergesort.Impl1.Correctness.Order {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)  where

open import Data.List
open import Function using (_∘_)
open import List.Sorted _≤_
open import Mergesort.Impl1 _≤_ tot≤
open import SList
open import SOList.Lower _≤_
open import SOList.Lower.Properties _≤_

theorem-mergesort-sorted : (xs : List A) → Sorted (forget (mergesort (size A xs)))
theorem-mergesort-sorted = lemma-solist-sorted  ∘ mergesort ∘ (size A)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Fough where

open import Agda.Primitive renaming (_⊔_ to lmax)

record Setoid l : Set (lsuc l) where
  field
    El : Set l
    Eq : El -> El -> Set l
    Rf : (x : El) -> Eq x x
    Sy : (x y : El) -> Eq x y -> Eq y x
    Tr : (x y z : El) -> Eq x y -> Eq y z -> Eq x z
open Setoid

module PACKQ {l}(X : Setoid l) where

  record _|-_~~_ (x y : El X) : Set l where
    constructor eq
    field
      qe : Eq X x y

  open _|-_~~_ public

  qprf = qe

module _ {l}{X : Setoid l} where

  open PACKQ X

  infixr 5 _~[_>~_ _~<_]~_
  infixr 6 _[SQED]

  _~[_>~_ : forall x {y z} -> _|-_~~_ x y -> _|-_~~_ y z -> _|-_~~_ x z
  x ~[ eq q >~ eq q' = eq (Tr X _ _ _ q q')

  _~<_]~_ : forall x {y z} -> _|-_~~_ y x -> _|-_~~_ y z -> _|-_~~_ x z
  x ~< eq q ]~ eq q' = eq (Tr X _ _ _ (Sy X _ _ q) q')

  _[SQED] : forall x -> _|-_~~_ x x
  _[SQED] x = eq (Rf X x)

  rS : forall {x} -> _|-_~~_ x x
  rS {x} = eq (Rf X x)

open PACKQ public

module _ {l}{X : Set l} where
  data _~_ (x : X) : X -> Set l where
    r~ : x ~ x

{-# BUILTIN EQUALITY _~_ #-}

module _ {l}(X : Set l) where

  IN : Setoid l
  El IN = X
  Eq IN = _~_
  Rf IN x = r~
  Sy IN x y r~ = r~
  Tr IN x y z r~ q = q

module _ {k l}(S : Set k)(T : S -> Set l) where

  record _><_ : Set (lmax k l) where
    constructor _,_
    field
      fst : S
      snd : T fst
  open _><_ public

  infixr 10 _,_
  infixr 20 _><_

module _ (l : Level) where
  record One : Set l where constructor <>

infixr 20 _*_
_*_ : forall {k l} -> Set k -> Set l -> Set (lmax k l)
S * T = S >< \ _ -> T

infix 22 <_>
<_> : forall {k l}{S : Set k}(T : S -> Set l) -> Set (lmax k l)
< T > = _ >< T

infixr 23 _:*_
_:*_ : forall {k l}{S : Set k}(T U : S -> Set l) -> S -> Set l
(T :* U) s = T s * U s

infixr 11 _&_
pattern _&_ s t = _ , s , t

infixr 9 _/\_
_/\_ : forall {k l}{S : Set k}{T : Set l} -> S -> T -> S * T
s /\ t = s , t

module _ {k l}(S : Set k)(T : S -> Setoid l) where

  PI : Setoid (lmax k l)
  El PI     = (s : S) -> El (T s)
  Eq PI f g = (s : S) -> Eq (T s) (f s) (g s)
  Rf PI f s         = Rf (T s) (f s)
  Sy PI f g q s     = Sy (T s) (f s) (g s) (q s)
  Tr PI f g h p q s = Tr (T s) (f s) (g s) (h s) (p s) (q s)

  IM : Setoid (lmax k l)
  El IM     = {s : S} -> El (T s)
  Eq IM f g = (s : S) -> Eq (T s) (f {s}) (g {s})
  Rf IM f s         = Rf (T s) f
  Sy IM f g q s     = Sy (T s) f g (q s)
  Tr IM f g h p q s = Tr (T s) f g h (p s) (q s)

  SG : Setoid (lmax k l)
  El SG = S >< \ s -> El (T s)
  Eq SG (s0 , t0) (s1 , t1) = (s0 ~ s1) >< \ { r~ -> Eq (T s0) t0 t1 }
  Rf SG (s , t) = r~ , Rf (T s) t
  Sy SG (s0 , t0) (.s0 , t1) (r~ , q) = r~ , Sy (T s0) t0 t1 q
  fst (Tr SG (s0 , t0) (.s0 , t1) (s2 , t2) (r~ , q01) (q , q12)) = q
  snd (Tr SG (s0 , t0) (.s0 , t1) (.s0 , t2) (r~ , q01) (r~ , q12)) = Tr (T s0) t0 t1 t2 q01 q12

module _ {k l}(T : Setoid k)(P : El T -> Set l) where

  EX : Setoid (lmax k l)
  El EX = El T >< P
  Eq EX (t0 , _) (t1 , _) = Eq T t0 t1 * One l
  Rf EX (t , _) = Rf T t , <>
  Sy EX (t0 , _) (t1 , _) (q , <>) = Sy T t0 t1 q , <>
  Tr EX (t0 , _) (t1 , _) (t2 , _) (q01 , <>) (q12 , <>) =
    Tr T t0 t1 t2 q01 q12 , <>

module _ (k l : Level) where

  record Cat : Set (lsuc (lmax k l)) where
    field
      Obj  : Set k
      Arr  : Obj -> Obj -> Setoid l
    _~>_ : Obj -> Obj -> Set l
    S ~> T = El (Arr S T)
    _~~_ : {S T : Obj}(f g : S ~> T) -> Set l
    _~~_ {S}{T} = _|-_~~_ (Arr S T)
    field
      id   : {T : Obj} -> T ~> T
      _-_  : {R S T : Obj} -> R ~> S -> S ~> T -> R ~> T
      coex : {R S T : Obj}{f f' : R ~> S}{g g' : S ~> T} ->
             f ~~ f' -> g ~~ g' -> (f - g) ~~ (f' - g')
      idco : {S T : Obj}(f : S ~> T) -> (id - f) ~~ f
      coid : {S T : Obj}(f : S ~> T) -> (f - id) ~~ f
      coco : {R S T U : Obj}(f : R ~> S)(g : S ~> T)(h : T ~> U) ->
               (f - (g - h)) ~~ ((f - g) - h)

module _ (l : Level) where
  open Cat

  SET : Cat (lsuc l) l
  Obj  SET = Set l
  Arr  SET S T = PI S \ _ -> IN T
  id   SET x = x
  _-_  SET f g x = g (f x)
  qe (coex SET (eq qf) (eq qg)) x rewrite qf x = qg _
  qe (idco SET f) x = r~
  qe (coid SET f) x = r~
  qe (coco SET f g h) x = r~

module _ {l k l' k'}(C : Cat l k)(D : Cat l' k') where
  private module C = Cat C ; module D = Cat D

  Fun : Setoid (lmax l (lmax k (lmax l' k')))
  Fun = SG (C.Obj -> D.Obj) \ Map ->
        EX (IM C.Obj \ S -> IM C.Obj \ T ->
            PI (S C.~> T) \ _ -> D.Arr (Map S) (Map T)) \ map ->
        ({S T : C.Obj}{f g : S C.~> T} -> f C.~~ g -> map f D.~~ map g)
      * ({X : C.Obj} -> map (C.id {X}) D.~~ D.id {Map X})
      * ({R S T : C.Obj}(f : R C.~> S)(g : S C.~> T) ->
          map (f C.- g) D.~~ (map f D.- map g))

module _ (l k : Level) where

  CAT : Cat (lsuc (lmax l k)) (lmax l k)
  Cat.Obj CAT = Cat l k
  Cat.Arr CAT = Fun
  Cat.id CAT {C}
    = (\ X -> X) , (\ f -> f)
    , (\ q -> q)
    , rS
    , \ _ _ -> rS
    where open Cat C
  Cat._-_  CAT {C}{D}{E} (F , fm , fx , fi , fc) (G , gm , gx , gi , gc)
    = (\ X -> G (F X)) , (\ a -> gm (fm a))
    , (\ q -> gx (fx q))
    , (gm (fm C.id) ~[ gx fi >~
       gm (D.id)    ~[ gi >~
       E.id          [SQED])
    , \ f g ->
       gm (fm (f C.- g))         ~[ gx (fc _ _) >~
       gm (fm f D.- fm g)        ~[ gc _ _ >~
       (gm (fm f) E.- gm (fm g))  [SQED]
    where private module C = Cat C ; module D = Cat D ; module E = Cat E
  qe (Cat.coex CAT {C} {D} {E} {F , fm , fz} {F' , fm' , fz'} {G , gm , gx , gz} {G' , gm' , gz'}
     (eq (r~ , qf , <>)) (eq (r~ , qg , <>)))
     = r~
     , (\ S T f -> qe {X = Cat.Arr E (G (F S)) (G (F T))}
       (gm (fm f)    ~[ gx (eq (qf _ _ _)) >~
        gm (fm' f)   ~[ eq (qg _ _ _) >~
        gm' (fm' f)   [SQED]))
     , <>
  qe (Cat.idco CAT {C}{D} (F , fm , fz)) =
    r~ , (\ S T f -> qprf (D.Arr (F S) (F T)) rS) , <>
    where private module C = Cat C ; module D = Cat D
  qe (Cat.coid CAT {C} {D} (F , fm , fz)) =
    r~ , (\ S T f -> qprf (D.Arr (F S) (F T)) rS) , <>
    where private module C = Cat C ; module D = Cat D
  qe (Cat.coco CAT {B} {C} {D} {E} (F , fm , fz) (G , gm , gz) (H , hm , hz))
    = r~
    , (\ S T f -> qprf (Cat.Arr E (H (G (F S))) (H (G (F T)))) rS )
    , <>

module _ {l k l' k' : Level}(C : Cat l k)(D : Cat l' k') where
  private module C = Cat C ; module D = Cat D

  _=>_ : Cat (lmax l (lmax k (lmax l' k'))) (lmax l (lmax k k'))
  Cat.Obj _=>_ = El (Fun C D)
  Cat.Arr _=>_ (F , fm , _) (G , gm , _) =
    EX (IM C.Obj \ X -> D.Arr (F X) (G X)) \ n ->
    {S T : C.Obj}(f : S C.~> T) -> (fm f D.- n {T}) D.~~ (n {S} D.- gm f)
  Cat.id _=>_ {F , fm , _}
    = D.id
    , \ f ->
      fm f D.- D.id   ~[ D.coid _ >~
      fm f            ~< D.idco _ ]~
      (D.id D.- fm f)  [SQED]
  Cat._-_ _=>_ {F , fm , fx , fi , fc} {G , gm , gx , gi , gc} {H , hm , hx , hi , hc}
    (n , na) (p , pa)
    = n D.- p
    , \ f ->
      fm f D.- (n D.- p)   ~[ D.coco _ _ _ >~
      (fm f D.- n) D.- p   ~[ D.coex (na f) rS >~
      (n D.- gm f) D.- p   ~< D.coco _ _ _ ]~
      n D.- (gm f D.- p)   ~[ D.coex rS (pa f) >~
      n D.- (p D.- hm f)   ~[ D.coco _ _ _ >~
      ((n D.- p) D.- hm f   [SQED])
  qe (Cat.coex _=>_ (eq (nq , <>)) (eq (pq , <>)))
    = (\ X -> qe (D.coex (eq (nq X)) (eq (pq X))))
    , <>
  qe (Cat.idco _=>_ _) = (\ _ -> qe (D.idco _)) , <>
  qe (Cat.coid _=>_ _) = (\ _ -> qe (D.coid _)) , <>
  qe (Cat.coco _=>_ _ _ _) = (\ _ -> qe (D.coco _ _ _)) , <>

module _ {l k : Level}(C : Cat l k)(I : Cat.Obj C) where
  open Cat C

  _/_ : Cat (lmax l k) k
  Cat.Obj _/_ = Obj >< \ X -> X ~> I
  Cat.Arr _/_ (X , f) (Y , g) = EX (Arr X Y) \ h -> (h - g) ~~ f
  Cat.id _/_ = id , idco _
  Cat._-_ _/_ {R , r}{S , s}{T , t} (f , p) (g , q)
    = (f - g)
    , ((f - g) - t ~< coco _ _ _ ]~
       f - (g - t) ~[ coex rS q >~
       f - s ~[ p >~
       r [SQED])
  qe (Cat.coex _/_ (eq (q , <>)) (eq (q' , <>))) = qe (coex (eq q) (eq q')) , <>
  qe (Cat.idco _/_ _) = qe (idco _) , <>
  qe (Cat.coid _/_ _) = qe (coid _) , <>
  qe (Cat.coco _/_ _ _ _) = qe (coco _ _ _) , <>

module BWD (X : Set) where
  data Bwd : Set where
    _-,_ : Bwd -> X -> Bwd
    [] : Bwd
  infixl 30 _-,_

module _ {X : Set} where
  open BWD X

  data _<=_ : Bwd -> Bwd -> Set where
    _-^_ : forall {ga de} -> ga <= de -> forall x -> ga <= (de -, x)
    _-,_ : forall {ga de} -> ga <= de -> forall x -> (ga -, x) <= (de -, x)
    []   : [] <= []
  infixl 30 _-^_

  data <_-_>~_ : forall {ga de ze}(th : ga <= de)(ph : de <= ze)(ps : ga <= ze) -> Set where
    _-^_  : forall {ga de ze}{th : ga <= de}{ph : de <= ze}{ps : ga <= ze} ->
            < th - ph >~ ps -> forall x -> < th - ph -^ x >~ ps -^ x
    _-^,_ : forall {ga de ze}{th : ga <= de}{ph : de <= ze}{ps : ga <= ze} ->
            < th - ph >~ ps -> forall x -> < th -^ x - ph -, x >~ ps -^ x
    _-,_  : forall {ga de ze}{th : ga <= de}{ph : de <= ze}{ps : ga <= ze} ->
            < th - ph >~ ps -> forall x -> < th -, x - ph -, x >~ ps -, x
    []    : < [] - [] >~ []
  infix 25 <_-_>~_
  infixl 30 _-^,_

  io : forall {ga} -> ga <= ga
  io {ga -, x} = io {ga} -, x
  io {[]} = []

  mkCo : forall {ga de ze}(th : ga <= de)(ph : de <= ze) -> <(< th - ph >~_)>
  mkCo th         (ph -^ x) = let _ , v = mkCo th ph in _ , v -^ x
  mkCo (th -^ .x) (ph -, x) = let _ , v = mkCo th ph in _ , v -^, x
  mkCo (th -, .x) (ph -, x) = let _ , v = mkCo th ph in _ , v -, x
  mkCo []         []        = _ , []

  _~-~_ : forall {ga de ze}{th : ga <= de}{ph : de <= ze}{ps0 ps1 : ga <= ze} ->
          (v0 : < th - ph >~ ps0)(v1 : < th - ph >~ ps1) ->
          (ps0 ~ ps1) >< \ { r~ -> v0 ~ v1 }
  (v0 -^ x)  ~-~ (v1 -^ .x)   with r~ , r~ <- v0 ~-~ v1 = r~ , r~
  (v0 -^, x) ~-~ (v1 -^, .x)  with r~ , r~ <- v0 ~-~ v1 = r~ , r~
  (v0 -, x)  ~-~ (v1 -, .x)   with r~ , r~ <- v0 ~-~ v1 = r~ , r~
  []         ~-~ []                                     = r~ , r~

  _-<=_ : forall {ga de ze} -> ga <= de -> de <= ze -> ga <= ze
  th -<= ph = fst (mkCo th ph)

  io- : forall {ga de}(th : ga <= de) -> < io - th >~ th
  io- (th -^ x) = io- th -^ x
  io- (th -, x) = io- th -, x
  io- [] = []

  infixl 30 _-io
  _-io : forall {ga de}(th : ga <= de) -> < th - io >~ th
  th -^ x -io = th -io -^, x
  th -, x -io = th -io -, x
  [] -io = []

  assoc02 : forall {ga0 ga1 ga2 ga3}
              {th01 : ga0 <= ga1}{th23 : ga2 <= ga3}
              {th03 : ga0 <= ga3}{th12 : ga1 <= ga2} ->
              <(< th01 -_>~ th03)  :* (< th12 - th23 >~_)> ->
              <(< th01 - th12 >~_) :* (<_- th23 >~ th03)>
  assoc02 (v -^ .x & w -^ x) = let v' & w' = assoc02 (v & w) in v' & w' -^ x
  assoc02 (v -^ .x & w -^, x) = let v' & w' = assoc02 (v & w) in v' -^ x & w' -^, x
  assoc02 (v -^, .x & w -, x) = let v' & w' = assoc02 (v & w) in v' -^, x & w' -^, x
  assoc02 (v -, .x & w -, x) = let v' & w' = assoc02 (v & w) in v' -, x & w' -, x
  assoc02 ([] & []) = [] & []

  assoc03 : forall {ga0 ga1 ga2 ga3}
              {th01 : ga0 <= ga1}{th23 : ga2 <= ga3}
              {th02 : ga0 <= ga2}{th13 : ga1 <= ga3} ->
              <(< th01 -_>~ th02)  :* (<_- th23 >~ th13)> ->
              <(< th01 - th13 >~_) :* (< th02 - th23 >~_)>
  assoc03 {th01 = th}{th13 = ph} (v & w) with _ , v' <- mkCo th ph |
    v0 & v1 <- assoc02 (v' & w) | r~ , r~ <- v ~-~ v0 = v' & v1

  assoc13 : forall {ga0 ga1 ga2 ga3}
              {th01 : ga0 <= ga1}{th23 : ga2 <= ga3}
              {th03 : ga0 <= ga3}{th12 : ga1 <= ga2} ->
              <(< th01 - th12 >~_)  :* (<_- th23 >~ th03)> ->
              <(< th01 -_>~ th03) :* (< th12 - th23 >~_)>
  assoc13 {th23 = ph}{th12 = th} (v & w) with  _ , v' <- mkCo th ph |
    v0 & v1 <- assoc03 (v & v') | r~ , r~ <- w ~-~ v1 = v0 & v'

  THIN : Cat lzero lzero
  Cat.Obj  THIN = Bwd
  Cat.Arr  THIN ga de = IN (ga <= de)
  Cat.id   THIN = io
  Cat._-_  THIN = _-<=_
  Cat.coex THIN (eq r~) (eq r~) = eq r~
  Cat.idco THIN th with v <- io- th | _ , w <- mkCo io th | r~ , r~ <- v ~-~ w
    = rS
  Cat.coid THIN ph with v <- ph -io | _ , w <- mkCo ph io | r~ , r~ <- v ~-~ w
    = rS
  Cat.coco THIN th ph ps with thph , v <- mkCo th ph | phps , w <- mkCo ph ps |
    _ , v1 <- mkCo thph ps | _ , w1 <- mkCo th phps |
    v2 & w2 <- assoc02 (w1 & w) | r~ , r~ <- v ~-~ v2 | r~ , r~ <- v1 ~-~ w2
    = rS

  THIN/ : Bwd -> Cat lzero lzero
  Cat.Obj (THIN/ de) = <(_<= de)>
  Cat.Arr (THIN/ de) (_ , th0) (_ , th1) = EX (IN _) (<_- th1 >~ th0)
  Cat.id (THIN/ de) = io , io- _
  Cat._-_ (THIN/ de) (th0 , v0) (th1 , v1) with w0 & w1 <- assoc02 (v0 & v1)
    = _ , w1
  qe (Cat.coex (THIN/ de) {f = _ , v0} {._ , w0} {_ , v1} {._ , w1}
    (eq (r~ , <>)) (eq (r~ , <>))) with
    (r~ , r~) , (r~ , r~) <- v0 ~-~ w0 /\ v1 ~-~ w1
    = r~ , <>
  qe (Cat.idco (THIN/ de) {_ , ph} (th , v)) with
    w <- io- th | w' & _ <- assoc02 (io- ph & v) | r~ , r~ <- w ~-~ w'
    = r~ , <>
  qe (Cat.coid (THIN/ de) {T = _ , ph} (th , v)) with
    w <- th -io | w' & _ <- assoc02 (v & io- ph) | r~ , r~ <- w ~-~ w'
    = r~ , <>
  qe (Cat.coco (THIN/ de) (_ , v01) (_ , v12) (_ , v23)) with
    w13  & v13  <- assoc02 (v12 & v23) | w02  & v02  <- assoc02 (v01 & v12) |
    w013 & v013 <- assoc02 (v01 & v13) | w023 & v023 <- assoc02 (v02 & v23) |
    w013' & w023' <- assoc03 (w02 & w13) |
    (r~ , r~) , (r~ , r~) <- w013' ~-~ w013 /\ w023' ~-~ w023
    = r~ , <>

max_stars_repo_name: gallais/EGTBS

max_issues_repo_name: gallais/EGTBS

max_forks_repo_name: gallais/EGTBS


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

open import HoTT
open import groups.ExactSequence
open import homotopy.FunctionOver
open import homotopy.PtdAdjoint
open import homotopy.SuspAdjointLoop
open import cohomology.MayerVietoris
open import cohomology.Theory

{- Standard Mayer-Vietoris exact sequence (algebraic) derived from
 - the result in cohomology.MayerVietoris (topological).
 - This is a whole bunch of algebra which is not very interesting.
 -}

module cohomology.MayerVietorisExact {i} (CT : CohomologyTheory i)
  (n : ℤ) (ps : ⊙Span {i} {i} {i}) where

open MayerVietorisFunctions ps
module MV = MayerVietoris ps
open ⊙Span ps

open CohomologyTheory CT
open import cohomology.BaseIndependence CT
open import cohomology.Functor CT
open import cohomology.InverseInSusp CT
open import cohomology.LongExactSequence CT n ⊙reglue
open import cohomology.Wedge CT

mayer-vietoris-seq : HomSequence _ _
mayer-vietoris-seq =
  C n (⊙Pushout ps)
    ⟨ ×ᴳ-fanout (CF-hom n (⊙left ps)) (CF-hom n (⊙right ps)) ⟩→
  C n X ×ᴳ C n Y
    ⟨ ×ᴳ-fanin (C-is-abelian _ _) (CF-hom n f)
               (inv-hom _ (C-is-abelian _ _) ∘ᴳ (CF-hom n g)) ⟩→
  C n Z
    ⟨ CF-hom (succ n) ⊙extract-glue ∘ᴳ fst ((C-Susp n Z)⁻¹ᴳ) ⟩→
  C (succ n) (⊙Pushout ps)
    ⟨ ×ᴳ-fanout (CF-hom _ (⊙left ps)) (CF-hom _ (⊙right ps)) ⟩→
  C (succ n) X ×ᴳ C (succ n) Y ⊣|

mayer-vietoris-exact : is-exact-seq mayer-vietoris-seq
mayer-vietoris-exact =
  transport (λ {(r , s) → is-exact-seq s})
    (pair= _ $ sequence= _ _ $
      idp
        ∥⟨ ↓-over-×-in _→ᴳ_ idp (CWedge.⊙Wedge-rec-over n X Y _ _) ⟩∥
      CWedge.path n X Y
        ∥⟨ ↓-over-×-in' _→ᴳ_
             (ap↓ (λ φ → φ ∘ᴳ fst (C-Susp n (X ⊙∨ Y) ⁻¹ᴳ))
                  (CF-↓cod= (succ n) MV.ext-over)
              ∙ᵈ codomain-over-iso {χ = diff'} (codomain-over-equiv _ _))
             (CWedge.Wedge-hom-η n X Y _
              ▹ ap2 (×ᴳ-fanin (C-is-abelian n Z)) inl-lemma inr-lemma) ⟩∥
      ap (C (succ n)) MV.⊙path ∙ uaᴳ (C-Susp n Z)
        ∥⟨ ↓-over-×-in _→ᴳ_
            (CF-↓dom= (succ n) MV.cfcod-over
             ∙ᵈ domain-over-iso
                  (! (ap (λ h → CF _ ⊙extract-glue ∘ h)
                     (λ= (is-equiv.g-f (snd (C-Susp n Z)))))
                   ◃ domain-over-equiv _ _))
            idp                                              ⟩∥
      idp
        ∥⟨ ↓-over-×-in _→ᴳ_ idp (CWedge.⊙Wedge-rec-over (succ n) X Y _ _) ⟩∥
      CWedge.path (succ n) X Y ∥⊣|)
    long-cofiber-exact
  where
  {- shorthand -}
  diff' = fst (C-Susp n Z) ∘ᴳ CF-hom (succ n) MV.⊙mv-diff
                           ∘ᴳ fst (C-Susp n (X ⊙∨ Y) ⁻¹ᴳ)

  {- Variations on suspension axiom naturality -}
  natural-lemma₁ : {X Y : Ptd i} (n : ℤ) (f : X ⊙→ Y)
    → (fst (C-Susp n X) ∘ᴳ CF-hom _ (⊙Susp-fmap f)) ∘ᴳ fst (C-Susp n Y ⁻¹ᴳ)
      == CF-hom n f
  natural-lemma₁ {X} {Y} n f =
    ap (λ φ → φ ∘ᴳ fst (C-Susp n Y ⁻¹ᴳ)) (C-SuspF n f)
    ∙ group-hom= (λ= (ap (CF n f) ∘ is-equiv.f-g (snd (C-Susp n Y))))

  natural-lemma₂ : {X Y : Ptd i} (n : ℤ) (f : X ⊙→ Y)
    → CF-hom _ (⊙Susp-fmap f) ∘ᴳ fst (C-Susp n Y ⁻¹ᴳ)
      == fst (C-Susp n X ⁻¹ᴳ) ∘ᴳ CF-hom n f
  natural-lemma₂ {X} {Y} n f =
    group-hom= (λ= (! ∘ is-equiv.g-f (snd (C-Susp n X))
                 ∘ CF _ (⊙Susp-fmap f)
                 ∘ GroupHom.f (fst (C-Susp n Y ⁻¹ᴳ))))
    ∙ ap (λ φ → fst (C-Susp n X ⁻¹ᴳ) ∘ᴳ φ) (natural-lemma₁ n f)

  {- Associativity lemmas -}
  assoc-lemma : ∀ {i} {G H K L J : Group i}
    (φ : L →ᴳ J) (ψ : K →ᴳ L) (χ : H →ᴳ K) (ξ : G →ᴳ H)
    → (φ ∘ᴳ ψ) ∘ᴳ χ ∘ᴳ ξ == φ ∘ᴳ ((ψ ∘ᴳ χ) ∘ᴳ ξ)
  assoc-lemma _ _ _ _ = group-hom= idp

  assoc-lemma₂ : ∀ {i} {G H K L J : Group i}
    (φ : L →ᴳ J) (ψ : K →ᴳ L) (χ : H →ᴳ K) (ξ : G →ᴳ H)
    → (φ ∘ᴳ ψ ∘ᴳ χ) ∘ᴳ ξ == φ ∘ᴳ ψ ∘ᴳ χ ∘ᴳ ξ
  assoc-lemma₂ _ _ _ _ = group-hom= idp

  inl-lemma : diff' ∘ᴳ CF-hom n (⊙projl X Y) == CF-hom n f
  inl-lemma =
    assoc-lemma₂
      (fst (C-Susp n Z)) (CF-hom (succ n) MV.⊙mv-diff)
      (fst (C-Susp n (X ⊙∨ Y) ⁻¹ᴳ)) (CF-hom n (⊙projl X Y))
    ∙ ap (λ φ → fst (C-Susp n Z) ∘ᴳ CF-hom (succ n) MV.⊙mv-diff ∘ᴳ φ)
         (! (natural-lemma₂ n (⊙projl X Y)))
    ∙ ! (assoc-lemma₂
           (fst (C-Susp n Z)) (CF-hom _ MV.⊙mv-diff)
           (CF-hom _ (⊙Susp-fmap (⊙projl X Y)))
           (fst (C-Susp n X ⁻¹ᴳ)))
    ∙ ap (λ φ → (fst (C-Susp n Z) ∘ᴳ φ) ∘ᴳ fst (C-Susp n X ⁻¹ᴳ))
         (! (CF-comp _ (⊙Susp-fmap (⊙projl X Y)) MV.⊙mv-diff))
    ∙ ap (λ φ → (fst (C-Susp n Z) ∘ᴳ φ) ∘ᴳ fst (C-Susp n X ⁻¹ᴳ))
         (CF-λ= (succ n) projl-mv-diff)
    ∙ natural-lemma₁ n f
    where
    {- Compute the left projection of mv-diff -}
    projl-mv-diff : (σz : fst (⊙Susp Z))
      → Susp-fmap (projl X Y) (MV.mv-diff σz)
        == Susp-fmap (fst f) σz
    projl-mv-diff = Susp-elim idp (merid (pt X)) $
      ↓-='-from-square ∘ λ z →
        (ap-∘ (Susp-fmap (projl X Y)) MV.mv-diff (merid z)
         ∙ ap (ap (Susp-fmap (projl X Y))) (MV.MVDiff.merid-β z)
         ∙ ap-∙ (Susp-fmap (projl X Y))
                (merid (winl (fst f z))) (! (merid (winr (fst g z))))
         ∙ (SuspFmap.merid-β (projl X Y) (winl (fst f z))
            ∙2 (ap-! (Susp-fmap _) (merid (winr (fst g z)))
                ∙ ap ! (SuspFmap.merid-β (projl X Y) (winr (fst g z))))))
        ∙v⊡ (vid-square {p = merid (fst f z)}
             ⊡h rt-square (merid (pt X)))
        ⊡v∙ (∙-unit-r _ ∙ ! (SuspFmap.merid-β (fst f) z))

  inr-lemma : diff' ∘ᴳ CF-hom n (⊙projr X Y)
                           == inv-hom _ (C-is-abelian n Z) ∘ᴳ CF-hom n g
  inr-lemma =
    assoc-lemma₂
      (fst (C-Susp n Z)) (CF-hom (succ n) MV.⊙mv-diff)
      (fst (C-Susp n (X ⊙∨ Y) ⁻¹ᴳ)) (CF-hom n (⊙projr X Y))
    ∙ ap (λ φ → fst (C-Susp n Z) ∘ᴳ CF-hom (succ n) MV.⊙mv-diff ∘ᴳ φ)
         (! (natural-lemma₂ n (⊙projr X Y)))
    ∙ ! (assoc-lemma₂
           (fst (C-Susp n Z)) (CF-hom _ MV.⊙mv-diff)
           (CF-hom _ (⊙Susp-fmap (⊙projr X Y)))
           (fst (C-Susp n Y ⁻¹ᴳ)))
    ∙ ap (λ φ → (fst (C-Susp n Z) ∘ᴳ φ) ∘ᴳ fst (C-Susp n Y ⁻¹ᴳ))
         (! (CF-comp _ (⊙Susp-fmap (⊙projr X Y)) MV.⊙mv-diff))
    ∙ ∘ᴳ-assoc (fst (C-Susp n Z))
        (CF-hom _ (⊙Susp-fmap (⊙projr X Y) ⊙∘ MV.⊙mv-diff))
        (fst (C-Susp n Y ⁻¹ᴳ))
    ∙ ap (λ φ → fst (C-Susp n Z) ∘ᴳ φ ∘ᴳ fst (C-Susp n Y ⁻¹ᴳ))
         (CF-λ= (succ n) projr-mv-diff)
    ∙ ap (λ φ → fst (C-Susp n Z) ∘ᴳ φ ∘ᴳ fst (C-Susp n Y ⁻¹ᴳ))
         (CF-comp _ (⊙Susp-fmap g) (⊙Susp-flip Z))
    ∙ ! (assoc-lemma (fst (C-Susp n Z)) (CF-hom _ (⊙Susp-flip Z))
                     (CF-hom _ (⊙Susp-fmap g)) (fst (C-Susp n Y ⁻¹ᴳ)))
    ∙ ap (λ φ → (fst (C-Susp n Z) ∘ᴳ φ)
                ∘ᴳ CF-hom _ (⊙Susp-fmap g) ∘ᴳ fst (C-Susp n Y ⁻¹ᴳ))
         (C-Susp-flip-is-inv (succ n))
    ∙ ap (λ φ → φ ∘ᴳ CF-hom _ (⊙Susp-fmap g) ∘ᴳ fst (C-Susp n Y ⁻¹ᴳ))
         (inv-hom-natural (C-is-abelian _ _) (C-is-abelian _ _)
           (fst (C-Susp n Z)))
    ∙ assoc-lemma (inv-hom _ (C-is-abelian n Z)) (fst (C-Susp n Z))
                  (CF-hom _ (⊙Susp-fmap g)) (fst (C-Susp n Y ⁻¹ᴳ))
    ∙ ap (λ φ → inv-hom _ (C-is-abelian n Z) ∘ᴳ φ) (natural-lemma₁ n g)
    where
    {- Compute the right projection of mv-diff -}
    projr-mv-diff : (σz : fst (⊙Susp Z))
      → Susp-fmap (projr X Y) (MV.mv-diff σz)
        == Susp-fmap (fst g) (Susp-flip σz)
    projr-mv-diff = Susp-elim (merid (pt Y)) idp $
      ↓-='-from-square ∘ λ z →
        (ap-∘ (Susp-fmap (projr X Y)) MV.mv-diff (merid z)
         ∙ ap (ap (Susp-fmap (projr X Y))) (MV.MVDiff.merid-β z)
         ∙ ap-∙ (Susp-fmap (projr X Y))
             (merid (winl (fst f z))) (! (merid (winr (fst g z))))
         ∙ (SuspFmap.merid-β (projr X Y) (winl (fst f z))
            ∙2 (ap-! (Susp-fmap (projr X Y))
                  (merid (winr (fst g z)))
                ∙ ap ! (SuspFmap.merid-β (projr X Y) (winr (fst g z))))))
        ∙v⊡ ((lt-square (merid (pt Y))
             ⊡h vid-square {p = ! (merid (fst g z))}))
        ⊡v∙ ! (ap-∘ (Susp-fmap (fst g)) Susp-flip (merid z)
               ∙ ap (ap (Susp-fmap (fst g))) (FlipSusp.merid-β z)
               ∙ ap-! (Susp-fmap (fst g)) (merid z)
               ∙ ap ! (SuspFmap.merid-β (fst g) z))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module x03relations where

import      Relation.Binary.PropositionalEquality as Eq
open        Eq                  using (_≡_; refl; cong; sym)
open import Data.Nat            using (ℕ; zero; suc; _+_; _*_)
open import Data.Nat.Properties using (+-comm; +-identityʳ; *-comm; +-suc)

{-
------------------------------------------------------------------------------
-- DEFINING RELATIONS : INEQUALITY ≤

z≤n --------
    zero ≤ n

        m ≤     n
s≤s -------------
    suc m ≤ suc n
-}

-- INDEXED datatype : the type m ≤ n is indexed by two naturals, m and n
data _≤_ : ℕ → ℕ → Set where

  -- base case holds for all naturals
  z≤n : ∀ {n : ℕ}    -- IMPLICIT args
      --------
    → zero ≤ n

  -- inductive case holds if m ≤ n
  s≤s : ∀ {m n : ℕ}  -- IMPLICIT args
    →     m ≤     n
      -------------
    → suc m ≤ suc n

{-
proof 2 ≤ 4

  z≤n -----
      0 ≤ 2
 s≤s -------
      1 ≤ 3
s≤s ---------
      2 ≤ 4
-}

_ : 2 ≤ 4
_ = s≤s (s≤s z≤n) -- no explicit 'n'     arg  to z≤n because implicit
                  -- no explicit 'm' 'n' args to s≤s because implicit

-- can be explicit

_ : 2 ≤ 4 -- with implicit args
_ = s≤s {1} {3} (s≤s {0} {2} (z≤n {2}))

_ : 2 ≤ 4 -- with named implicit args
_ = s≤s {m = 1} {n = 3} (s≤s {m = 0} {n = 2} (z≤n {n = 2}))

_ : 2 ≤ 4 -- with some implicit named args
_ = s≤s {n = 3} (s≤s {n = 2} z≤n)

-- infer explicit term via _
-- e.g., +-identityʳ variant with implicit arguments
+-identityʳ′ : ∀ {m : ℕ} → m + zero ≡ m
+-identityʳ′ = +-identityʳ _ -- agda infers _ from context (if it can)

-- precedence

infix 4 _≤_

------------------------------------------------------------------------------
-- DECIDABILITY : can compute ≤ : see Chapter Decidable

{-
------------------------------------------------------------------------------
-- INVERSION

above def goes from smaller to larger things (e.g., m ≤ n to suc m ≤ suc n)

sometimes go from bigger to smaller things.

only one way to prove suc m ≤ suc n, for any m n

use it to invert rule
-}

inv-s≤s : ∀ {m n : ℕ}
  → suc m ≤ suc n
    -------------
  →     m ≤     n
inv-s≤s (s≤s m≤n) = m≤n
{-           ^
          variable name  (m ≤ n (with spaces) is a type)

m≤n is of type m ≤ n

convention : var name from type

not every rule is invertible
e.g., rule for z≤n has no non-implicit hypotheses, so nothing to invert

another example inversion
-}

inv-z≤n : ∀ {m : ℕ}
  → m ≤ zero
    --------
  → m ≡ zero -- only one way a number can be ≤ zero
inv-z≤n z≤n = refl

{-
------------------------------------------------------------------------------
-- PROPERTIES OF ORDERING RELATIONS

- REFLEXIVE       : ∀ n    , n ≤ n
- TRANSITIVE      : ∀ m n p, if m ≤ n && n ≤ p then m ≤ p
- ANTI-SYMMETRIC  : ∀ m n  , if m ≤ n && n ≤ m then m ≡ n
- TOTAL           : ∀ m n  , either m ≤ n or n ≤ m

_≤_ satisfies all 4

names for some combinations:

PREORDER      : reflexive and transitive
PARTIAL ORDER : preorder      that is also anti-symmetric
TOTAL ORDER   : partial order that is also total

Exercise orderings (practice)

preorder that is not a partial order:

-- https://math.stackexchange.com/a/2217969

partial order that is not a total order:

-- https://math.stackexchange.com/a/367590

-- other properties

- SYMMETRIC : ∀ x y, if x R y then y R x

------------------------------------------------------------------------------
REFLEXIVITY
-}

-- proof is via induction on implicit arg n
≤-refl : ∀ {n : ℕ} -- implicit arg to make it easier to invoke
    -----
  → n ≤ n

≤-refl {zero}  = z≤n        -- zero  ≤ zero
-- inductive case applies IH '≤-refl {n}' for a proof of n ≤ n to 's≤s' giving proof suc n ≤ suc n
≤-refl {suc n} = s≤s ≤-refl -- suc n ≤ suc n

{-
------------------------------------------------------------------------------
TRANSITIVITY
-}

-- inductive proof using evidence m ≤ n
≤-trans : ∀ {m n p : ℕ}
  → m ≤ n
  → n ≤ p
    -----
  → m ≤ p

-- base
-- 1st first inequality holds by z≤n
--            v
≤-trans      z≤n         _  = z≤n
{-                       ^     ^
                         |     now must show zero ≤ p; follows by z≤n
n ≤ p case is irrelevant (written _)

-}

{-
inductive
-- 1st inequality
--          |     2nd inequality
            v         v -}
≤-trans (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans m≤n n≤p)
{-
1st proves
   suc m ≤ suc n
2nd proves
           suc n ≤ suc p
must now show
   suc m         ≤ suc p

IH '≤-trans m≤n n≤p' establishes m ≤ p

goal follows by applying s≤s

≤-trans (s≤s m≤n) z≤n case cannot arise since
- 1st inequality implies middle value is suc n
- 2nd inequality implies that it is zero

-}

≤-trans′ : ∀ (m n p : ℕ) -- ALTERNATIVE with explicit args
  → m ≤ n
  → n ≤ p
    -----
  → m ≤ p
≤-trans′   zero       _       _       z≤n         _  = z≤n
≤-trans′ (suc m) (suc n) (suc p) (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans′ m n p m≤n n≤p)

{-
technique of induction on evidence that a property holds
- e.g., inducting on evidence that m ≤ n
rather than induction on values of which the property holds
- e.g., inducting on m
is often used

------------------------------------------------------------------------------
ANTI-SYMMETRY
-}

-- 842
-- proof via rewrite
≤-antisym' : ∀ {m n : ℕ}
  → m ≤ n
  → n ≤ m
    -----
  → m ≡ n
≤-antisym'      z≤n       z≤n  = refl
≤-antisym' (s≤s m≤n) (s≤s n≤m) rewrite ≤-antisym' m≤n n≤m = refl

-- proof via induction over the evidence that m ≤ n and n ≤ m hold
≤-antisym : ∀ {m n : ℕ}
  → m ≤ n
  → n ≤ m
    -----
  → m ≡ n
≤-antisym      z≤n       z≤n  = refl
≤-antisym (s≤s m≤n) (s≤s n≤m) = cong suc (≤-antisym m≤n n≤m)

{-
base : both inequalities hold by z≤n
- so given zero ≤ zero and zero ≤ zero
- shows zero ≡ zero (via Reflexivity of equality)

inductive
- after using evidence for 1st and 2nd inequalities
- have suc m ≤ suc n and suc n ≤ suc m
- must show suc m ≡ suc n
- IH '≤-antisym m≤n n≤m' establishes m ≡ n
- goal follows by congruence

Exercise ≤-antisym-cases (practice) TODO : describe why missing case OK

The above proof omits cases where one argument is z≤n and one argument is s≤s.
Why is it ok to omit them?

-- Your code goes here

------------------------------------------------------------------------------
TOTAL
-}

-- datatype with PARAMETERS
data Total (m n : ℕ) : Set where

  forward :
      m ≤ n
      ---------
    → Total m n

  flipped :
      n ≤ m
      ---------
    → Total m n

{-
Evidence that Total m n holds is either of the form
- forward m≤n or
- flipped n≤m
where m≤n and n≤m are evidence of m ≤ n and n ≤ m respectively

(above definition could also be written as a disjunction; see Chapter Connectives.)

above data type uses PARAMETERS m n --- equivalent to following INDEXED datatype:
-}

data Total′ : ℕ → ℕ → Set where

  forward′ : ∀ {m n : ℕ}
    → m ≤ n
      ----------
    → Total′ m n

  flipped′ : ∀ {m n : ℕ}
    → n ≤ m
      ----------
    → Total′ m n

{-
Each parameter of the type translates as an implicit parameter of each constructor.
Unlike an indexed datatype, where the indexes can vary (as in zero ≤ n and suc m ≤ suc n),
in a parameterised datatype the parameters must always be the same (as in Total m n).

Parameterised declarations are shorter, easier to read,
and occasionally aid Agda’s termination checker.
Use them in preference to indexed types when possible.

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

show ≤ is a total order by induction over 1st and 2nd args

uses WITH
-}

≤-total : ∀ (m n : ℕ) → Total m n

-- base : 1st arg zero so forward case holds with z≤n as evidence that zero ≤ n
≤-total   zero       n = forward z≤n

-- base : 2nd arg zero so flipped case holds with z≤n as evidence that zero ≤ suc m
≤-total (suc m)   zero = flipped z≤n

-- inductive : IH establishes one of
≤-total (suc m) (suc n) with ≤-total m n
-- forward case of IH with m≤n as evidence that m ≤ n
-- follows that forward case of prop holds with s≤s m≤n as evidence that suc m ≤ suc n
... | forward m≤n = forward (s≤s m≤n)
-- flipped case of IH with n≤m as evidence that n ≤ m
-- follows that flipped case of prop holds with s≤s n≤m as evidence that suc n ≤ suc m
... | flipped n≤m = flipped (s≤s n≤m)

{-
WITH expression and one or more subsequent lines
each line begins ... | followed by pattern and right-hand side

WITH equivalent to defining a helper function:
-}

≤-total′ : ∀ (m n : ℕ) → Total m n
≤-total′   zero       n  = forward z≤n
≤-total′ (suc m)   zero  = flipped z≤n
≤-total′ (suc m) (suc n) = helper (≤-total′ m n)
 where
  helper : Total m n → Total (suc m) (suc n)
  helper (forward m≤n) = forward (s≤s m≤n)
  helper (flipped n≤m) = flipped (s≤s n≤m)

{-
WHERE

vars bound on the left-hand side of the preceding equation (e.g., m n) in scope in nested def
any identifiers bound in nested definition (e.g., helper)
in scope in right-hand side of preceding equation

If both arguments are equal, then both cases hold and we could return evidence of either.
In the code above we return the forward case, but there is a variant that returns the flipped case:
-}

≤-total″ : ∀ (m n : ℕ) → Total m n
≤-total″      m    zero  = flipped z≤n
≤-total″   zero  (suc n) = forward z≤n
≤-total″ (suc m) (suc n) with ≤-total″ m n
... | forward m≤n = forward (s≤s m≤n)
... | flipped n≤m = flipped (s≤s n≤m)

-- differs from original : pattern matches on 2nd arg before 1st

{-
------------------------------------------------------------------------------
MONOTONICITY ∀ {m n p q : ℕ} → m ≤ n → p ≤ q → m + p ≤ n + q

addition is monotonic on the right
proof by induction on 1st arg
-}

+-monoʳ-≤ : ∀ (n p q : ℕ)
  →     p ≤     q
    -------------
  → n + p ≤ n + q
-- base      : 1st is zero;        zero + p  ≤   zero + q
--                  def/eq                p  ≤          q
-- evidence given by arg p≤q
+-monoʳ-≤ zero    p q p≤q  =  p≤q
-- inductive : 1st is suc n;      suc n + p  ≤  suc n + q
--                  def/eq;      suc (n + p) ≤ suc (n + q)
-- IH +-monoʳ-≤ n p q p≤q establishes n + p ≤ n + q
-- goal follows by applying s≤s
+-monoʳ-≤ (suc n) p q p≤q  =  s≤s (+-monoʳ-≤ n p q p≤q)

{-
addition is monotonic on the left
via previous result and commutativity of addition:
-}
+-monoˡ-≤ : ∀ (m n p : ℕ)
  → m     ≤ n
    -------------
  → m + p ≤ n + p
+-monoˡ-≤ m n p m≤n         -- m + p ≤ n + p
  rewrite
    +-comm m p              -- p + m ≤ n + p
  | +-comm n p              -- p + m ≤ p + n
 = +-monoʳ-≤ p m n m≤n

-- combine above results:

+-mono-≤ : ∀ (m n p q : ℕ)
  → m     ≤ n
  →     p ≤     q
    -------------
  → m + p ≤ n + q
+-mono-≤ m n p q m≤n p≤q
  = ≤-trans               -- combining below via transitivity proves m + p ≤ n + q
    (+-monoˡ-≤ m n p m≤n) -- proves m + p ≤ n + p
    (+-monoʳ-≤ n p q p≤q) -- proves n + p ≤ n + q

{-
------------------------------------------------------------------------------
Exercise *-mono-≤ (stretch) Show that multiplication is monotonic with regard to inequality.
-}
-------------------------
-- multiplication is monotonic on the right
*-monoʳ-≤ : ∀ (n p q : ℕ)
  →     p ≤     q
    -------------
  → n * p ≤ n * q

*-monoʳ-≤ zero p q p≤q          --  zero * p ≤  zero * q
                                --  zero     ≤  zero
  = z≤n

*-monoʳ-≤ n zero q p≤q          --  n * zero ≤ n * q
  rewrite
    *-comm n zero               --         0 ≤ n * q
  = z≤n

*-monoʳ-≤ n p zero p≤q          --     n * p ≤ n * zero
  rewrite
    *-comm n zero               --     n * p ≤ 0
  | inv-z≤n p≤q                 --     n * 0 ≤ 0
  | *-comm n zero               --         0 ≤ 0
  = z≤n

*-monoʳ-≤ n (suc p) (suc q) p≤q -- n * suc p ≤ n * suc q
  rewrite
    *-comm n (suc p)            -- n + p * n ≤ n * suc q
  | *-comm n (suc q)            -- n + p * n ≤ n + q * n
  | *-comm p n                  -- n + n * p ≤ n + q * n
  | *-comm q n                  -- n + n * p ≤ n + n * q
  = +-monoʳ-≤ n (n * p) (n * q) (*-monoʳ-≤ n p q (inv-s≤s p≤q))

-------------------------
-- multiplication is monotonic on the left
*-monoˡ-≤ : ∀ (m n p : ℕ)
  → m     ≤ n
    -------------
  → m * p ≤ n * p

*-monoˡ-≤ zero n p m≤n          --  zero * p ≤ n * p
                                --  zero     ≤ n * p
  = z≤n

*-monoˡ-≤ m zero p m≤n          --     m * p ≤ zero * p
                                --     m * p ≤ zero
  rewrite inv-z≤n m≤n           --     0 * p ≤ 0
                                --      zero ≤ 0
  = z≤n

*-monoˡ-≤ (suc m) (suc n) p m≤n -- suc m * p ≤ suc n * p
                                -- p + m * p ≤ p + n * p
  = +-monoʳ-≤ p (m * p) (n * p) (*-monoˡ-≤ m n p (inv-s≤s m≤n))

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

*-mono-≤ : ∀ (m n p q : ℕ)
  → m     ≤ n
  →     p ≤     q
    -------------
  → m * p ≤ n * q
*-mono-≤ m n p q m≤n p≤q
  = ≤-trans
    (*-monoˡ-≤ m n p m≤n)
    (*-monoʳ-≤ n p q p≤q)

{-
------------------------------------------------------------------------------
STRICT INEQUALITY <
-}

infix 4 _<_

data _<_ : ℕ → ℕ → Set where

  z<s : ∀ {n : ℕ}
      ------------
    → zero < suc n -- diff from '≤' : 'zero ≤ n'

  s<s : ∀ {m n : ℕ}
    →     m <     n
      -------------
    → suc m < suc n

{-
NOT REFLEXIVE

IRREFLEXIVE : n < n never holds for any n

TRANSITIVE

NOT TOTAL

TRICHOTOMY: ∀ m n, one of m < n, m ≡ n, or m > n holds
- where m > n hold when n < m

MONOTONIC with regards to ADDITION and MULTIPLICATION

negation required to prove (so deferred to Chapter Negation)
- irreflexivity
- trichotomy case are mutually exclusive

------------------------------------------------------------------------------
show suc m ≤ n implies m < n (and conversely)
-}

m≤n→m<n : ∀ {m n : ℕ}
        → suc m ≤ n
          ---------
        →     m < n
m≤n→m<n  {zero}  {zero} ()
m≤n→m<n  {zero} {suc n} m≤n = z<s
m≤n→m<n {suc m} {suc n} m≤n = s<s (m≤n→m<n {m} {n} (inv-s≤s m≤n))

inv-s<s : ∀ {m n : ℕ}
        → suc m < suc n
          -------------
        →     m <     n
inv-s<s (s<s m<n) = m<n

m<n→m≤n : ∀ {m n : ℕ}
        → m < n
        → m ≤ n
m<n→m≤n  {zero} {suc n} m<n = z≤n
m<n→m≤n {suc m} {suc n} m<n = s≤s (m<n→m≤n {m} {n} (inv-s<s m<n))

{-
can then give an alternative derivation of the properties of strict inequality
(e.g., transitivity) by exploiting the corresponding properties of inequality

------------------------------------------------------------------------------
Exercise <-trans (recommended) : strict inequality is transitive.
-}

<-trans : ∀ {m n p : ℕ}
  → m < n
  → n < p
    -----
  → m < p
<-trans  {zero}     {n}     {p}      z<s  (s<s n<p) = z<s
<-trans {suc m} {suc n} {suc p} (s<s m<n) (s<s n<p) = s<s (<-trans {m} {n} {p} m<n n<p)

<-trans' : ∀ {m n p : ℕ}
  → m < n
  → n < p
    -----
  → m < p
<-trans'      z<s  (s<s n<p) = z<s
<-trans' (s<s m<n) (s<s n<p) = s<s (<-trans' m<n n<p)

{-
------------------------------------------------------------------------------
Exercise trichotomy (practice)

Show that strict inequality satisfies a weak version of trichotomy,
in the sense that for any m and n that one of the following holds:
- m < n
- m ≡ n
- m > n

Define m > n to be the same as n < m.

Need a data declaration, similar to that used for totality.
(Later will show that the three cases are exclusive after negation is introduced.)
-}

-- from 842
data Trichotomy (m n : ℕ) : Set where
  is-< : m < n → Trichotomy m n
  is-≡ : m ≡ n → Trichotomy m n
  is-> : n < m → Trichotomy m n

-- hc
<-trichotomy : ∀ (m n : ℕ) → Trichotomy m n
<-trichotomy   zero    zero  = is-≡ refl
<-trichotomy   zero  (suc n) = is-< z<s
<-trichotomy (suc m)   zero  = is-> z<s
<-trichotomy (suc m) (suc n) = helper (<-trichotomy m n)
 where
  helper : Trichotomy m n -> Trichotomy (suc m) (suc n)
  helper (is-< x) = is-< (s<s x)
  helper (is-≡ x) = is-≡ (cong suc x)
  helper (is-> x) = is-> (s<s x)

{-
------------------------------------------------------------------------------
Exercise +-mono-< (practice)

Show that addition is monotonic with respect to strict inequality.
As with inequality, some additional definitions may be required.
-}

-- HC
-- these proof are literal cut/paste/change '≤' to '<'
-- no additional defs were required

+-monoʳ-< : ∀ (n p q : ℕ)
  → p < q
    -------------
  → n + p < n + q
+-monoʳ-< zero    p q p<q  =  p<q
+-monoʳ-< (suc n) p q p<q  =  s<s (+-monoʳ-< n p q p<q)

+-monoˡ-< : ∀ (m n p : ℕ)
  → m < n
    -------------
  → m + p < n + p
+-monoˡ-< m n p m<n
  rewrite
    +-comm m p
  | +-comm n p
 = +-monoʳ-< p m n m<n

+-mono-< : ∀ (m n p q : ℕ)
  → m < n
  → p < q
    -------------
  → m + p < n + q
+-mono-< m n p q m<n p<q
  = <-trans
    (+-monoˡ-< m n p m<n)
    (+-monoʳ-< n p q p<q)

{-
------------------------------------------------------------------------------
Exercise ≤-iff-< (recommended) : suc m ≤ n implies m < n, and conversely
-}

-- 842 exercise: LEtoLTS (1 point) ≤-<-to

m≤n→m<sucn : ∀ {m n : ℕ}
  → m ≤     n
  → m < suc n
m≤n→m<sucn  {zero}         m≤n = z<s
m≤n→m<sucn {suc m} {suc n} m≤n = s<s (m≤n→m<sucn {m} {n} (inv-s≤s m≤n))

-- 842 exercise: LEStoLT (1 point) ≤-<--to′

sucm≤n→m<n : ∀ {m n : ℕ}
  → suc m ≤ n
  →     m < n
sucm≤n→m<n  {zero} {suc n} sucm≤n = z<s
sucm≤n→m<n {suc m} {suc n} sucm≤n = s<s (sucm≤n→m<n {m} {n} (inv-s≤s sucm≤n))

-- 842 exercise: LTtoSLE (1 point) ≤-<-from

m<n→sucm≤n : ∀ {m n : ℕ}
  →     m < n
  → suc m ≤ n
m<n→sucm≤n  {zero} {suc n} m<n = s≤s z≤n
m<n→sucm≤n {suc m} {suc n} m<n = s≤s (m<n→sucm≤n {m} {n} (inv-s<s m<n))

-- 842 exercise: LTStoLE (1 point) ≤-<-from′

m<sucn→m≤n : ∀ {m n : ℕ}
  → m < suc n
  → m ≤     n
m<sucn→m≤n  {zero}              z<n  = z≤n
m<sucn→m≤n {suc m} {suc n} (s<s m<n) = s≤s (m<sucn→m≤n {m} {n} m<n)
--                          ^
--                   critical move

{-
------------------------------------------------------------------------------
Exercise <-trans-revisited (practice)

Give an alternative proof that strict inequality is transitive,
using the relation between strict inequality and inequality
and the fact that inequality is transitive.

-- 842: use the above to give a proof of <-trans that uses ≤-trans
-}

n<p→n<sucp : ∀ {n p : ℕ}
  → n <     p
  → n < suc p
n<p→n<sucp                 z<s = z<s
n<p→n<sucp {suc n} {suc p} n<p = s<s (n<p→n<sucp {n} {p} (inv-s<s n<p))

<-trans'' : ∀ {m n p : ℕ}
  → m < n
  → n < p
    -----
  → m < p
<-trans''  {zero} {suc n} {suc p}      z<s         _  = z<s
<-trans'' {suc m} {suc n} {suc p} (s<s m<n) (s<s n<p)
  = sucm≤n→m<n
      (≤-trans (m<n→sucm≤n (s<s             m<n))
               (m<sucn→m≤n (s<s (n<p→n<sucp n<p))))

{-
------------------------------------------------------------------------------
EVEN and ODD : MUTUALLY RECURSIVE DATATYPE DECLARATION and OVERLOADED CONSTRUCTORS

inequality and strict inequality are BINARY RELATIONS

even and odd are UNARY RELATIONS, sometimes called PREDICATES
-}

-- identifier must be defined before it is used, so declare both before giving constructors.
data even : ℕ → Set
data odd  : ℕ → Set

data even where

  zero :           -- overloaded with nat def
      ---------
      even zero

  suc  : ∀ {n : ℕ}
    → odd       n
      ------------
    → even (suc n)

data odd where

  suc  : ∀ {n : ℕ} -- suc is overloaded with one above and nat def
    → even     n
      -----------
    → odd (suc n)
{-
overloading constructors is OK (handled by type inference
overloading defined names NOT OK
best practice : only overload related meanings
-}

-- mutually recursive proof functions : give types first, then impls

-- sum of two even numbers is even
e+e≡e : ∀ {m n : ℕ}
  → even m
  → even n
    ------------
  → even (m + n)

-- sum of even and odd is odd
o+e≡o : ∀ {m n : ℕ}
  → odd m
  → even n
    -----------
  → odd (m + n)

-- given: zero is evidence that 1st is even
-- given: 2nd is even
-- result: even because 2nd is even
e+e≡e zero     en = en
-- given: 1st is even because it is suc of odd
-- given: 2nd is even
-- result: even because it is suc of sum of odd and even number, which is odd
e+e≡e (suc om) en = suc (o+e≡o om en)

-- given: 1st odd because it is suc of even
-- given: 2nd is event
-- result: odd because it is suc of sum of two evens, which is even
o+e≡o (suc em) en = suc (e+e≡e em en)

------------------------------------------------------------------------------
-- Exercise o+o≡e (stretch) : sum of two odd numbers is even
-- 842 Hint: need to define another theorem and prove both by mutual induction

-- sum of odd and even is odd
e+o≡o : ∀ {m n : ℕ}
  → even m
  → odd n
    -----------
  → odd (m + n)

-- sum of odd and odd is even
o+o≡e : ∀ {m n : ℕ}
  → odd m
  → odd n
  --------------
  → even (m + n)

e+o≡o    zero  on = on
e+o≡o (suc em) on = suc (o+o≡e em on)

o+o≡e (suc om) on = suc (e+o≡o om on)

{-
------------------------------------------------------------------------------
Exercise Bin-predicates (stretch)

representations not unique due to leading zeros

eleven:
  ⟨⟩     I O I I --     canonical
  ⟨⟩ O O I O I I -- not canonical
-}

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

inc : Bin → Bin
inc  ⟨⟩    = ⟨⟩      I
inc (b  O) =      b  I
inc (b  I) = (inc b) O

to : ℕ → Bin
to   zero  = ⟨⟩ O
to (suc m) = inc (to m)

dbl : ℕ → ℕ
dbl   zero  = zero
dbl (suc m) = suc (suc (dbl m))

from : Bin → ℕ
from     ⟨⟩ = 0
from (b  O) =      dbl (from b)
from (b  I) = suc (dbl (from b))

-- httpS://www.reddit.com/r/agda/comments/hrvk07/plfa_quantifiers_help_with_binisomorphism/

-- holds if bitstring has a leading one
data One : Bin → Set where
  one    :                 One (⟨⟩ I)
  _withO : ∀ {b} → One b → One  (b O)
  _withI : ∀ {b} → One b → One  (b I)

{-
Hint: to prove below
- first state/prove properties of One
-}

n≤1+n : ∀ (n : ℕ) → n ≤ 1 + n
n≤1+n   zero  = z≤n
n≤1+n (suc n) = s≤s (n≤1+n n)

dbl-mono : ∀ (n : ℕ) → n ≤ dbl n
dbl-mono  zero   = z≤n
dbl-mono (suc n) = s≤s (≤-trans (dbl-mono n) (n≤1+n (dbl n)))

-- not used; I thought it would be useful; first try
n≤fromb→n≤dblfromb' : ∀ {n : ℕ} {b : Bin} → n ≤ from b → n ≤ dbl (from b)
n≤fromb→n≤dblfromb'  {zero} {b}        p  = z≤n
n≤fromb→n≤dblfromb' {suc n} {b O}      p  =
                ≤-trans p (dbl-mono      (from (b O)))
n≤fromb→n≤dblfromb' {suc n} {b I} (s≤s p) =
  s≤s (≤-trans (≤-trans p (dbl-mono (dbl (from b))))
               (n≤1+n (dbl (dbl (from b)))))

-- not used; above cleaned up
n≤fromb→n≤dblfromb : ∀ {n : ℕ} {b : Bin}
  → n ≤      from b
  → n ≤ dbl (from b)
n≤fromb→n≤dblfromb {_} {b} p = ≤-trans p (dbl-mono (from b))

-- HINT: prove if One b then 1 is less or equal to the result of from b
oneb→1≤fromb : ∀ {b : Bin} → One b → 1 ≤ from b
oneb→1≤fromb {b I}        _  = s≤s z≤n
oneb→1≤fromb {b O} (p withO) = ≤-trans (oneb→1≤fromb p) (dbl-mono (from b))

oneb→0<fromb : ∀ {b : Bin} → One b → 0 < from b
oneb→0<fromb p = m≤n→m<n (oneb→1≤fromb p)

-- not used
num-trailing-zeros : (b : Bin) {p : One b} → ℕ
num-trailing-zeros (b I)           = 0
num-trailing-zeros (b O) {p withO} = 1 + num-trailing-zeros b {p}

-- not used
do-dbls : ℕ -> ℕ
do-dbls   zero  = suc zero
do-dbls (suc n) = dbl (do-dbls n)
{-
xxx : {b : Bin} {n : ℕ}
  → (p : One b)
  →         n ≡ num-trailing-zeros b {p}
  → do-dbls n ≤ from b
xxx {⟨⟩ I}  {zero}       one  ntz = s≤s z≤n
xxx {b  I}  {zero} (ob withI) ntz = s≤s z≤n
xxx {b  O}  {zero} (ob withO) ntz = ≤-trans (oneb→1≤fromb ob) (dbl-mono (from b))
xxx {b  O} {suc n} (ob withO) ntz = {!!}
-}
-- bitstring is canonical if
data Can : Bin → Set where
  czero : Can (⟨⟩ O)  -- it consists of a single zero (representing zero)

  cone : ∀ {b : Bin}
    → One b           -- it has a leading one (representing a positive number)
      -----
    → Can b

{-
--------------------------------------------------
show that increment preserves canonical bitstrings
-}

oneb→one-incb : ∀ {b : Bin} → One b → One (inc b)
oneb→one-incb      one  =             one withO
oneb→one-incb (p withO) =               p withI
oneb→one-incb (p withI) = oneb→one-incb p withO

canb→canincb : ∀ {b : Bin}
  → Can      b
    ----------
  → Can (inc b)
canb→canincb {.(⟨⟩ O)}   czero  = cone one
canb→canincb       {b} (cone p) = cone (oneb→one-incb p)

{-
--------------------------------------------------
show that converting a natural to a bitstring always yields a canonical bitstring
-}

can-to-n : ∀ {n : ℕ} → Can (to n)
can-to-n  {zero} = czero
can-to-n {suc n} = canb→canincb (can-to-n {n})

{-
--------------------------------------------------
show that converting a canonical bitstring to a natural and back is the identity TODO
-}

ob→obO : ∀ {b : Bin} → One b → One (b O)
ob→obI : ∀ {b : Bin} → One b → One (b I)

ob→obI {.(⟨⟩ I)}     one  =           one withI
ob→obI {.(_ O)} (p withO) = ob→obO      p withI
ob→obI  {(b I)} (p withI) = ob→obI  {b} p withI

ob→obO {.(⟨⟩ I)}     one  =           one  withO
ob→obO {.(_ O)} (p withO) = (ob→obO     p) withO
ob→obO  {(b I)} (p withI) =  ob→obI {b} p  withO

dblb : Bin → Bin
dblb   ⟨⟩    = ⟨⟩
dblb  (⟨⟩ O) = ⟨⟩ O
dblb    b     = b O

dblbo : ∀ {b} → One b → Bin → Bin
dblbo _ b = b O

dblbc : ∀ {b} → Can b → Bin → Bin
dblbc   czero  _ = ⟨⟩ O
dblbc (cone _) b =  b O

xxxx : ∀ {b : Bin} {n : ℕ}
  → b ≡ (⟨⟩ I)
  → b ≡ to n
  → n ≡ 1
  → (⟨⟩ I O) ≡ to (dbl n)
xxxx p1 p2 p3 rewrite p3 = refl

xx : ∀ {b : Bin} → One b -> to (dbl (from b)) ≡ b O
xx      one  = refl
xx {b O} (p withO)              --             to (dbl (from (b O)))     ≡ ((b O) O)
                                --             to (dbl (dbl (from b)))   ≡ ((b O) O)
  rewrite
    sym (xx p)                  --             to (dbl (dbl (from b)))   ≡ (to (dbl (from b)) O)
  = {!!}
xx {b I} (p withI)              --             to (dbl (from (b I))      ≡ ((b I) O)
                                --   inc (inc (to (dbl (dbl (from b))))) ≡ ((b I) O)
  = {!!}

can-b→to-from-b≡b : ∀ {b : Bin}
  → Can      b
    ---------------
  → to (from b) ≡ b
can-b→to-from-b≡b             czero  = refl
can-b→to-from-b≡b {.⟨⟩ I} (cone one) = refl
can-b→to-from-b≡b {b O} (cone (p withO)) --      to (dbl (from b))  ≡ (b O)
  = xx p

can-b→to-from-b≡b {b I} (cone (p withI)) -- inc (to (dbl (from b))) ≡ (b I)
  rewrite xx p                           --                   (b I) ≡ (b I)
  = refl

{-
------------------------------------------------------------------------------
Standard library

defs in this chapter in standard library:

import Data.Nat using (_≤_; z≤n; s≤s)
import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym; ≤-total;
                                  +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)

------------------------------------------------------------------------------
Unicode

≤  U+2264  LESS-THAN OR EQUAL TO    (\<=, \le)
≥  U+2265  GREATER-THAN OR EQUAL TO (\>=, \ge)
ˡ  U+02E1  MODIFIER LETTER SMALL L  (\^l)
ʳ  U+02B3  MODIFIER LETTER SMALL R  (\^r)
-}

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

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

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


text:
module Data.Boolean.Numeral where

open import Data
open import Data.Boolean
open import Data.Boolean.Stmt
import      Lvl
open import Numeral.Natural
open import Numeral.Natural.Oper.Comparisons
open import Syntax.Number
open import Type

Bool-to-ℕ : Bool → ℕ
Bool-to-ℕ 𝐹 = 0
Bool-to-ℕ 𝑇 = 1

ℕ-to-Bool : (n : ℕ) → . ⦃ _ : IsTrue(n <? 2) ⦄ → Bool
ℕ-to-Bool 0 = 𝐹
ℕ-to-Bool 1 = 𝑇

instance
  Bool-from-ℕ : Numeral(Bool)
  Numeral.restriction-ℓ Bool-from-ℕ     = Lvl.𝟎
  Numeral.restriction   Bool-from-ℕ   n = IsTrue(n <? 2)
  num                 ⦃ Bool-from-ℕ ⦄ n = ℕ-to-Bool n


text:
module Lib.Vec where

open import Common.Nat
open import Lib.Fin
open import Common.Unit
import Common.List as List; open List using (List ; [] ; _∷_)

data Vec (A : Set) :  Nat → Set where
  _∷_ : {n : Nat} → A → Vec A n → Vec A (suc n)
  []  : Vec A zero

infixr 30 _++_

_++_ : {A : Set}{m n : Nat} → Vec A m → Vec A n → Vec A (m + n)
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

snoc : {A : Set}{n : Nat} → Vec A n → A → Vec A (suc n)
snoc []       e = e ∷ []
snoc (x ∷ xs) e = x ∷ snoc xs e

-- Recursive length.

length : {A : Set}{n : Nat} → Vec A n → Nat
length [] = zero
length (x ∷ xs) = 1 + length xs

length' : {A : Set}{n : Nat} → Vec A n → Nat
length' {n = n} _ = n

zipWith3 : ∀ {A B C D n} → (A → B → C → D) → Vec A n → Vec B n → Vec C n → Vec D n
zipWith3 f []       []       []       = []
zipWith3 f (x ∷ xs) (y ∷ ys) (z ∷ zs) = f x y z ∷ zipWith3 f xs ys zs

zipWith : ∀ {A B C n} → (A → B → C) → Vec A n → Vec B n → {u : Unit} → Vec C n
zipWith _ [] [] = []
zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys {u = unit}

_!_ : ∀ {A n} → Vec A n → Fin n → A
(x ∷ xs) ! fz   = x
(_ ∷ xs) ! fs n = xs ! n
[] ! ()

-- Update vector at index

_[_]=_ : {A : Set}{n : Nat} → Vec A n → Fin n → A → Vec A n
(a ∷ as) [ fz   ]= e = e ∷ as
(a ∷ as) [ fs n ]= e = a ∷ (as [ n ]= e)
[] [ () ]= e

map : ∀ {A B n}(f : A → B)(xs : Vec A n) → Vec B n
map f []        = []
map f (x ∷ xs) = f x ∷ map f xs

-- Vector to List, forget the length.

forgetL : {A : Set}{n : Nat} → Vec A n → List A
forgetL []       = []
forgetL (x ∷ xs) = x ∷ forgetL xs

-- List to Vector, "rem"member the length.

rem : {A : Set}(xs : List A) → Vec A (List.length xs)
rem [] = []
rem (x ∷ xs) = x ∷ rem xs

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Lens.Composition where

open import Prelude
open import Lens.Definition
open import Lens.Operators

infixr 9 _⋯_
_⋯_ : Lens A B → Lens B C → Lens A C
fst (ab ⋯ bc) xs = ac
  where
  ab-xs : LensPart _ _
  ab-xs = fst ab xs

  bc-ys : LensPart _ _
  bc-ys = fst bc (get ab-xs)

  ac : LensPart _ _
  get ac = get bc-ys
  set ac v = set ab-xs (set bc-ys v)
get-set (snd (ab ⋯ bc)) s v = cong (getter bc) (get-set (snd ab) s _) ; bc .snd .get-set (get (fst ab s)) v
set-get (snd (ab ⋯ bc)) s = cong (setter ab s) (set-get (snd bc) (get (fst ab s))) ; set-get (snd ab) s
set-set (snd (ab ⋯ bc)) s v₁ v₂ = set-set (snd ab) s _ _ ; cong (setter ab s) (cong (flip (setter bc) v₂) (get-set (snd ab) _ _) ; set-set (snd bc) _ _ _)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module InstanceArgumentsAmbiguous where

postulate A B : Set
          f : {{a : A}} → B
          a₁ a₂ : A

test : B
test = f

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import Basics
open import lib.Basics
open import Flat

module Axiom.C1 {@♭ i j : ULevel} (@♭ I : Type i) (@♭ R : I → Type j) where
    open import Axiom.C0 I R

    postulate C1 : (index : I) → R index

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A Categorical view of the Sum type (Right-biased)
------------------------------------------------------------------------

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

open import Level

module Data.Sum.Categorical.Right (a : Level) {b} (B : Set b) where

open import Data.Sum
open import Category.Functor
open import Category.Applicative
open import Category.Monad
open import Function
import Function.Identity.Categorical as Id

Sumᵣ : Set (a ⊔ b) → Set (a ⊔ b)
Sumᵣ A = A ⊎ B

functor : RawFunctor Sumᵣ
functor = record { _<$>_ = map₁ }

applicative : RawApplicative Sumᵣ
applicative = record
  { pure = inj₁
  ; _⊛_ = [ map₁ , const ∘ inj₂ ]′
  }

monadT : RawMonadT (_∘′ Sumᵣ)
monadT M = record
  { return = M.pure ∘′ inj₁
  ; _>>=_  = λ ma f → ma M.>>= [ f , M.pure ∘′ inj₂ ]′
  } where module M = RawMonad M

monad : RawMonad Sumᵣ
monad = monadT Id.monad

------------------------------------------------------------------------
-- Get access to other monadic functions

module _ {F} (App : RawApplicative {a ⊔ b} F) where

  open RawApplicative App

  sequenceA : ∀ {A} → Sumᵣ (F A) → F (Sumᵣ A)
  sequenceA (inj₂ a) = pure (inj₂ a)
  sequenceA (inj₁ x) = inj₁ <$> x

  mapA : ∀ {A B} → (A → F B) → Sumᵣ A → F (Sumᵣ B)
  mapA f = sequenceA ∘ map₁ f

  forA : ∀ {A B} → Sumᵣ A → (A → F B) → F (Sumᵣ B)
  forA = flip mapA

module _ {M} (Mon : RawMonad {a ⊔ b} M) where

  private App = RawMonad.rawIApplicative Mon

  sequenceM : ∀ {A} → Sumᵣ (M A) → M (Sumᵣ A)
  sequenceM = sequenceA App

  mapM : ∀ {A B} → (A → M B) → Sumᵣ A → M (Sumᵣ B)
  mapM = mapA App

  forM : ∀ {A B} → Sumᵣ A → (A → M B) → M (Sumᵣ B)
  forM = forA App


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

module ProMonoid where

open import Level
open import Algebra.Core using (Op₂)
open import Algebra.Definitions using (Congruent₂)
open import Algebra.Structures
open import Algebra.Bundles
open import Relation.Binary

-- Pre-ordered monoids, additively written

record ProMonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≼_
  infixl 7 _∙_
  field
    Carrier    : Set c
    _≈_        : Rel Carrier ℓ₁  -- The underlying equality.

    _≼_        : Rel Carrier ℓ₂  -- The relation.
    isPreorder : IsPreorder _≈_ _≼_

    _∙_        : Op₂ Carrier     -- The monoid operations.
    ε          : Carrier
    isMonoid   : IsMonoid _≈_ _∙_ ε

    ∙-mon      : Congruent₂ _≼_ _∙_

  open IsPreorder isPreorder public
    hiding (module Eq)

  module Eq where
    setoid : Setoid c ℓ₁
    setoid = record { isEquivalence = isEquivalence }

    open Setoid setoid public

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

  open IsMonoid isMonoid public -- using (∙-cong)
    hiding (reflexive; refl)

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


text:
-- Andreas, 2016-01-13, highlighting of import directives
-- {-# OPTIONS -v highlighting.names:100 -v scope.decl:70 -v tc.decl:10 #-}

module _ where

import Common.Product as Prod hiding (proj₁) -- proj₁ should be highlighted as field

open Prod using (_×_)                        -- _×_ should be highlighted as record type

module M (A : Set) = Prod
  using (_,_)                                -- highlighted as constructor
  renaming (proj₂ to snd)                    -- highlighted as projections

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Everything where

import Cubical.Data.BinNat
import Cubical.Data.Bool
import Cubical.Data.Empty
import Cubical.Data.Equality
import Cubical.Data.Fin
import Cubical.Data.Nat
import Cubical.Data.Nat.Algebra
import Cubical.Data.Nat.Order
import Cubical.Data.NatMinusOne
import Cubical.Data.NatMinusTwo
import Cubical.Data.NatPlusOne
import Cubical.Data.Int
import Cubical.Data.Sum
import Cubical.Data.Prod
import Cubical.Data.Unit
import Cubical.Data.Sigma
import Cubical.Data.DiffInt
import Cubical.Data.Group
import Cubical.Data.HomotopyGroup
import Cubical.Data.List
import Cubical.Data.Graph
import Cubical.Data.InfNat
import Cubical.Data.Queue

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


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

open import LogicalFormulae
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Functions.Definition
open import Setoids.Setoids
open import Setoids.Subset
open import Graphs.Definition

module Graphs.InducedSubgraph {a b c : _} {V' : Set a} {V : Setoid {a} {b} V'} (G : Graph c V) where

open Graph G

inducedSubgraph : {d : _} {pred : V' → Set d} (sub : subset V pred) → Graph c (subsetSetoid V sub)
Graph._<->_ (inducedSubgraph sub) (x , _) (y , _) = x <-> y
Graph.noSelfRelation (inducedSubgraph sub) (x , _) x=x = noSelfRelation x x=x
Graph.symmetric (inducedSubgraph sub) {x , _} {y , _} x=y = symmetric x=y
Graph.wellDefined (inducedSubgraph sub) {x , _} {y , _} {z , _} {w , _} x=y z=w x-z = wellDefined x=y z=w x-z


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

-- Andreas, 2016-12-19, issue #2344, reported by oinkium, shrunk by Ulf
-- The function Agda.TypeChecking.Telescope.permuteTel
-- used in the unifier was buggy.

-- {-# OPTIONS -v tc.meta:25 #-}
-- {-# OPTIONS -v tc.lhs:10 #-}
-- {-# OPTIONS -v tc.lhs.unify:100 #-}
-- {-# OPTIONS -v tc.cover:20 #-}

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

data Fin : Nat → Set where
  zero : ∀ n → Fin (suc n)

postulate
  T     : Nat → Set
  mkT   : ∀{l} → T l
  toNat : ∀ m → Fin m → Nat

-- The underscore in the type signature is originally dependent on A,X,i
-- but then pruned to be dependent on A,X only.
-- The unifier had a problem with this.
toNat-injective : ∀ (A : Set) X i → T (toNat _ i)  -- Yellow expected.
toNat-injective A X (zero n) = mkT

-- Should pass.

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
module Data.Boolean.NaryOperators where

open import Data.Boolean
import      Data.Boolean.Operators
open        Data.Boolean.Operators.Logic
open import Function.DomainRaise
open import Numeral.Natural

private variable n : ℕ

-- N-ary conjunction (AND).
-- Every term is true.
∧₊ : (n : ℕ) → (Bool →̂ Bool)(n)
∧₊(0) = 𝑇
∧₊(1) x = x
∧₊(𝐒(𝐒(n))) x = (x ∧_) ∘ (∧₊(𝐒(n)))

-- N-ary disjunction (OR).
-- There is a term which is true.
∨₊ : (n : ℕ) → (Bool →̂ Bool)(n)
∨₊(0) = 𝐹
∨₊(1) x = x
∨₊(𝐒(𝐒(n))) x = (x ∨_) ∘ (∨₊(𝐒(n)))

-- N-ary implication.
-- All left terms together imply the right-most term.
⟶₊ : (n : ℕ) → (Bool →̂ Bool)(n)
⟶₊(0) = 𝑇
⟶₊(1) x = x
⟶₊(𝐒(𝐒(n))) x = (x ⟶_) ∘ (⟶₊(𝐒(n)))

-- N-ary NAND.
-- Not every term is true.
-- There is a term which is false.
⊼₊ : (n : ℕ) → (Bool →̂ Bool)(n)
⊼₊(0) = 𝐹
⊼₊(1) x = ¬ x
⊼₊(𝐒(𝐒(n))) x = (x ⊼_) ∘ ((¬) ∘ (⊼₊(𝐒(n))))

-- N-ary NOR.
-- There are no terms that are true.
-- Every term is false.
⊽₊ : (n : ℕ) → (Bool →̂ Bool)(n)
⊽₊(0) = 𝐹
⊽₊(1) x = ¬ x
⊽₊(𝐒(𝐒(n))) x = (x ⊽_) ∘ ((¬) ∘ (⊽₊(𝐒(n))))


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

open import LogicalFormulae
open import Decidable.Sets

module Decidable.Lemmas {a : _} {A : Set a} (dec : DecidableSet A) where

squash : {x y : A} → .(x ≡ y) → x ≡ y
squash {x} {y} x=y with dec x y
... | inl pr = pr
... | inr bad = exFalso (bad x=y)