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

open import lib.Basics
open import lib.cubical.Square
open import lib.types.Bool
open import lib.types.Coproduct
open import lib.types.FunctionSeq
open import lib.types.Paths
open import lib.types.Pointed
open import lib.types.Span
open import lib.types.Pushout
open import lib.types.Sigma

module lib.types.Smash where

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  ⊙∧-span : ⊙Span
  ⊙∧-span = ⊙span (X ⊙× Y) ⊙Bool (X ⊙⊔ Y)
    (⊔-rec (_, pt Y) (pt X ,_) , idp)
    (⊙⊔-fmap {Y = Y} ⊙cst ⊙cst)

  ∧-span : Span
  ∧-span = ⊙Span-to-Span ⊙∧-span

  abstract
    _∧_ : Type (lmax i j)
    _∧_ = Pushout ∧-span
  Smash = _∧_

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  abstract
    smin : de⊙ X → de⊙ Y → Smash X Y
    smin x y = left (x , y)

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  _⊙∧_ = ptd (X ∧ Y) (smin (pt X) (pt Y))
  ⊙Smash = _⊙∧_

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  abstract

    smbasel : Smash X Y
    smbasel = right true

    smbaser : Smash X Y
    smbaser = right false

    smgluel : (x : de⊙ X) → smin x (pt Y) == smbasel
    smgluel x = glue (inl x)

    smgluer : (y : de⊙ Y) → smin (pt X) y == smbaser
    smgluer y = glue (inr y)

  ∧-norm-l-seq : (x : de⊙ X) → smin x (pt Y) =-= smin (pt X) (pt Y)
  ∧-norm-l-seq x = smgluel x ◃∙ ! (smgluel (pt X)) ◃∎

  ∧-norm-l : (x : de⊙ X) → smin x (pt Y) == smin (pt X) (pt Y)
  ∧-norm-l x = ↯ (∧-norm-l-seq x)

  ∧-norm-r-seq : (y : de⊙ Y) → smin (pt X) y =-= smin (pt X) (pt Y)
  ∧-norm-r-seq y = smgluer y ◃∙ ! (smgluer (pt Y)) ◃∎

  ∧-norm-r : (y : de⊙ Y) → smin (pt X) y == smin (pt X) (pt Y)
  ∧-norm-r y = ↯ (∧-norm-r-seq y)

  ∧-⊙inl : de⊙ Y → X ⊙→ ⊙Smash X Y
  ∧-⊙inl y = (λ x → smin x y) , smgluer y ∙ ! (smgluer (pt Y))

  ∧-⊙inr : de⊙ X → Y ⊙→ ⊙Smash X Y
  ∧-⊙inr x = (λ y → smin x y) , smgluel x ∙ ! (smgluel (pt X))

  ∧-glue-lr : smbasel == smbaser
  ∧-glue-lr = ! (smgluel (pt X)) ∙ smgluer (pt Y)

  ap-smin-l : {a b : de⊙ X} (p : a == b)
    → ap (λ x → smin x (pt Y)) p == smgluel a ∙ ! (smgluel b)
  ap-smin-l = ap-null-homotopic (λ x → smin x (pt Y)) smgluel

  ap-smin-r : {a b : de⊙ Y} (p : a == b)
    → ap (smin (pt X)) p == smgluer a ∙ ! (smgluer b)
  ap-smin-r = ap-null-homotopic (λ y → smin (pt X) y) smgluer

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  module SmashElim {k} {P : Smash X Y → Type k}
    (smin* : (x : de⊙ X) (y : de⊙ Y) → P (smin x y))
    (smbasel* : P smbasel) (smbaser* : P smbaser)
    (smgluel* : (x : de⊙ X) → smin* x (pt Y) == smbasel* [ P ↓ smgluel x ])
    (smgluer* : (y : de⊙ Y) → smin* (pt X) y == smbaser* [ P ↓ smgluer y ]) where

    -- It would be better to encapsulate the repetition in the following definitions in a
    -- private module as follows. Unfortunately, this is not possible when the smash
    -- datatype is declared abstract.
    {-private
      module M = PushoutElim
        (uncurry smin*)
        (Coprod-elim (λ _ → smbasel*) (λ _ → smbaser*))
        (Coprod-elim smgluel* smgluer*)-}

    abstract
      f : (s : X ∧ Y) → P s
      f = PushoutElim.f (uncurry smin*) (Coprod-elim (λ _ → smbasel*) (λ _ → smbaser*)) (Coprod-elim smgluel* smgluer*)

      smin-β : ∀ x y → f (smin x y) ↦ smin* x y
      smin-β x y = PushoutElim.left-β (uncurry smin*) (Coprod-elim (λ _ → smbasel*) (λ _ → smbaser*)) (Coprod-elim smgluel* smgluer*) (x , y)
      {-# REWRITE smin-β #-}

      smbasel-β : f smbasel ↦ smbasel*
      smbasel-β = PushoutElim.right-β (uncurry smin*) (Coprod-elim (λ _ → smbasel*) (λ _ → smbaser*)) (Coprod-elim smgluel* smgluer*) true
      {-# REWRITE smbasel-β #-}

      smbaser-β : f smbaser ↦ smbaser*
      smbaser-β = PushoutElim.right-β (uncurry smin*) (Coprod-elim (λ _ → smbasel*) (λ _ → smbaser*)) (Coprod-elim smgluel* smgluer*) false
      {-# REWRITE smbaser-β #-}

      smgluel-β : ∀ (x : de⊙ X) → apd f (smgluel x) == smgluel* x
      smgluel-β = PushoutElim.glue-β (uncurry smin*) (Coprod-elim (λ _ → smbasel*) (λ _ → smbaser*)) (Coprod-elim smgluel* smgluer*) ∘ inl

      smgluer-β : ∀ (y : de⊙ Y) → apd f (smgluer y) == smgluer* y
      smgluer-β = PushoutElim.glue-β (uncurry smin*) (Coprod-elim (λ _ → smbasel*) (λ _ → smbaser*)) (Coprod-elim smgluel* smgluer*) ∘ inr

  Smash-elim = SmashElim.f

  module SmashRec {k} {C : Type k}
    (smin* : (x : de⊙ X) (y : de⊙ Y) → C)
    (smbasel* smbaser* : C)
    (smgluel* : (x : de⊙ X) → smin* x (pt Y) == smbasel*)
    (smgluer* : (y : de⊙ Y) → smin* (pt X) y == smbaser*) where

    -- It would be better to encapsulate the repetition in the following definitions in a
    -- private module as follows. Unfortunately, this is not possible when the smash
    -- datatype is declared abstract.
    {-private
      module M = PushoutRec {d = ∧-span X Y}
        (uncurry smin*)
        (Coprod-rec (λ _ → smbasel*) (λ _ → smbaser*))
        (Coprod-elim smgluel* smgluer*)-}

    abstract
      f : X ∧ Y → C
      f = PushoutRec.f (uncurry smin*) (Coprod-elim (λ _ → smbasel*) (λ _ → smbaser*)) (Coprod-elim smgluel* smgluer*)

      smin-β : ∀ x y → f (smin x y) ↦ smin* x y
      smin-β x y = PushoutRec.left-β {d = ∧-span X Y} (uncurry smin*) (Coprod-rec (λ _ → smbasel*) (λ _ → smbaser*)) (Coprod-elim smgluel* smgluer*) (x , y)
      {-# REWRITE smin-β #-}

      smbasel-β : f smbasel ↦ smbasel*
      smbasel-β = PushoutRec.right-β {d = ∧-span X Y} (uncurry smin*) (Coprod-rec (λ _ → smbasel*) (λ _ → smbaser*)) (Coprod-elim smgluel* smgluer*) true
      {-# REWRITE smbasel-β #-}

      smbaser-β : f smbaser ↦ smbaser*
      smbaser-β = PushoutRec.right-β {d = ∧-span X Y} (uncurry smin*) (Coprod-rec (λ _ → smbasel*) (λ _ → smbaser*)) (Coprod-elim smgluel* smgluer*) false
      {-# REWRITE smbaser-β #-}

      smgluel-β : ∀ (x : de⊙ X) → ap f (smgluel x) == smgluel* x
      smgluel-β = PushoutRec.glue-β (uncurry smin*) (Coprod-rec (λ _ → smbasel*) (λ _ → smbaser*)) (Coprod-elim smgluel* smgluer*) ∘ inl

      smgluer-β : ∀ (y : de⊙ Y) → ap f (smgluer y) == smgluer* y
      smgluer-β = PushoutRec.glue-β (uncurry smin*) (Coprod-rec (λ _ → smbasel*) (λ _ → smbaser*)) (Coprod-elim smgluel* smgluer*) ∘ inr

      ∧-norm-l-β : ∀ (x : de⊙ X) → ap f (∧-norm-l x) == smgluel* x ∙ ! (smgluel* (pt X))
      ∧-norm-l-β x =
        ap f (∧-norm-l x)
          =⟨ ap-∙ f (smgluel x) (! (smgluel (pt X))) ⟩
        ap f (smgluel x) ∙ ap f (! (smgluel (pt X)))
          =⟨ ap2 _∙_ (smgluel-β x)
                     (ap-! f (smgluel (pt X)) ∙
                      ap ! (smgluel-β (pt X))) ⟩
        smgluel* x ∙ ! (smgluel* (pt X)) =∎

      ∧-norm-r-β : ∀ (y : de⊙ Y) → ap f (∧-norm-r y) == smgluer* y ∙ ! (smgluer* (pt Y))
      ∧-norm-r-β y =
        ap f (∧-norm-r y)
          =⟨ ap-∙ f (smgluer y) (! (smgluer (pt Y))) ⟩
        ap f (smgluer y) ∙ ap f (! (smgluer (pt Y)))
          =⟨ ap2 _∙_ (smgluer-β y)
                     (ap-! f (smgluer (pt Y)) ∙
                      ap ! (smgluer-β (pt Y))) ⟩
        smgluer* y ∙ ! (smgluer* (pt Y)) =∎

  Smash-rec = SmashRec.f

  module SmashPathOverElim {k} {P : Smash X Y → Type k}
    (g₁ g₂ : (xy : Smash X Y) → P xy)
    (smin* : (x : de⊙ X) (y : de⊙ Y) → g₁ (smin x y) == g₂ (smin x y))
    (smbasel* : g₁ smbasel == g₂ smbasel)
    (smbaser* : g₁ smbaser == g₂ smbaser)
    (smgluel* : (x : de⊙ X) →
      smin* x (pt Y) ◃ apd g₂ (smgluel x) ==
      apd g₁ (smgluel x) ▹ smbasel*)
    (smgluer* : (y : de⊙ Y) →
      smin* (pt X) y ◃ apd g₂ (smgluer y) ==
      apd g₁ (smgluer y) ▹ smbaser*)
    where

    f : g₁ ∼ g₂
    f =
      Smash-elim
        {P = λ xy → g₁ xy == g₂ xy}
        smin*
        smbasel*
        smbaser*
        (λ x → ↓-=-in (smgluel* x))
        (λ y → ↓-=-in (smgluer* y))

  Smash-PathOver-elim = SmashPathOverElim.f

  module SmashPathElim {k} {C : Type k}
    (g₁ g₂ : Smash X Y → C)
    (smin* : (x : de⊙ X) (y : de⊙ Y) → g₁ (smin x y) == g₂ (smin x y))
    (smbasel* : g₁ smbasel == g₂ smbasel)
    (smbaser* : g₁ smbaser == g₂ smbaser)
    (smgluel* : (x : de⊙ X) →
      Square (smin* x (pt Y)) (ap g₁ (smgluel x))
             (ap g₂ (smgluel x)) smbasel*)
    (smgluer* : (y : de⊙ Y) →
      Square (smin* (pt X) y) (ap g₁ (smgluer y))
             (ap g₂ (smgluer y)) smbaser*)
    where

    f : g₁ ∼ g₂
    f =
      Smash-elim
        {P = λ xy → g₁ xy == g₂ xy}
        smin*
        smbasel*
        smbaser*
        (λ x → ↓-='-from-square (smgluel* x))
        (λ y → ↓-='-from-square (smgluer* y))

  Smash-Path-elim = SmashPathElim.f

module _ {i j k l} {X : Ptd i} {Y : Ptd j} {X' : Ptd k} {Y' : Ptd l} (f : X ⊙→ X') (g : Y ⊙→ Y') where

  private
    module M = SmashRec
      {C = X' ∧ Y'}
      (λ x y → smin (fst f x) (fst g y))
      (smin (pt X') (pt Y'))
      (smin (pt X') (pt Y'))
      (λ x → ap (λ y' → smin (fst f x) y') (snd g) ∙ ∧-norm-l (fst f x))
      (λ y → ap (λ x' → smin x' (fst g y)) (snd f) ∙ ∧-norm-r (fst g y))

  abstract
    ∧-fmap : X ∧ Y → X' ∧ Y'
    ∧-fmap = M.f

    ∧-fmap-smin-β : ∀ x y → ∧-fmap (smin x y) ↦ smin (fst f x) (fst g y)
    ∧-fmap-smin-β = M.smin-β
    {-# REWRITE ∧-fmap-smin-β #-}

    ∧-fmap-smbasel-β : ∧-fmap smbasel ↦ smin (pt X') (pt Y')
    ∧-fmap-smbasel-β = M.smbasel-β
    {-# REWRITE ∧-fmap-smbasel-β #-}

    ∧-fmap-smbaser-β : ∧-fmap smbaser ↦ smin (pt X') (pt Y')
    ∧-fmap-smbaser-β = M.smbaser-β
    {-# REWRITE ∧-fmap-smbaser-β #-}

    ∧-fmap-smgluel-β' : ∀ x →
      ap ∧-fmap (smgluel x)
      ==
      ap (λ y' → smin (fst f x) y') (snd g) ∙
      ∧-norm-l (fst f x)
    ∧-fmap-smgluel-β' x = M.smgluel-β x

    ∧-fmap-smgluer-β' : ∀ y →
      ap ∧-fmap (smgluer y)
      ==
      ap (λ x' → smin x' (fst g y)) (snd f) ∙
      ∧-norm-r (fst g y)
    ∧-fmap-smgluer-β' = M.smgluer-β

  ∧-fmap-smgluel-β : ∀ x →
    ap ∧-fmap (smgluel x) ◃∎
    =ₛ
    ap (λ y' → smin (fst f x) y') (snd g) ◃∙
    ∧-norm-l (fst f x) ◃∎
  ∧-fmap-smgluel-β x = =ₛ-in (∧-fmap-smgluel-β' x)

  ∧-fmap-smgluer-β : ∀ y →
    ap ∧-fmap (smgluer y) ◃∎
    =ₛ
    ap (λ x' → smin x' (fst g y)) (snd f) ◃∙
    ∧-norm-r (fst g y) ◃∎
  ∧-fmap-smgluer-β y = =ₛ-in (∧-fmap-smgluer-β' y)

  ⊙∧-fmap : X ⊙∧ Y ⊙→ X' ⊙∧ Y'
  ⊙∧-fmap = ∧-fmap , ap2 smin (snd f) (snd g)

  ∧-fmap-norm-l : ∀ x →
    ap ∧-fmap (∧-norm-l x) ◃∎
    =ₛ
    ap (λ y' → smin (fst f x) y') (snd g) ◃∙
    smgluel (fst f x) ◃∙
    ! (smgluel (fst f (pt X))) ◃∙
    ! (ap (smin (fst f (pt X))) (snd g)) ◃∎
  ∧-fmap-norm-l x =
    ap ∧-fmap (∧-norm-l x) ◃∎
      =ₛ⟨ ap-seq-∙ ∧-fmap (∧-norm-l-seq x) ⟩
    ap ∧-fmap (smgluel x) ◃∙
    ap ∧-fmap (! (smgluel (pt X))) ◃∎
      =ₛ₁⟨ 1 & 1 & ap-! ∧-fmap (smgluel (pt X)) ⟩
    ap ∧-fmap (smgluel x) ◃∙
    ! (ap ∧-fmap (smgluel (pt X))) ◃∎
      =ₛ⟨ 0 & 1 & ∧-fmap-smgluel-β x ⟩
    ap (smin (fst f x)) (snd g) ◃∙
    ∧-norm-l (fst f x) ◃∙
    ! (ap ∧-fmap (smgluel (pt X))) ◃∎
      =ₛ⟨ 2 & 1 & !-=ₛ (∧-fmap-smgluel-β (pt X)) ⟩
    ap (smin (fst f x)) (snd g) ◃∙
    ∧-norm-l (fst f x) ◃∙
    ! (∧-norm-l (fst f (pt X))) ◃∙
    ! (ap (smin (fst f (pt X))) (snd g)) ◃∎
      =ₛ⟨ 2 & 1 & !-=ₛ (expand (∧-norm-l-seq (fst f (pt X)))) ⟩
    ap (smin (fst f x)) (snd g) ◃∙
    ∧-norm-l (fst f x) ◃∙
    ! (! (smgluel (pt X'))) ◃∙
    ! (smgluel (fst f (pt X))) ◃∙
    ! (ap (smin (fst f (pt X))) (snd g)) ◃∎
      =ₛ⟨ 1 & 1 & expand (∧-norm-l-seq (fst f x)) ⟩
    ap (smin (fst f x)) (snd g) ◃∙
    smgluel (fst f x) ◃∙
    ! (smgluel (pt X')) ◃∙
    ! (! (smgluel (pt X'))) ◃∙
    ! (smgluel (fst f (pt X))) ◃∙
    ! (ap (smin (fst f (pt X))) (snd g)) ◃∎
      =ₛ⟨ 2 & 2 & seq-!-inv-r (! (smgluel (pt X')) ◃∎) ⟩
    ap (smin (fst f x)) (snd g) ◃∙
    smgluel (fst f x) ◃∙
    ! (smgluel (fst f (pt X))) ◃∙
    ! (ap (smin (fst f (pt X))) (snd g)) ◃∎ ∎ₛ

  ∧-fmap-norm-r : ∀ y →
    ap ∧-fmap (∧-norm-r y) ◃∎
    =ₛ
    ap (λ x' → smin x' (fst g y)) (snd f) ◃∙
    smgluer (fst g y) ◃∙
    ! (smgluer (fst g (pt Y))) ◃∙
    ! (ap (λ x' → smin x' (fst g (pt Y))) (snd f)) ◃∎
  ∧-fmap-norm-r y =
    ap ∧-fmap (∧-norm-r y) ◃∎
      =ₛ⟨ ap-seq-∙ ∧-fmap (∧-norm-r-seq y) ⟩
    ap ∧-fmap (smgluer y) ◃∙
    ap ∧-fmap (! (smgluer (pt Y))) ◃∎
      =ₛ₁⟨ 1 & 1 & ap-! ∧-fmap (smgluer (pt Y)) ⟩
    ap ∧-fmap (smgluer y) ◃∙
    ! (ap ∧-fmap (smgluer (pt Y))) ◃∎
      =ₛ⟨ 0 & 1 & ∧-fmap-smgluer-β y ⟩
    ap (λ x' → smin x' (fst g y)) (snd f) ◃∙
    ∧-norm-r (fst g y) ◃∙
    ! (ap ∧-fmap (smgluer (pt Y))) ◃∎
      =ₛ⟨ 2 & 1 & !-=ₛ (∧-fmap-smgluer-β (pt Y)) ⟩
    ap (λ x' → smin x' (fst g y)) (snd f) ◃∙
    ∧-norm-r (fst g y) ◃∙
    ! (∧-norm-r (fst g (pt Y))) ◃∙
    ! (ap (λ x' → smin x' (fst g (pt Y))) (snd f)) ◃∎
      =ₛ⟨ 2 & 1 & !-=ₛ (expand (∧-norm-r-seq (fst g (pt Y)))) ⟩
    ap (λ x' → smin x' (fst g y)) (snd f) ◃∙
    ∧-norm-r (fst g y) ◃∙
    ! (! (smgluer (pt Y'))) ◃∙
    ! (smgluer (fst g (pt Y))) ◃∙
    ! (ap (λ x' → smin x' (fst g (pt Y))) (snd f)) ◃∎
      =ₛ⟨ 1 & 1 & expand (∧-norm-r-seq (fst g y)) ⟩
    ap (λ x' → smin x' (fst g y)) (snd f) ◃∙
    smgluer (fst g y) ◃∙
    ! (smgluer (pt Y')) ◃∙
    ! (! (smgluer (pt Y'))) ◃∙
    ! (smgluer (fst g (pt Y))) ◃∙
    ! (ap (λ x → smin x (fst g (pt Y))) (snd f)) ◃∎
      =ₛ⟨ 2 & 2 & seq-!-inv-r (! (smgluer (pt Y')) ◃∎) ⟩
    ap (λ x' → smin x' (fst g y)) (snd f) ◃∙
    smgluer (fst g y) ◃∙
    ! (smgluer (fst g (pt Y))) ◃∙
    ! (ap (λ x' → smin x' (fst g (pt Y))) (snd f)) ◃∎ ∎ₛ

module _ {i i' i'' j j' j''}
         {X : Ptd i} {X' : Ptd i'} {X'' : Ptd i''} (f : X ⊙→ X') (f' : X' ⊙→ X'')
         {Y : Ptd j} {Y' : Ptd j'} {Y'' : Ptd j''} (g : Y ⊙→ Y') (g' : Y' ⊙→ Y'') where

  ∧-fmap-comp : ∀ xy →
    ∧-fmap (f' ⊙∘ f) (g' ⊙∘ g) xy == ∧-fmap f' g' (∧-fmap f g xy)
  ∧-fmap-comp =
    Smash-elim {X = X} {Y = Y}
      {P = λ xy → ∧-fmap (f' ⊙∘ f) (g' ⊙∘ g) xy == ∧-fmap f' g' (∧-fmap f g xy)}
      (λ x y → idp)
      (! (ap2 smin (snd f') (snd g')))
      (! (ap2 smin (snd f') (snd g')))
      (λ x → ↓-='-in-=ₛ $
        idp ◃∙
        ap (∧-fmap f' g' ∘ ∧-fmap f g) (smgluel x) ◃∎
          =ₛ⟨ 0 & 1 & expand [] ⟩
        ap (∧-fmap f' g' ∘ ∧-fmap f g) (smgluel x) ◃∎
          =ₛ₁⟨ ap-∘ (∧-fmap f' g') (∧-fmap f g) (smgluel x) ⟩
        ap (∧-fmap f' g') (ap (∧-fmap f g) (smgluel x)) ◃∎
          =ₛ⟨ ap-seq-=ₛ (∧-fmap f' g') (∧-fmap-smgluel-β f g x) ⟩
        ap (∧-fmap f' g') (ap (smin (fst f x)) (snd g)) ◃∙
        ap (∧-fmap f' g') (∧-norm-l (fst f x)) ◃∎
          =ₛ₁⟨ 0 & 1 & ∘-ap (∧-fmap f' g') (smin (fst f x)) (snd g) ⟩
        ap (smin (fst (f' ⊙∘ f) x) ∘ fst g') (snd g) ◃∙
        ap (∧-fmap f' g') (∧-norm-l (fst f x)) ◃∎
          =ₛ⟨ 1 & 1 & ∧-fmap-norm-l f' g' (fst f x) ⟩
        ap (smin (fst (f' ⊙∘ f) x) ∘ fst g') (snd g) ◃∙
        ap (smin (fst (f' ⊙∘ f) x)) (snd g') ◃∙
        smgluel (fst (f' ⊙∘ f) x) ◃∙
        ! (smgluel (fst f' (pt X'))) ◃∙
        ! (ap (smin (fst f' (pt X'))) (snd g')) ◃∎
          =ₛ₁⟨ 0 & 1 & ap-∘ (smin (fst (f' ⊙∘ f) x)) (fst g') (snd g) ⟩
        ap (smin (fst (f' ⊙∘ f) x)) (ap (fst g') (snd g)) ◃∙
        ap (smin (fst (f' ⊙∘ f) x)) (snd g') ◃∙
        smgluel (fst (f' ⊙∘ f) x) ◃∙
        ! (smgluel (fst f' (pt X'))) ◃∙
        ! (ap (smin (fst f' (pt X'))) (snd g')) ◃∎
          =ₛ⟨ 0 & 2 & ∙-ap-seq (smin (fst (f' ⊙∘ f) x)) (ap (fst g') (snd g) ◃∙ snd g' ◃∎) ⟩
        ap (smin (fst f' (fst f x))) (snd (g' ⊙∘ g)) ◃∙
        smgluel (fst (f' ⊙∘ f) x) ◃∙
        ! (smgluel (fst f' (pt X'))) ◃∙
        ! (ap (smin (fst f' (pt X'))) (snd g')) ◃∎
          =ₛ⟨ 3 & 0 & !ₛ (seq-!-inv-r (ap (λ x'' → smin x'' (pt Y'')) (snd f') ◃∎)) ⟩
        ap (smin (fst f' (fst f x))) (snd (g' ⊙∘ g)) ◃∙
        smgluel (fst (f' ⊙∘ f) x) ◃∙
        ! (smgluel (fst f' (pt X'))) ◃∙
        ap (λ x'' → smin x'' (pt Y'')) (snd f') ◃∙
        ! (ap (λ x'' → smin x'' (pt Y'')) (snd f')) ◃∙
        ! (ap (smin (fst f' (pt X'))) (snd g')) ◃∎
          =ₛ⟨ 4 & 2 & !ₛ $ !-=ₛ $ ap2-out' smin (snd f') (snd g') ⟩
        ap (smin (fst f' (fst f x))) (snd (g' ⊙∘ g)) ◃∙
        smgluel (fst (f' ⊙∘ f) x) ◃∙
        ! (smgluel (fst f' (pt X'))) ◃∙
        ap (λ x'' → smin x'' (pt Y'')) (snd f') ◃∙
        ! (ap2 smin (snd f') (snd g')) ◃∎
          =ₛ⟨ 3 & 1 &
              =ₛ-in {t = smgluel (fst f' (pt X')) ◃∙ ! (smgluel (pt X'')) ◃∎} $
              ap-null-homotopic (λ x'' → smin x'' (pt Y'')) smgluel (snd f') ⟩
        ap (smin (fst f' (fst f x))) (snd (g' ⊙∘ g)) ◃∙
        smgluel (fst (f' ⊙∘ f) x) ◃∙
        ! (smgluel (fst f' (pt X'))) ◃∙
        smgluel (fst f' (pt X')) ◃∙
        ! (smgluel (pt X'')) ◃∙
        ! (ap2 smin (snd f') (snd g')) ◃∎
          =ₛ⟨ 2 & 2 & seq-!-inv-l (smgluel (fst f' (pt X')) ◃∎) ⟩
        ap (smin (fst f' (fst f x))) (snd (g' ⊙∘ g)) ◃∙
        smgluel (fst (f' ⊙∘ f) x) ◃∙
        ! (smgluel (pt X'')) ◃∙
        ! (ap2 smin (snd f') (snd g')) ◃∎
          =ₛ⟨ 1 & 2 & contract ⟩
        ap (smin (fst f' (fst f x))) (snd (g' ⊙∘ g)) ◃∙
        ∧-norm-l (fst (f' ⊙∘ f) x) ◃∙
        ! (ap2 smin (snd f') (snd g')) ◃∎
          =ₛ⟨ 0 & 2 & !ₛ (∧-fmap-smgluel-β (f' ⊙∘ f) (g' ⊙∘ g) x) ⟩
        ap (∧-fmap (f' ⊙∘ f) (g' ⊙∘ g)) (smgluel x) ◃∙
        ! (ap2 smin (snd f') (snd g')) ◃∎ ∎ₛ)
      (λ y → ↓-='-in-=ₛ $
        idp ◃∙
        ap (∧-fmap f' g' ∘ ∧-fmap f g) (smgluer y) ◃∎
          =ₛ⟨ 0 & 1 & expand [] ⟩
        ap (∧-fmap f' g' ∘ ∧-fmap f g) (smgluer y) ◃∎
          =ₛ₁⟨ ap-∘ (∧-fmap f' g') (∧-fmap f g) (smgluer y) ⟩
        ap (∧-fmap f' g') (ap (∧-fmap f g) (smgluer y)) ◃∎
          =ₛ⟨ ap-seq-=ₛ (∧-fmap f' g') (∧-fmap-smgluer-β f g y) ⟩
        ap (∧-fmap f' g') (ap (λ x' → smin x' (fst g y)) (snd f)) ◃∙
        ap (∧-fmap f' g') (∧-norm-r (fst g y)) ◃∎
          =ₛ₁⟨ 0 & 1 & ∘-ap (∧-fmap f' g') (λ x' → smin x' (fst g y)) (snd f) ⟩
        ap (λ x' → smin (fst f' x') (fst (g' ⊙∘ g) y)) (snd f) ◃∙
        ap (∧-fmap f' g') (∧-norm-r (fst g y)) ◃∎
          =ₛ⟨ 1 & 1 & ∧-fmap-norm-r f' g' (fst g y) ⟩
        ap (λ x' → smin (fst f' x') (fst (g' ⊙∘ g) y)) (snd f) ◃∙
        ap (λ x'' → smin x'' (fst (g' ⊙∘ g) y)) (snd f') ◃∙
        smgluer (fst (g' ⊙∘ g) y) ◃∙
        ! (smgluer (fst g' (pt Y'))) ◃∙
        ! (ap (λ x' → smin x' (fst g' (pt Y'))) (snd f')) ◃∎
          =ₛ₁⟨ 0 & 1 & ap-∘ (λ x'' → smin x'' (fst (g' ⊙∘ g) y)) (fst f') (snd f) ⟩
        ap (λ x'' → smin x'' (fst (g' ⊙∘ g) y)) (ap (fst f') (snd f)) ◃∙
        ap (λ x'' → smin x'' (fst (g' ⊙∘ g) y)) (snd f') ◃∙
        smgluer (fst (g' ⊙∘ g) y) ◃∙
        ! (smgluer (fst g' (pt Y'))) ◃∙
        ! (ap (λ x' → smin x' (fst g' (pt Y'))) (snd f')) ◃∎
          =ₛ⟨ 0 & 2 & ∙-ap-seq (λ x'' → smin x'' (fst (g' ⊙∘ g) y))
                               (ap (fst f') (snd f) ◃∙ snd f' ◃∎) ⟩
        ap (λ x'' → smin x'' (fst (g' ⊙∘ g) y)) (snd (f' ⊙∘ f)) ◃∙
        smgluer (fst (g' ⊙∘ g) y) ◃∙
        ! (smgluer (fst g' (pt Y'))) ◃∙
        ! (ap (λ x' → smin x' (fst g' (pt Y'))) (snd f')) ◃∎
          =ₛ⟨ 3 & 0 & !ₛ (seq-!-inv-r (ap (smin (pt X'')) (snd g') ◃∎)) ⟩
        ap (λ x'' → smin x'' (fst (g' ⊙∘ g) y)) (snd (f' ⊙∘ f)) ◃∙
        smgluer (fst (g' ⊙∘ g) y) ◃∙
        ! (smgluer (fst g' (pt Y'))) ◃∙
        ap (smin (pt X'')) (snd g') ◃∙
        ! (ap (smin (pt X'')) (snd g')) ◃∙
        ! (ap (λ x' → smin x' (fst g' (pt Y'))) (snd f')) ◃∎
          =ₛ⟨ 4 & 2 & !ₛ $ !-=ₛ $ ap2-out smin (snd f') (snd g') ⟩
        ap (λ x'' → smin x'' (fst (g' ⊙∘ g) y)) (snd (f' ⊙∘ f)) ◃∙
        smgluer (fst (g' ⊙∘ g) y) ◃∙
        ! (smgluer (fst g' (pt Y'))) ◃∙
        ap (smin (pt X'')) (snd g') ◃∙
        ! (ap2 smin (snd f') (snd g')) ◃∎
          =ₛ⟨ 3 & 1 &
              =ₛ-in {t = smgluer (fst g' (pt Y')) ◃∙ ! (smgluer (pt Y'')) ◃∎} $
              ap-null-homotopic (smin (pt X'')) smgluer (snd g') ⟩
        ap (λ x'' → smin x'' (fst (g' ⊙∘ g) y)) (snd (f' ⊙∘ f)) ◃∙
        smgluer (fst (g' ⊙∘ g) y) ◃∙
        ! (smgluer (fst g' (pt Y'))) ◃∙
        smgluer (fst g' (pt Y')) ◃∙
        ! (smgluer (pt Y'')) ◃∙
        ! (ap2 smin (snd f') (snd g')) ◃∎
          =ₛ⟨ 2 & 2 & seq-!-inv-l (smgluer (fst g' (pt Y')) ◃∎) ⟩
        ap (λ x'' → smin x'' (fst (g' ⊙∘ g) y)) (snd (f' ⊙∘ f)) ◃∙
        smgluer (fst (g' ⊙∘ g) y) ◃∙
        ! (smgluer (pt Y'')) ◃∙
        ! (ap2 smin (snd f') (snd g')) ◃∎
          =ₛ⟨ 1 & 2 & contract ⟩
        ap (λ x'' → smin x'' (fst (g' ⊙∘ g) y)) (snd (f' ⊙∘ f)) ◃∙
        ∧-norm-r (fst (g' ⊙∘ g) y) ◃∙
        ! (ap2 smin (snd f') (snd g')) ◃∎
          =ₛ⟨ 0 & 2 & !ₛ (∧-fmap-smgluer-β (f' ⊙∘ f) (g' ⊙∘ g) y) ⟩
        ap (∧-fmap (f' ⊙∘ f) (g' ⊙∘ g)) (smgluer y) ◃∙
        ! (ap2 smin (snd f') (snd g')) ◃∎ ∎ₛ)

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  ×-to-∧ : de⊙ X × de⊙ Y → X ∧ Y
  ×-to-∧ (x , y) = smin x y

  ×-⊙to-∧ : X ⊙× Y ⊙→ X ⊙∧ Y
  ×-⊙to-∧ = ×-to-∧ , idp

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  module SmashSwap =
    SmashRec {X = X} {Y = Y}
      {C = Y ∧ X}
      (λ x y → smin y x)
      (smin (pt Y) (pt X))
      (smin (pt Y) (pt X))
      ∧-norm-r
      ∧-norm-l

  ∧-swap : X ∧ Y → Y ∧ X
  ∧-swap = SmashSwap.f

  ⊙∧-swap : X ⊙∧ Y ⊙→ Y ⊙∧ X
  ⊙∧-swap = ∧-swap , idp

  ∧-swap-norm-l-β : ∀ x →
    ap ∧-swap (∧-norm-l x) == ∧-norm-r x
  ∧-swap-norm-l-β x =
    ap ∧-swap (∧-norm-l x)
      =⟨ SmashSwap.∧-norm-l-β x ⟩
    ∧-norm-r x ∙ ! (∧-norm-r (pt X))
      =⟨ ap (λ u → ∧-norm-r x ∙ ! u) (!-inv-r (smgluer (pt X))) ⟩
    ∧-norm-r x ∙ idp
      =⟨ ∙-unit-r (∧-norm-r x) ⟩
    ∧-norm-r x =∎

  ∧-swap-norm-r-β : ∀ y →
    ap ∧-swap (∧-norm-r y) == ∧-norm-l y
  ∧-swap-norm-r-β y =
    ap ∧-swap (∧-norm-r y)
      =⟨ SmashSwap.∧-norm-r-β y ⟩
    ∧-norm-l y ∙ ! (∧-norm-l (pt Y))
      =⟨ ap (λ u → ∧-norm-l y ∙ ! u) (!-inv-r (smgluel (pt Y))) ⟩
    ∧-norm-l y ∙ idp
      =⟨ ∙-unit-r (∧-norm-l y) ⟩
    ∧-norm-l y =∎

  ×-to-∧-swap : ∧-swap ∘ ×-to-∧ ∼ ×-to-∧ ∘ ×-swap
  ×-to-∧-swap (x , y) = idp

  ×-⊙to-∧-swap :
    ⊙∧-swap ◃⊙∘ ×-⊙to-∧ ◃⊙idf
    =⊙∘
    ×-⊙to-∧ ◃⊙∘ ⊙×-swap ◃⊙idf
  ×-⊙to-∧-swap = =⊙∘-in $
    ⊙λ=' ×-to-∧-swap idp

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  module SmashSwapInvolutive =
    SmashElim {X = X} {Y = Y}
      {P = λ xy → ∧-swap Y X (∧-swap X Y xy) == xy}
      (λ x y → idp)
      (smgluel (pt X))
      (smgluer (pt Y))
      (λ x → ↓-app=idf-in $ ! $
        ap (∧-swap Y X ∘ ∧-swap X Y) (smgluel x) ∙ smgluel (pt X)
          =⟨ ap (_∙ smgluel (pt X)) $
             ap-∘ (∧-swap Y X) (∧-swap X Y) (smgluel x) ⟩
        ap (∧-swap Y X) (ap (∧-swap X Y) (smgluel x)) ∙ smgluel (pt X)
          =⟨ ap (λ p → ap (∧-swap Y X) p ∙ smgluel (pt X)) $
             SmashSwap.smgluel-β X Y x ⟩
        ap (∧-swap Y X) (∧-norm-r x) ∙ smgluel (pt X)
          =⟨ ap (_∙ smgluel (pt X)) (∧-swap-norm-r-β Y X x) ⟩
        ∧-norm-l x ∙ smgluel (pt X)
          =⟨ ∙-assoc (smgluel x) (! (smgluel (pt X))) (smgluel (pt X))⟩
        smgluel x ∙ ! (smgluel (pt X)) ∙ smgluel (pt X)
          =⟨ ap (smgluel x ∙_) (!-inv-l (smgluel (pt X))) ⟩
        smgluel x ∙ idp
          =⟨ ∙-unit-r (smgluel x) ⟩
        smgluel x
          =⟨ ! (∙'-unit-l (smgluel x)) ⟩
        idp ∙' smgluel x =∎)
      (λ y → ↓-app=idf-in $ ! $
        ap (∧-swap Y X ∘ ∧-swap X Y) (smgluer y) ∙ smgluer (pt Y)
          =⟨ ap (_∙ smgluer (pt Y)) $
             ap-∘ (∧-swap Y X) (∧-swap X Y) (smgluer y) ⟩
        ap (∧-swap Y X) (ap (∧-swap X Y) (smgluer y)) ∙ smgluer (pt Y)
          =⟨ ap (λ p → ap (∧-swap Y X) p ∙ smgluer (pt Y)) $
             SmashSwap.smgluer-β X Y y ⟩
        ap (∧-swap Y X) (∧-norm-l y) ∙ smgluer (pt Y)
          =⟨ ap (_∙ smgluer (pt Y)) (∧-swap-norm-l-β Y X y) ⟩
        ∧-norm-r y ∙ smgluer (pt Y)
          =⟨ ∙-assoc (smgluer y) (! (smgluer (pt Y))) (smgluer (pt Y)) ⟩
        smgluer y ∙ ! (smgluer (pt Y)) ∙ smgluer (pt Y)
          =⟨ ap (smgluer y ∙_) (!-inv-l (smgluer (pt Y))) ⟩
        smgluer y ∙ idp
          =⟨ ∙-unit-r (smgluer y) ⟩
        smgluer y
          =⟨ ! (∙'-unit-l (smgluer y)) ⟩
        idp ∙' smgluer y =∎)

  ∧-swap-inv : ∀ xy → ∧-swap Y X (∧-swap X Y xy) == xy
  ∧-swap-inv = SmashSwapInvolutive.f

  ⊙∧-swap-inv : ⊙∧-swap Y X ◃⊙∘ ⊙∧-swap X Y ◃⊙idf =⊙∘ ⊙idf-seq
  ⊙∧-swap-inv = =⊙∘-in (⊙λ=' ∧-swap-inv idp)

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  ∧-swap-is-equiv : is-equiv (∧-swap X Y)
  ∧-swap-is-equiv = is-eq _ (∧-swap Y X) (∧-swap-inv Y X) (∧-swap-inv X Y)

  ∧-swap-equiv : (X ∧ Y) ≃ (Y ∧ X)
  ∧-swap-equiv = ∧-swap X Y , ∧-swap-is-equiv

module _ {i i' j j'} {X : Ptd i} {X' : Ptd i'} {Y : Ptd j} {Y' : Ptd j'}
         (f : X ⊙→ X') (g : Y ⊙→ Y') where

  ∧-swap-naturality : ∀ xy →
    ∧-fmap g f (∧-swap X Y xy) == ∧-swap X' Y' (∧-fmap f g xy)
  ∧-swap-naturality =
    Smash-elim {X = X} {Y = Y}
      {P = λ xy → ∧-fmap g f (∧-swap X Y xy) == ∧-swap X' Y' (∧-fmap f g xy)}
      (λ x y → idp)
      (ap2 smin (snd g) (snd f))
      (ap2 smin (snd g) (snd f))
      (λ x → ↓-='-in-=ₛ $
        idp ◃∙
        ap (∧-swap X' Y' ∘ ∧-fmap f g) (smgluel x) ◃∎
          =ₛ⟨ 0 & 1 & expand [] ⟩
        ap (∧-swap X' Y' ∘ ∧-fmap f g) (smgluel x) ◃∎
          =ₛ₁⟨ ap-∘ (∧-swap X' Y') (∧-fmap f g) (smgluel x) ⟩
        ap (∧-swap X' Y') (ap (∧-fmap f g) (smgluel x)) ◃∎
          =ₛ⟨ ap-seq-=ₛ (∧-swap X' Y') (∧-fmap-smgluel-β f g x) ⟩
        ap (∧-swap X' Y') (ap (smin (fst f x)) (snd g)) ◃∙
        ap (∧-swap X' Y') (∧-norm-l (fst f x)) ◃∎
          =ₛ₁⟨ 0 & 1 & ∘-ap (∧-swap X' Y') (smin (fst f x)) (snd g) ⟩
        ap (λ y' → smin y' (fst f x)) (snd g) ◃∙
        ap (∧-swap X' Y') (∧-norm-l (fst f x)) ◃∎
          =ₛ₁⟨ 1 & 1 & ∧-swap-norm-l-β X' Y' (fst f x) ⟩
        ap (λ y' → smin y' (fst f x)) (snd g) ◃∙
        ∧-norm-r (fst f x) ◃∎
          =ₛ⟨ 1 & 1 & expand (∧-norm-r-seq (fst f x)) ⟩
        ap (λ y' → smin y' (fst f x)) (snd g) ◃∙
        smgluer (fst f x) ◃∙
        ! (smgluer (pt X')) ◃∎
          =ₛ⟨ 2 & 0 & !ₛ (seq-!-inv-l (smgluer (fst f (pt X)) ◃∎)) ⟩
        ap (λ y' → smin y' (fst f x)) (snd g) ◃∙
        smgluer (fst f x) ◃∙
        ! (smgluer (fst f (pt X))) ◃∙
        smgluer (fst f (pt X)) ◃∙
        ! (smgluer (pt X')) ◃∎
          =ₛ₁⟨ 3 & 2 & ! (ap-null-homotopic (smin (pt Y')) smgluer (snd f)) ⟩
        ap (λ y' → smin y' (fst f x)) (snd g) ◃∙
        smgluer (fst f x) ◃∙
        ! (smgluer (fst f (pt X))) ◃∙
        ap (smin (pt Y')) (snd f) ◃∎
          =ₛ⟨ 3 & 0 & !ₛ (seq-!-inv-l (ap (λ y' → smin y' (fst f (pt X))) (snd g) ◃∎)) ⟩
        ap (λ y' → smin y' (fst f x)) (snd g) ◃∙
        smgluer (fst f x) ◃∙
        ! (smgluer (fst f (pt X))) ◃∙
        ! (ap (λ y' → smin y' (fst f (pt X))) (snd g)) ◃∙
        ap (λ y' → smin y' (fst f (pt X))) (snd g) ◃∙
        ap (smin (pt Y')) (snd f) ◃∎
          =ₛ⟨ 4 & 2 & !ₛ (ap2-out smin (snd g) (snd f)) ⟩
        ap (λ y' → smin y' (fst f x)) (snd g) ◃∙
        smgluer (fst f x) ◃∙
        ! (smgluer (fst f (pt X))) ◃∙
        ! (ap (λ y' → smin y' (fst f (pt X))) (snd g)) ◃∙
        ap2 smin (snd g) (snd f) ◃∎
          =ₛ⟨ 0 & 4 & !ₛ (∧-fmap-norm-r g f x) ⟩
        ap (∧-fmap g f) (∧-norm-r x) ◃∙
        ap2 smin (snd g) (snd f) ◃∎
          =ₛ₁⟨ 0 & 1 & ! (ap (ap (∧-fmap g f)) (SmashSwap.smgluel-β X Y x)) ⟩
        ap (∧-fmap g f) (ap (∧-swap X Y) (smgluel x)) ◃∙
        ap2 smin (snd g) (snd f) ◃∎
          =ₛ₁⟨ 0 & 1 & ∘-ap (∧-fmap g f) (∧-swap X Y) (smgluel x) ⟩
        ap (∧-fmap g f ∘ ∧-swap X Y) (smgluel x) ◃∙
        ap2 smin (snd g) (snd f) ◃∎ ∎ₛ)
      (λ y → ↓-='-in-=ₛ $
        idp ◃∙
        ap (∧-swap X' Y' ∘ ∧-fmap f g) (smgluer y) ◃∎
          =ₛ⟨ 0 & 1 & expand [] ⟩
        ap (∧-swap X' Y' ∘ ∧-fmap f g) (smgluer y) ◃∎
          =ₛ₁⟨ ap-∘ (∧-swap X' Y') (∧-fmap f g) (smgluer y) ⟩
        ap (∧-swap X' Y') (ap (∧-fmap f g) (smgluer y)) ◃∎
          =ₛ⟨ ap-seq-=ₛ (∧-swap X' Y') (∧-fmap-smgluer-β f g y) ⟩
        ap (∧-swap X' Y') (ap (λ x' → smin x' (fst g y)) (snd f)) ◃∙
        ap (∧-swap X' Y') (∧-norm-r (fst g y)) ◃∎
          =ₛ₁⟨ 0 & 1 & ∘-ap (∧-swap X' Y') (λ x' → smin x' (fst g y)) (snd f) ⟩
        ap (smin (fst g y)) (snd f) ◃∙
        ap (∧-swap X' Y') (∧-norm-r (fst g y)) ◃∎
          =ₛ₁⟨ 1 & 1 & ∧-swap-norm-r-β X' Y' (fst g y) ⟩
        ap (smin (fst g y)) (snd f) ◃∙
        ∧-norm-l (fst g y) ◃∎
          =ₛ⟨ 1 & 1 & expand (∧-norm-l-seq (fst g y)) ⟩
        ap (smin (fst g y)) (snd f) ◃∙
        smgluel (fst g y) ◃∙
        ! (smgluel (pt Y')) ◃∎
          =ₛ⟨ 2 & 0 & !ₛ (seq-!-inv-l (smgluel (fst g (pt Y)) ◃∎)) ⟩
        ap (smin (fst g y)) (snd f) ◃∙
        smgluel (fst g y) ◃∙
        ! (smgluel (fst g (pt Y))) ◃∙
        smgluel (fst g (pt Y)) ◃∙
        ! (smgluel (pt Y')) ◃∎
          =ₛ₁⟨ 3 & 2 & ! (ap-null-homotopic (λ y' → smin y' (pt X')) smgluel (snd g)) ⟩
        ap (smin (fst g y)) (snd f) ◃∙
        smgluel (fst g y) ◃∙
        ! (smgluel (fst g (pt Y))) ◃∙
        ap (λ y' → smin y' (pt X')) (snd g) ◃∎
          =ₛ⟨ 3 & 0 & !ₛ (seq-!-inv-l (ap (smin (fst g (pt Y))) (snd f) ◃∎)) ⟩
        ap (smin (fst g y)) (snd f) ◃∙
        smgluel (fst g y) ◃∙
        ! (smgluel (fst g (pt Y))) ◃∙
        ! (ap (smin (fst g (pt Y))) (snd f)) ◃∙
        ap (smin (fst g (pt Y))) (snd f) ◃∙
        ap (λ y' → smin y' (pt X')) (snd g) ◃∎
          =ₛ⟨ 4 & 2 & !ₛ (ap2-out' smin (snd g) (snd f)) ⟩
        ap (smin (fst g y)) (snd f) ◃∙
        smgluel (fst g y) ◃∙
        ! (smgluel (fst g (pt Y))) ◃∙
        ! (ap (smin (fst g (pt Y))) (snd f)) ◃∙
        ap2 smin (snd g) (snd f) ◃∎
          =ₛ⟨ 0 & 4 & !ₛ (∧-fmap-norm-l g f y) ⟩
        ap (∧-fmap g f) (∧-norm-l y) ◃∙
        ap2 smin (snd g) (snd f) ◃∎
          =ₛ₁⟨ 0 & 1 & ! (ap (ap (∧-fmap g f)) (SmashSwap.smgluer-β X Y y)) ⟩
        ap (∧-fmap g f) (ap (∧-swap X Y) (smgluer y)) ◃∙
        ap2 smin (snd g) (snd f) ◃∎
          =ₛ₁⟨ 0 & 1 & ∘-ap (∧-fmap g f) (∧-swap X Y) (smgluer y) ⟩
        ap (∧-fmap g f ∘ ∧-swap X Y) (smgluer y) ◃∙
        ap2 smin (snd g) (snd f) ◃∎ ∎ₛ)

  ⊙∧-swap-naturality : ⊙∧-fmap g f ⊙∘ ⊙∧-swap X Y ==
                       ⊙∧-swap X' Y' ⊙∘ ⊙∧-fmap f g
  ⊙∧-swap-naturality =
    ⊙λ=' ∧-swap-naturality $ =ₛ-out $
    ap2 smin (snd g) (snd f) ◃∎
      =ₛ⟨ ap2-out smin (snd g) (snd f) ⟩
    ap (λ u → smin u (fst f (pt X))) (snd g) ◃∙
    ap (smin (pt Y')) (snd f) ◃∎
      =ₛ⟨ !ₛ $ ap2-out' (λ x y → smin y x) (snd f) (snd g) ⟩
    ap2 (λ x y → smin y x) (snd f) (snd g) ◃∎
      =ₛ₁⟨ ! $ ap-ap2 (∧-swap X' Y') smin (snd f) (snd g) ⟩
    ap (∧-swap X' Y') (ap2 smin (snd f) (snd g)) ◃∎
      =ₛ⟨ 1 & 0 & contract ⟩
    ap (∧-swap X' Y') (ap2 smin (snd f) (snd g)) ◃∙ idp ◃∎ ∎ₛ

  ∧-swap-fmap : ∀ xy →
    ∧-swap Y' X' (∧-fmap g f (∧-swap X Y xy)) == ∧-fmap f g xy
  ∧-swap-fmap xy =
    ∧-swap Y' X' (∧-fmap g f (∧-swap X Y xy))
      =⟨ ap (∧-swap Y' X') (∧-swap-naturality xy) ⟩
    ∧-swap Y' X' (∧-swap X' Y' (∧-fmap f g xy))
      =⟨ ∧-swap-inv X' Y' (∧-fmap f g xy) ⟩
    ∧-fmap f g xy =∎

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
-- Testing parameterised records in parameterised modules
module Exist (X : Set) where

data [_] (a : Set) : Set where
  []  : [ a ]
  _∷_ : a -> [ a ] -> [ a ]

map : forall {a b} -> (a -> b) -> [ a ] -> [ b ]
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

record ∃ (a : Set) (P : a -> Set) : Set where
  field
    witness : a
    proof   : P witness

ListP : (a : Set) -> (a -> Set) -> Set
ListP a P = [ ∃ a P ]

mapP : forall {a b P Q}
  -> (f : a -> b) -> (forall {x} -> P x -> Q (f x))
  -> ListP a P -> ListP b Q
mapP {a} {b} {P} {Q} f pres xs = map helper xs
  where
  helper : ∃ a P -> ∃ b Q
  helper r = record { witness = f (∃.witness r)
                    ; proof   = pres (∃.proof r)
                    }

ext: agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import Relation.Binary using (Rel; Setoid; IsEquivalence)
module Structures
  {a ℓ} {A : Set a}  -- The underlying set
  (_≈_ : Rel A ℓ)    -- The underlying equality relation
  where

open import Algebra.Core
open import Level using (_⊔_)
open import Data.Product using (_,_; proj₁; proj₂)
open import Algebra.Definitions _≈_
open import Algebra.Structures _≈_
open import Definitions _≈_

------------------------------------------------------------------------
-- Structures with 1 binary operation
------------------------------------------------------------------------

record IsLatinQuasigroup (∙ : Op₂ A ) : Set (a ⊔ ℓ) where
  field
    isMagma     : IsMagma ∙
    latinSquare : LatinSquare ∙

  open IsMagma isMagma public

  latinSquare₁ : LatinSquare₁ ∙
  latinSquare₁ = proj₁ latinSquare

  latinSquare₂ : LatinSquare₂ ∙
  latinSquare₂ = proj₂ latinSquare

record IsIdempotentMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isMagma : IsMagma ∙
    idem    : Idempotent ∙

  open IsMagma isMagma public

record IsAlternateMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isMagma  : IsMagma ∙
    alter    : Alternative ∙

  open IsMagma isMagma public

record IsFlexibleMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isMagma  : IsMagma ∙
    flex     : Flexible ∙

  open IsMagma isMagma public

record IsMedialMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isMagma : IsMagma ∙
    medial  : Medial ∙

  open IsMagma isMagma public

record IsSemimedialMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isMagma : IsMagma ∙
    semiMedial  : Semimedial ∙

  open IsMagma isMagma public

record IsInverseSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isSemigroup     : IsSemigroup ∙
    pseudoInverse   : PseudoInverse ∙

  open IsSemigroup isSemigroup public

------------------------------------------------------------------------
-- Structures with 1 binary operation and 1 element
------------------------------------------------------------------------

record IsLeftUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isMagma  : IsMagma ∙
    identity : LeftIdentity ε ∙

  open IsMagma isMagma public

record IsRightUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isMagma  : IsMagma ∙
    identity : RightIdentity ε ∙

  open IsMagma isMagma public

------------------------------------------------------------------------
-- Structures with 2 binary operations, 1 unary operation & 1 element
------------------------------------------------------------------------

record IsNonAssociativeRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    +-isAbelianGroup : IsAbelianGroup + 0# -_
    *-cong           : Congruent₂ *
    identity         : Identity 1# *
    distrib          : * DistributesOver +
    zero             : Zero 0# *

  open IsAbelianGroup +-isAbelianGroup public
    renaming
    ( assoc                   to +-assoc
    ; ∙-cong                  to +-cong
    ; ∙-congˡ                 to +-congˡ
    ; ∙-congʳ                 to +-congʳ
    ; identity                to +-identity
    ; identityˡ               to +-identityˡ
    ; identityʳ               to +-identityʳ
    ; inverse                 to -‿inverse
    ; inverseˡ                to -‿inverseˡ
    ; inverseʳ                to -‿inverseʳ
    ; ⁻¹-cong                 to -‿cong
    ; comm                    to +-comm
    ; isMagma                 to +-isMagma
    ; isSemigroup             to +-isSemigroup
    ; isMonoid                to +-isMonoid
    ; isUnitalMagma           to +-isUnitalMagma
    ; isCommutativeMagma      to +-isCommutativeMagma
    ; isCommutativeMonoid     to +-isCommutativeMonoid
    ; isCommutativeSemigroup  to +-isCommutativeSemigroup
    ; isInvertibleMagma       to +-isInvertibleMagma
    ; isInvertibleUnitalMagma to +-isInvertibleUnitalMagma
    ; isGroup                 to +-isGroup
    )

  *-isMagma : IsMagma *
  *-isMagma = record
    { isEquivalence = isEquivalence
    ; ∙-cong        = *-cong
    }

  *-identityˡ : LeftIdentity 1# *
  *-identityˡ = proj₁ identity

  *-identityʳ : RightIdentity 1# *
  *-identityʳ = proj₂ identity

------------------------------------------------------------------------
-- Structures with 3 binary operation and 1 element
------------------------------------------------------------------------

record IsLeftBolLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isLoop  : IsLoop ∙ \\ //  ε
    leftBol : LeftBol ∙

  open IsLoop isLoop public

record IsRightBolLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isLoop   : IsLoop ∙ \\ //  ε
    rightBol : RightBol ∙

  open IsLoop isLoop public

record IsMoufangLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isLoop           : IsLoop ∙ \\ // ε
    moufangIdentity  : MoufangIdentity₁ ∙
    moufangIdentity₂ : MoufangIdentity₂ ∙
    moufangIdentity₃ : MoufangIdentity₃ ∙
    moufangIdentity₄ : MoufangIdentity₄ ∙

  open IsLoop isLoop public

record IsPique (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isQuasigroup : IsQuasigroup ∙ \\ //
    idem         : Idempotent ∙

  open IsQuasigroup isQuasigroup public


text:
-- Andreas, 2016-10-04, issue #2236
-- Result splitting should not insert hidden arguments visibly

-- {-# OPTIONS -v interaction.case:100 #-}
-- {-# OPTIONS -v tc.cover:100 #-}
-- {-# OPTIONS -v reify.clause:100 #-}
-- {-# OPTIONS -v reify.implicit:100 #-}

splitMe : (A : Set) {B : Set} → Set
splitMe = {!!}  -- C-c C-c RET inserts hidden {B}

splitMe' : (A : Set) {B : Set} (C : Set) {D : Set} → Set
splitMe' = {!!}  -- C-c C-c RET inserts hidden {B} and {D}

splitMe'' : {B : Set} (C : Set) {D : Set} → Set
splitMe'' = {!!}  -- C-c C-c RET inserts hidden {D}

postulate
  N : Set
  P : N → Set

test : (A : Set) → ∀ {n} → P n → Set
test = {!!} -- C-c C-c RET inserts hidden {n}

-- Correct is:
-- No hidden arguments inserted on lhs.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Fragment.Algebra.Signature

module Fragment.Algebra.Free.Base (Σ : Signature) where

open import Fragment.Algebra.Algebra Σ
open import Fragment.Algebra.Free.Atoms public

open import Level using (Level; _⊔_)
open import Function using (_∘_)

open import Data.Empty using (⊥)
open import Data.Nat using (ℕ)
open import Data.Fin using (Fin)
open import Data.Vec using (Vec; []; _∷_)
open import Data.Vec.Relation.Binary.Pointwise.Inductive
  using (Pointwise; []; _∷_)

open import Relation.Binary using (Setoid; IsEquivalence)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)

private
  variable
    a ℓ : Level

module _ (A : Set a) where

  data Term : Set a where
    atom : A → Term
    term : ∀ {arity} → (f : ops Σ arity) → Vec Term arity → Term

module _ (S : Setoid a ℓ) where

  open Setoid S renaming (Carrier to A)

  data _~_ : Term A → Term A → Set (a ⊔ ℓ) where
      atom : ∀ {x y} → x ≈ y → atom x ~ atom y
      term : ∀ {arity xs ys} {f : ops Σ arity}
             → Pointwise _~_ xs ys
             → term f xs ~ term f ys

  private

    mutual
      map-~-refl : ∀ {n} {xs : Vec _ n} → Pointwise _~_ xs xs
      map-~-refl {xs = []}     = []
      map-~-refl {xs = x ∷ xs} = ~-refl ∷ map-~-refl

      ~-refl : ∀ {x} → x ~ x
      ~-refl {atom _}   = atom refl
      ~-refl {term _ _} = term map-~-refl

    mutual
      map-~-sym : ∀ {n} {xs ys : Vec _ n}
                   → Pointwise _~_ xs ys
                   → Pointwise _~_ ys xs
      map-~-sym [] = []
      map-~-sym (x≈y ∷ xs≈ys) =
        ~-sym x≈y ∷ map-~-sym xs≈ys

      ~-sym : ∀ {x y} → x ~ y → y ~ x
      ~-sym (atom x≈y)   = atom (sym x≈y)
      ~-sym (term xs≈ys) = term (map-~-sym xs≈ys)

    mutual
      map-~-trans : ∀ {n} {xs ys zs : Vec _ n}
                    → Pointwise _~_ xs ys
                    → Pointwise _~_ ys zs
                    → Pointwise _~_ xs zs
      map-~-trans [] [] = []
      map-~-trans (x≈y ∷ xs≈ys) (y≈z ∷ ys≈zs) =
        ~-trans x≈y y≈z ∷ map-~-trans xs≈ys ys≈zs

      ~-trans : ∀ {x y z} → x ~ y → y ~ z → x ~ z
      ~-trans (atom x≈y) (atom y≈z)     =
        atom (trans x≈y y≈z)
      ~-trans (term xs≈ys) (term ys≈zs) =
        term (map-~-trans xs≈ys ys≈zs)

    ~-isEquivalence : IsEquivalence _~_
    ~-isEquivalence = record { refl  = ~-refl
                             ; sym   = ~-sym
                             ; trans = ~-trans
                             }

  Herbrand : Setoid _ _
  Herbrand = record { Carrier       = Term A
                    ; _≈_           = _~_
                    ; isEquivalence = ~-isEquivalence
                    }

  Free : Algebra
  Free = record { ∥_∥/≈           = Herbrand
                ; ∥_∥/≈-isAlgebra = Free-isAlgebra
                }
    where term-cong : Congruence Herbrand term
          term-cong f p = term p

          Free-isAlgebra : IsAlgebra Herbrand
          Free-isAlgebra = record { ⟦_⟧     = term
                                  ; ⟦⟧-cong = term-cong
                                  }

F : ℕ → Algebra
F = Free ∘ Atoms (PE.setoid ⊥)

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
-- 2011-09-14 posted by Nisse
-- Andreas: this failed since SubstHH for Telescopes was wrong.
-- {-# OPTIONS --show-implicit -v tc.lhs.unify:15 #-}
module Issue292-14 where

data D : Set where
  d : D

postulate T : D → D → Set

data T′ (x y : D) : Set where
  c : T x y → T′ x y

F : D → D → Set
F x d = T′ x d  -- blocking unfolding of F x y

record [F] : Set where
  field
    x y : D
    f   : F x y -- T′ x y  works

data _≡_ (x : [F]) : [F] → Set where
  refl : x ≡ x

Foo : ∀ {x} {t₁ t₂ : T x d} →
      record { f = c t₁ } ≡ record { f = c t₂ } → Set₁
Foo refl = Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}
{-# OPTIONS --type-in-type #-}

-- Note: Using this module is discouraged unless absolutely necessary.
-- Use `Data.Product` or `Data.Both` instead.

module Light.Indexed where

open import Light.Level using (Level)

postulate ℓ : Level
record Indexed {aℓ} (𝕒 : Set aℓ) {aℓf : 𝕒 → Level} (𝕓 : ∀ a → Set (aℓf a)) : Set ℓ where
      constructor indexed
      field index : 𝕒
      field thing : 𝕓 index
open Indexed public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


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

module Cubical.Algebra.Group.Action where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Morphism
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Notation
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Structures.LeftAction
open import Cubical.Structures.Axioms
open import Cubical.Structures.Macro
open import Cubical.Structures.Auto
open import Cubical.Data.Sigma

private
  variable
    ℓ ℓ' : Level

record IsGroupAction (G : Group {ℓ = ℓ})
                     (H : Group {ℓ = ℓ'})
                     (_α_ : LeftActionStructure ⟨ G ⟩ ⟨ H ⟩) : Type (ℓ-max ℓ ℓ') where

  constructor isgroupaction

  open GroupNotationG G

  field
    isHom : (g : ⟨ G ⟩) → isGroupHom H H (g α_)
    identity : (h : ⟨ H ⟩) → 0ᴳ α h ≡ h
    assoc : (g g' : ⟨ G ⟩) → (h : ⟨ H ⟩) → (g +ᴳ g') α h ≡ g α (g' α h)

record GroupAction (G : Group {ℓ}) (H : Group {ℓ'}): Type (ℓ-suc (ℓ-max ℓ ℓ')) where

  constructor groupaction

  field
    _α_ : LeftActionStructure ⟨ G ⟩ ⟨ H ⟩
    isGroupAction : IsGroupAction G H _α_

module ActionΣTheory {ℓ ℓ' : Level} where

  module _ (G : Group {ℓ}) (H : Group {ℓ'}) (_α_ : LeftActionStructure ⟨ G ⟩ ⟨ H ⟩) where

    open GroupNotationG G

    IsGroupActionΣ : Type (ℓ-max ℓ ℓ')
    IsGroupActionΣ = ((g : ⟨ G ⟩) → isGroupHom H H (g α_))
                         × ((h : ⟨ H ⟩) → 0ᴳ α h ≡ h)
                         × ((g g' : ⟨ G ⟩) → (h : ⟨ H ⟩) → (g +ᴳ g') α h ≡ g α (g' α h))

    isPropIsGroupActionΣ : isProp IsGroupActionΣ
    isPropIsGroupActionΣ = isPropΣ isPropIsHom λ _ → isPropΣ isPropIdentity λ _ → isPropAssoc
      where
        isPropIsHom = isPropΠ (λ g → isPropIsGroupHom H H)
        isPropIdentity = isPropΠ (λ h → GroupStr.is-set (snd H) (0ᴳ α h) h)
        isPropAssoc = isPropΠ3 (λ g g' h → GroupStr.is-set (snd H) ((g +ᴳ g') α h) (g α (g' α h)))

    IsGroupAction→IsGroupActionΣ : IsGroupAction G H _α_ → IsGroupActionΣ
    IsGroupAction→IsGroupActionΣ (isgroupaction isHom identity assoc) = isHom , identity , assoc

    IsGroupActionΣ→IsGroupAction : IsGroupActionΣ → IsGroupAction G H _α_
    IsGroupActionΣ→IsGroupAction (isHom , identity , assoc) = isgroupaction isHom identity assoc

    IsGroupActionΣIso : Iso (IsGroupAction G H _α_) IsGroupActionΣ
    Iso.fun IsGroupActionΣIso = IsGroupAction→IsGroupActionΣ
    Iso.inv IsGroupActionΣIso = IsGroupActionΣ→IsGroupAction
    Iso.rightInv IsGroupActionΣIso = λ _ → refl
    Iso.leftInv IsGroupActionΣIso = λ _ → refl

open ActionΣTheory

isPropIsGroupAction : {ℓ ℓ' : Level }
                      (G : Group {ℓ}) (H : Group {ℓ'})
                      (_α_ : LeftActionStructure ⟨ G ⟩ ⟨ H ⟩)
                      → isProp (IsGroupAction G H _α_)
isPropIsGroupAction G H _α_ = isOfHLevelRespectEquiv 1
                                                     (invEquiv (isoToEquiv (IsGroupActionΣIso G H _α_)))
                                                     (isPropIsGroupActionΣ G H _α_)

module ActionNotationα {N : Group {ℓ}} {H : Group {ℓ'}} (Act : GroupAction H N) where
  _α_ = GroupAction._α_ Act
  private
    isGroupAction = GroupAction.isGroupAction Act
  α-id = IsGroupAction.identity isGroupAction
  α-hom = IsGroupAction.isHom isGroupAction
  α-assoc = IsGroupAction.assoc isGroupAction

module ActionLemmas {G : Group {ℓ}} {H : Group {ℓ'}} (Act : GroupAction G H) where
  open ActionNotationα {N = H} {H = G} Act
  open GroupNotationᴴ H
  open GroupNotationG G
  open MorphismLemmas {G = H} {H = H}
  open GroupLemmas

  abstract
    actOnUnit : (g : ⟨ G ⟩) → g α 0ᴴ ≡ 0ᴴ
    actOnUnit g = mapId (grouphom (g α_) (α-hom g))

    actOn-Unit : (g : ⟨ G ⟩) → g α (-ᴴ 0ᴴ) ≡ 0ᴴ
    actOn-Unit g = (cong (g α_) (invId H)) ∙ actOnUnit g

    actOn- : (g : ⟨ G ⟩) (h : ⟨ H ⟩) → g α (-ᴴ h) ≡ -ᴴ (g α h)
    actOn- g h = mapInv (grouphom (g α_) (α-hom g)) h

    -idAct : (h : ⟨ H ⟩) → (-ᴳ 0ᴳ) α h ≡ h
    -idAct h = (cong (_α h) (invId G)) ∙ (α-id h)

-- Examples
-- left adjoint action of a group on a normal subgroup

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
{-

This file contains:

- Properties of set truncations

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.SetTruncation.Properties where

open import Cubical.HITs.SetTruncation.Base

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

private
  variable
    ℓ : Level
    A : Type ℓ

-- lemma 6.9.1 in HoTT book
elim : {B : ∥ A ∥₀ → Type ℓ} →
  (Bset : (x : ∥ A ∥₀) → isSet (B x)) →
  (g : (a : A) → B (∣ a ∣₀)) →
  (x : ∥ A ∥₀) → B x
elim Bset g ∣ a ∣₀ = g a
elim {A = A} {B = B} Bset g (squash₀ x y p q i j) =
  isOfHLevel→isOfHLevelDep 2 Bset _ _
    (cong (elim Bset g) p) (cong (elim Bset g) q) (squash₀ x y p q) i j

setTruncUniversal : {B : Type ℓ} → (isSet B) → (∥ A ∥₀ → B) ≃ (A → B)
setTruncUniversal Bset = isoToEquiv (iso intro out leftInv rightInv)
  where
  intro = (λ h a → h ∣ a ∣₀)
  out = elim (λ x → Bset)

  leftInv : ∀ g → intro (out g) ≡ g
  leftInv g = refl

  rightInv : ∀ h → out (intro h) ≡ h
  rightInv h i x =
    elim (λ x → isProp→isSet (Bset (out (intro h) x) (h x))) (λ a → refl) x i

elim2 : {B : ∥ A ∥₀ → ∥ A ∥₀ → Type ℓ}
  (Bset : ((x y : ∥ A ∥₀) → isSet (B x y)))
  (g : (a b : A) → B ∣ a ∣₀ ∣ b ∣₀)
  (x y : ∥ A ∥₀) → B x y
elim2 Bset g =
  elim (λ _ → isOfHLevelPi 2 (λ _ → Bset _ _))
    (λ a → elim (λ _ → Bset _ _) (λ b → g a b))

elim3 : {B : (x y z : ∥ A ∥₀) → Type ℓ}
  (Bset : ((x y z : ∥ A ∥₀) → isSet (B x y z)))
  (g : (a b c : A) → B ∣ a ∣₀ ∣ b ∣₀ ∣ c ∣₀)
  (x y z : ∥ A ∥₀) → B x y z
elim3 Bset g =
  elim2 (λ _ _ → isOfHLevelPi 2 λ _ → Bset _ _ _)
    (λ a b → elim (λ _ → Bset _ _ _) (λ c → g a b c))

setTruncIsSet : isSet ∥ A ∥₀
setTruncIsSet a b p q = squash₀ a b p q

setId : isSet A → ∥ A ∥₀ ≡ A
setId {A = A} isset =
  isoToPath (iso (elim {A = A} (λ _ → isset) (λ x → x)) (λ x → ∣ x ∣₀) (λ b → refl) (λ b → idLemma b))
  where
  idLemma : ∀ (b : ∥ A ∥₀) → ∣ elim (λ x → isset) (λ x → x) b ∣₀ ≡ b
  idLemma b =
    elim {B = (λ x → ∣ elim (λ _ → isset) (λ x → x) x ∣₀ ≡ x)}
      (λ x → isOfHLevelSuc 2 (setTruncIsSet {A = A}) ∣ elim (λ _ → isset) (λ x₁ → x₁) x ∣₀ x)
      (λ _ → refl)
      b

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


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

open import Base
open import Homotopy.TruncatedHIT
open import Spaces.Spheres
open import Integers

module Sets.Quotient {i j} (A : Set i) ⦃ p : is-set A ⦄
  (R : A → A → Set j) ⦃ q : (x y : A) → is-prop (R x y) ⦄ where

private
  data _#/_ : Set (max i j) where
    #proj : A → _#/_

    #top : (f : hSⁿ ⟨0⟩ → _#/_) → _#/_

_/_ : Set (max i j)
_/_ = _#/_

proj : A → _/_
proj = #proj

postulate  -- HIT
  eq : (x y : A) (p : R x y) → proj x ≡ proj y

top : (f : hSⁿ ⟨0⟩ → _/_) → _/_
top = #top

postulate  -- HIT
  rays : (f : hSⁿ ⟨0⟩ → _/_) (x : hSⁿ ⟨0⟩) → top f ≡ f x

#/-rec : ∀ {k} (P : _/_ → Set k)
  (proj* : (x : A) → P (proj x))
  (eq* : (x y : A) (p : R x y) → transport P (eq x y p) (proj* x) ≡ proj* y)
  (top* : (f : hSⁿ ⟨0⟩ → _/_) (p : (x : hSⁿ ⟨0⟩) → P (f x)) → P (top f))
  (rays* : (f : hSⁿ ⟨0⟩ → _/_) (p : (x : hSⁿ ⟨0⟩) → P (f x)) (x : hSⁿ ⟨0⟩)
         → transport P (rays f x) (top* f p) ≡ p x)
  → ((t : _/_) → P t)
#/-rec P proj* eq* top* rays* (#proj x) = proj* x
#/-rec P proj* eq* top* rays* (#top f) =
  top* f (λ x → #/-rec P proj* eq* top* rays* (f x))

#/-rec-nondep : ∀ {k} (B : Set k)
  (proj* : A → B)
  (eq* : (x y : A) (p : R x y) → proj* x ≡ proj* y)
  (top* : (f : hSⁿ ⟨0⟩ → _/_) (p : hSⁿ ⟨0⟩ → B) → B)
  (rays* : (f : hSⁿ ⟨0⟩ → _/_) (p : hSⁿ ⟨0⟩ → B) (x : hSⁿ ⟨0⟩) → top* f p ≡ p x)
  → (_/_ → B)
#/-rec-nondep B proj* eq* top* rays* (#proj x) = proj* x
#/-rec-nondep B proj* eq* top* rays* (#top f) =
  top* f (λ x → #/-rec-nondep B proj* eq* top* rays* (f x))

/-rec :  ∀ {k} (P : _/_ → Set k)
  (proj* : (x : A) → P (proj x))
  (eq* : (x y : A) (p : R x y) → transport P (eq x y p) (proj* x) ≡ proj* y)
  (trunc : (x : _/_) → is-set (P x))
  → ((t : _/_) → P t)
/-rec P proj* eq* trunc = #/-rec P proj* eq*
                                 (λ f p₁ → π₁ (u f p₁))
                                 (λ f p₁ → π₂ (u f p₁)) where
  u : _
  u = truncated-has-filling-dep _/_ P ⟨0⟩ (λ ()) (λ f → (top f , rays f))

/-rec-nondep : ∀ {k} (B : Set k)
  (proj* : A → B)
  (eq* : (x y : A) (p : R x y) → proj* x ≡ proj* y)
  (trunc : is-set B)
  → (_/_ → B)
/-rec-nondep B proj* eq* trunc = #/-rec-nondep B proj* eq*
                                               (λ _ p → π₁ (u p))
                                               (λ _ p → π₂ (u p)) where
  u : _
  u = truncated-has-spheres-filled ⟨0⟩ _ trunc

-- Reduction rules for paths are not needed

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-# OPTIONS --allow-unsolved-metas #-}
-- When instantiating metas, we can't ignore variables occurring in
-- irrelevant terms. If we do the irrelevant terms will become illformed
-- (and we get __IMPOSSIBLE__s)
-- For instance
--   _42 := DontCare (Just (Var 0 []))
-- is a bad thing to do. In the example below we hit the __IMPOSSIBLE__ in
-- the rename function in TypeChecking.MetaVars.assign.
module DontIgnoreIrrelevantVars where

import Common.Level
import Common.Irrelevance

record Category : Set₁ where
  field
    .Arr : Set

postulate C : Category

_∙_ : ∀ {A : Set} {B : A → Set} {C : Set} →
      (∀ {x} → B x → C) → (g : ∀ x → B x) → A → C
f ∙ g = λ x → f (g x)

Exp : (I : Set) → Category
Exp I = record { Arr = I → Category.Arr C }

postulate
  Functor : Category → Set

postulate
  flattenP : ∀ D → Functor D → Functor D
  flattenHʳ : ∀ J → Functor (Exp J) → Functor (Exp J)

flattenH : ∀ I → Functor (Exp I) → Functor (Exp I)
flattenH I = flattenHʳ _ ∙ flattenP _


text:
module Categories.Support.Experimental where

open import Relation.Binary.PropositionalEquality.TrustMe

open import Categories.Support.PropositionalEquality

≣-relevant : ∀ {l} {A : Set l} {X Y : A} -> .(X ≣ Y) -> X ≣ Y
≣-relevant _ = trustMe

private
  ≣-coe : ∀ {a} {A B : Set a} → (A ≣ B) -> A -> B
  ≣-coe ≣-refl a = a

≣-subst′ : ∀ {a p} {A : Set a} → (P : A -> Set p) -> {x y : A} -> .(x ≣ y) -> P x -> P y
≣-subst′ P eq Px = ≣-coe (≣-relevant (≣-cong P eq)) Px

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

open import Polynomial.Parameters

module Polynomial.NormalForm.Construction
  {a ℓ}
  (coeffs : RawCoeff a ℓ)
  where

open import Relation.Nullary         using (Dec; yes; no)
open import Level                    using (lift; lower; _⊔_)
open import Data.Unit                using (tt)
open import Data.List                using (_∷_; []; List; foldr)
open import Data.Nat            as ℕ using (ℕ; suc; zero)
open import Data.Nat.Properties      using (z≤′n)
open import Data.Product             using (_×_; _,_; map₁; curry; uncurry)
open import Data.Maybe               using (just; nothing)
open import Data.Bool                using (if_then_else_; true; false)

open import Function

open import Polynomial.NormalForm.InjectionIndex
open import Polynomial.NormalForm.Definition coeffs

open RawCoeff coeffs

----------------------------------------------------------------------
-- Construction
--
-- Because the polynomial is stored in a canonical form, we use a
-- normalising cons operator to construct the coefficient lists.
----------------------------------------------------------------------

-- Decision procedure for Zero
zero? : ∀ {n} → (p : Poly n) → Dec (Zero p)
zero? (Σ _ Π _) = no (λ z → z)
zero? (Κ x Π _) with Zero-C x
... | true = yes tt
... | false = no (λ z → z)
{-# INLINE zero? #-}

-- Exponentiate the first variable of a polynomial
infixr 8 _⍓*_ _⍓+_
_⍓*_ : ∀ {n} → Coeff n * → ℕ → Coeff n *
_⍓+_ : ∀ {n} → Coeff n + → ℕ → Coeff n +

[] ⍓* _ = []
(∹ xs) ⍓* i = ∹ xs ⍓+ i

coeff (head (xs ⍓+ i)) = coeff (head xs)
pow (head (xs ⍓+ i)) = pow (head xs) ℕ.+ i
tail (xs ⍓+ i) = tail xs

infixr 5 _∷↓_
_∷↓_ : ∀ {n} → PowInd (Poly n) → Coeff n * → Coeff n *
x Δ i ∷↓ xs = case zero? x of
  λ { (yes p) → xs ⍓* suc i
    ; (no ¬p) → ∹ _≠0 x {¬p} Δ i & xs
    }
{-# INLINE _∷↓_ #-}

-- Inject a polynomial into a larger polynomoial with more variables
_Π↑_ : ∀ {n m} → Poly n → (suc n ≤′ m) → Poly m
(xs Π i≤n) Π↑ n≤m = xs Π (≤′-step i≤n ⟨ ≤′-trans ⟩ n≤m)
{-# INLINE _Π↑_ #-}

infixr 4 _Π↓_
_Π↓_ : ∀ {i n} → Coeff i * → suc i ≤′ n → Poly n
[]                        Π↓ i≤n = Κ 0# Π z≤′n
(∹ x ≠0 Δ zero  & []  ) Π↓ i≤n = x Π↑ i≤n
(∹ x    Δ zero  & ∹ xs) Π↓ i≤n = Σ (x Δ zero  & ∹ xs) Π i≤n
(∹ x    Δ suc j & xs  ) Π↓ i≤n = Σ (x Δ suc j & xs) Π i≤n
{-# INLINE _Π↓_ #-}

--------------------------------------------------------------------------------
-- These folds allow us to abstract over the proofs later: we try to avoid
-- using ∷↓ and Π↓ directly anywhere except here, so if we prove that this fold
-- acts the same on a normalised or non-normalised polynomial, we can prove th
-- same about any operation which uses it.
PolyF : ℕ → Set a
PolyF i = Poly i × Coeff i *

Fold : ℕ → Set a
Fold i = PolyF i → PolyF i

para : ∀ {i} → Fold i → Coeff i + → Coeff i *
para f (x ≠0 Δ i & []) = case f (x , []) of λ { (y , ys) → y Δ i ∷↓ ys }
para f (x ≠0 Δ i & ∹ xs) = case f (x , para f xs) of λ { (y , ys) → y Δ i ∷↓ ys }

poly-map : ∀ {i} → (Poly i → Poly i) → Coeff i + → Coeff i *
poly-map f = para (λ { (x , y) → (f x , y)})
{-# INLINE poly-map #-}

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


text:
-- Andreas, 2011-04-14
module UnificationUndecidedForNonStronglyRigidOccurrence where

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

data _≡_ {A : Set}(a : A) : A -> Set where
  refl : a ≡ a

i : (f : Nat -> Nat)(n : Nat) -> n ≡ f n -> Nat
i f n ()
-- this should fail, since n ≡ f n is not always empty, only in case of f=suc
-- thus, an occurrence does not always mean no match, only strict occurrences
-- mean that.


text:
{-# OPTIONS --safe #-}
module JVM.Compiler where

open import JVM.Types
open import JVM.Syntax.Instructions

module _ 𝑭 where
  open import JVM.Compiler.Monad StackTy ⟨ 𝑭 ∣_↝_⟩ noop using (Compiler) public

module _ {𝑭} where
  open import JVM.Compiler.Monad StackTy ⟨ 𝑭 ∣_↝_⟩ noop hiding (Compiler) public


text:
open import Data.Nat
open import Data.Nat.Properties
open import Data.Bool
open import Function.Base
open import Data.Product

-- Sizes are ordinals up to ω, i.e. naturals

𝕊 : Set
𝕊 = ℕ

hat : 𝕊 → 𝕊
hat = suc

-- Sized naturals and lists indexed by a size

data SNat : (k : 𝕊) → Set where
  SZero : (k : 𝕊) → SNat k
  SSucc : (k : 𝕊) → SNat k → SNat (hat k)

data SList (A : Set) : (k : 𝕊) → Set where
  SNil : (k : 𝕊) → SList A k
  SCons : (k : 𝕊) → A → SList A k → SList A (hat k)

-- Helpers to shift the size of lists up as needed

shift : ∀ {A k} → SList A k → SList A (suc k)
shift (SNil k) = SNil (suc k)
shift (SCons k hd tl) = SCons (suc k) hd (shift tl)

shiftBy : ∀ {A} → (k offset : 𝕊) → SList A k → SList A (k + offset)
shiftBy _ offset (SNil k) = SNil (k + offset)
shiftBy _ offset (SCons k hd tl) = SCons (k + offset) hd (shiftBy k offset tl)

-- Minus and div functions, no unrolling needed
-- Minus is size-preserving in the first argument, with an arbitrary second argument size
-- Div is the same, also happening to be size-preesrving in the first argument

minus : (k l : 𝕊) → SNat k → SNat l → SNat k
minus _ _ (SZero k) _ = SZero k
minus _ _ k (SZero l) = k
minus _ _ (SSucc k n) (SSucc l m) = SSucc k (minus k l n m)

div : (k l : 𝕊) → SNat k → SNat l → SNat k
div _ _ (SZero k) _ = SZero k
div _ _ (SSucc k n) m = SSucc _ (div k _ (minus k _ n m) m)

-- Size-preserving filter

filter : ∀ {A} → (k : 𝕊) → (A → Bool) → SList A k → SList A k
filter zero _ ls = ls
filter (suc k) _ (SNil _) = SNil _
filter (suc k) pred (SCons k hd tl) =
  if (pred hd)
  then SCons k hd (filter k pred tl)
  else shift (filter k pred tl)

-- Two appends: First one explicitly returns a list whose size is the sum of the input list sizes,
-- while the second one returns a list with *some* size, which we don't know is the sum of the sizes

append : ∀ {A} → (k l : 𝕊) → SList A k → SList A l → SList A (k + l)
append zero _ _ ls = ls
append k l (SNil _) ls rewrite (+-comm k l) = shiftBy l k ls
append (suc k) l (SCons k hd tl) ls = SCons (k + l) hd (append k l tl ls)

append' : ∀ {A} → (k l : 𝕊) → SList A k → SList A l → ∃[ kl ] SList A kl
append' zero l _ ls = l , ls
append' k l (SNil _) ls = l , ls
append' (suc k) l (SCons k hd tl) ls =
  let kl , kls = append' k l tl ls
  in  suc kl , SCons kl hd kls

-- Qsort returning a list of some size
-- The most specific size we could give it would probably be exponential
qsort : (k : 𝕊) → SList ℕ k → ∃[ k ] (SList ℕ k)
qsort zero ls = zero , ls
qsort k (SNil _) = k , SNil _
qsort (suc k) (SCons k hd tl) =
  let k1 , q1 = qsort k (filter k (_<ᵇ hd) tl)
      k2 , q2 = qsort k (filter k (not ∘ _<ᵇ_ hd) tl)
  in  suc (k1 + k2) , SCons (k1 + k2) hd (append k1 k2 q1 q2)

-- Longer example: base 2 logarithm

data LogDom : (s : 𝕊) → (p : ℕ) → Set where
  LogDom1 : (s : 𝕊) → LogDom s (suc zero)
  LogDom2 : (s : 𝕊) → (p : ℕ) → LogDom s (suc ⌊ p /2⌋) → LogDom (hat s) (suc (suc p))

postulate logdomInv : (s : 𝕊) → (p : ℕ) → LogDom (hat s) (suc (suc p)) → LogDom s (suc ⌊ p /2⌋)

max_stars_repo_name: ionathanch/msc-thesis

max_issues_repo_name: ionathanch/msc-thesis

max_forks_repo_name: ionathanch/msc-thesis


text:
module Impure.STLCRef.Welltyped where

open import Prelude
open import Data.Nat
open import Data.Vec
open import Data.List
open import Data.Fin hiding (_<_)
open import Extensions.List as L using ()

open import Impure.STLCRef.Syntax

-- store typings
World : Set
World = List Type

_⊢loc_∶_ : World → ℕ → Type → Set
Σ ⊢loc i ∶ A = Σ L.[ i ]= A

Ctx : (n : ℕ) → Set
Ctx n = Vec Type n

data _,_⊢_∶_ : ∀ {n} → Ctx n → World → Exp n → Type → Set where
  unit : ∀ {n} {Γ : Ctx n} {Σ} →
         ---------------------------------------
         Γ , Σ ⊢ unit ∶ Unit

  var  : ∀ {n i A} {Γ : Ctx n} {Σ} →
         Γ [ i ]= A →
         ---------------------------------------
         Γ , Σ ⊢ var i ∶ A

  loc : ∀ {n i A} {Γ : Ctx n} {Σ} →
         Σ ⊢loc i ∶ A →
         ---------------------------------------
         Γ , Σ ⊢ loc i ∶ Ref A

  ƛ   : ∀ {n e A B} {Γ : Ctx n} {Σ} →
         (A ∷ Γ) , Σ ⊢ e ∶ B →
         ---------------------------------------
         Γ , Σ ⊢ (ƛ A e) ∶ (A ⇒ B)

  _·_ : ∀ {n f x A B} {Γ : Ctx n} {Σ} →
         Γ , Σ ⊢ f ∶ (A ⇒ B) →
         Γ , Σ ⊢ x ∶ A →
         ---------------------------------------
         Γ , Σ ⊢ (f · x) ∶ B

  ref : ∀ {n x A} {Γ : Ctx n} {Σ} →
        Γ , Σ ⊢ x ∶ A →
        ---------------------------------------
        Γ , Σ ⊢ ref x ∶ Ref A

  !_  : ∀ {n x A} {Γ : Ctx n} {Σ} →
        Γ , Σ ⊢ x ∶ Ref A →
        ---------------------------------------
        Γ , Σ ⊢ (! x) ∶ A

  _≔_ : ∀ {n i x A} {Γ : Ctx n} {Σ} →
        Γ , Σ ⊢ i ∶ Ref A →
        Γ , Σ ⊢ x ∶ A →
        ---------------------------------------
        Γ , Σ ⊢ (i ≔ x) ∶ Unit

open import Relation.Binary.List.Pointwise

-- store welltypedness relation
-- as a pointwise lifting of the welltyped relation on closed expressions between a world and a store
_,_⊢_ : ∀ {n} → Ctx n → World → Store n → Set
Γ , Σ ⊢ μ = Rel (λ A x → Γ , Σ ⊢ proj₁ x ∶ A) Σ μ


text:
module STLC.Coquand.Soundness where

open import STLC.Coquand.Completeness public

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

-- Un⟦_⟧
postulate
  ⟦_⟧Un : ∀ {Γ Ξ A} → {ρ : Γ ⊩⋆ Ξ}
                    → (M : Ξ ⊢ A) → Un⋆ ρ
                    → Un (⟦ M ⟧ ρ)

-- 𝒰⋆⟦_⟧ₛ
postulate
  ⟦_⟧Un⋆ : ∀ {Γ Ξ Φ} → {ρ : Γ ⊩⋆ Ξ}
                     → (σ : Ξ ⊢⋆ Φ) → Un⋆ ρ
                     → Un⋆ (⟦ σ ⟧⋆ ρ)

postulate
  ⟦_⟧Eq : ∀ {Γ Ξ A} → {ρ₁ ρ₂ : Γ ⊩⋆ Ξ}
                    → (M : Ξ ⊢ A) → Eq⋆ ρ₁ ρ₂ → Un⋆ ρ₁ → Un⋆ ρ₂
                    → Eq (⟦ M ⟧ ρ₁) (⟦ M ⟧ ρ₂)

-- Eq⋆⟦_⟧ₛ
postulate
  ⟦_⟧Eq⋆ : ∀ {Γ Ξ Φ} → {ρ₁ ρ₂ : Γ ⊩⋆ Ξ}
                     → (σ : Ξ ⊢⋆ Φ) → Eq⋆ ρ₁ ρ₂ → Un⋆ ρ₁ → Un⋆ ρ₂
                     → Eq⋆ (⟦ σ ⟧⋆ ρ₁) (⟦ σ ⟧⋆ ρ₂)

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

-- ⟦_⟧⬗Eq = symEq ∘ ↑⟨_⟩Eq⟦_⟧
⟦_⟧⬗Eq : ∀ {Γ Γ′ Ξ A} → {ρ : Γ ⊩⋆ Ξ}
                      → (M : Ξ ⊢ A) (η : Γ′ ∋⋆ Γ) → Un⋆ ρ
                      → Eq (⟦ M ⟧ (η ⬗ ρ))
                            (acc η (⟦ M ⟧ ρ))

⟦_⟧⬗Eq (𝓋 i)   η υ = get⬗Eq η i υ

⟦_⟧⬗Eq (ƛ M)   η υ = eq⊃ (λ η′ u →
                           ⟦ M ⟧Eq (comp⬗◇Eq⋆ η′ η υ , reflEq u)
                                   (cong⬗Un⋆ η′ (cong⬗Un⋆ η υ) , u)
                                   (cong⬗Un⋆ (η′ ○ η) υ , u))

⟦_⟧⬗Eq (M ∙ N) η υ =
    cong⟦∙⟧Eq idᵣ (⟦ M ⟧⬗Eq η υ) (⟦ M ⟧Un (cong⬗Un⋆ η υ)) (congaccUn η (⟦ M ⟧Un υ))
                  (⟦ N ⟧⬗Eq η υ) (⟦ N ⟧Un (cong⬗Un⋆ η υ)) (congaccUn η (⟦ N ⟧Un υ))
  ⦙ acc⟦∙⟧idEq η (⟦ M ⟧Un υ) (congaccUn η (⟦ N ⟧Un υ))
  ⦙ (cong⟦∙⟧Eq η ((lidaccEq (⟦ M ⟧Un υ)) ⁻¹) (⟦ M ⟧Un υ) (congaccUn idᵣ (⟦ M ⟧Un υ))
                 (reflEq (congaccUn η (⟦ N ⟧Un υ))) (congaccUn η (⟦ N ⟧Un υ)) (congaccUn η (⟦ N ⟧Un υ))
  ⦙ acc⟦∙⟧Eq idᵣ η (⟦ M ⟧Un υ) (⟦ N ⟧Un υ))

-- ⟦_⟧⬗Eq⋆ = symEq ∘ ↑⟨_⟩Eq⋆⟦_⟧ₛ
⟦_⟧⬗Eq⋆ : ∀ {Γ Γ′ Ξ Φ} → {ρ : Γ ⊩⋆ Ξ}
                       → (σ : Ξ ⊢⋆ Φ) (η : Γ′ ∋⋆ Γ) → Un⋆ ρ
                       → Eq⋆ (⟦ σ ⟧⋆ (η ⬗ ρ))
                              (η ⬗ ⟦ σ ⟧⋆ ρ)
⟦_⟧⬗Eq⋆ ∅       η υ = ∅
⟦_⟧⬗Eq⋆ (σ , M) η υ = ⟦ σ ⟧⬗Eq⋆ η υ , ⟦ M ⟧⬗Eq η υ

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

-- TODO: Generalise to zap⬖
postulate
  aux₄₈₁ : ∀ {Γ Ξ A} → {ρ : Γ ⊩⋆ Ξ} {a : Γ ⊩ A}
                     → Un⋆ ρ
                     → Eq⋆ ((ρ , a) ⬖ wkᵣ idᵣ) ρ

-- TODO
-- Basic properties of _◇_
-- Advanced properties of _◇_
-- Basic properties of _⬗_
-- Basic properties of _◆_
-- Advanced properties of _⬗_
-- Advanced properties of _◆_

-- TODO: Fix the instance argument problem; abstract over models; rename η to ξ…

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

renlift⟦_⟧Eq : ∀ {Γ Γ′ A B w w′} → {ρ : w ⊩⋆ Γ′} {a : w′ ⊩ A}
                                 → (M : Γ , A ⊢ B) (η₁ : Γ′ ∋⋆ Γ) (η₂ : w′ ∋⋆ w) → Un⋆ ρ → Un a
                                 → Eq (⟦ ren (liftᵣ {A} η₁) M ⟧ (η₂ ⬗ ρ , a))
                                       (⟦ M ⟧ (η₂ ⬗ (ρ ⬖ η₁) , a))

renlift⟦_⟧Eq (𝓋 zero) η₁ η₂ υ u = reflEq u

renlift⟦_⟧Eq {ρ = ρ} {a} (𝓋 (suc i)) η₁ η₂ υ u =
    ≡→Eq ((getᵥ (η₂ ⬗ ρ , a)) & natgetᵣ η₁ i)
          (conggetUn (getᵣ (wkᵣ η₁) i) (cong⬗Un⋆ η₂ υ , u))
  ⦙ get⬖Eq η₁ (getᵣ η₁ i) i (cong⬗Un⋆ η₂ υ) ⁻¹
  ⦙ conggetEq i (comp⬗⬖Eq⋆ η₂ η₁ υ ⁻¹)

renlift⟦_⟧Eq (ƛ M) η₁ η₂ υ u =
      eq⊃ (λ η′ u′ → renlift⟦ M ⟧Eq (liftᵣ η₁) η′ (cong⬗Un⋆ η₂ υ , u) u′
                    ⦙ ⟦ M ⟧Eq ( ( cong⬗Eq⋆ η′ (( comp⬗⬖Eq⋆ η₂ η₁ υ
                                               ⦙ zap⬖Eq⋆ (wkᵣ η₁) η₁ (cong⬗Un⋆ η₂ υ) ⁻¹
                                               ) ⁻¹)
                                , reflEq (congaccUn η′ u)
                                )
                              , reflEq u′
                              )
                              ((cong⬗Un⋆ η′ (cong⬖Un⋆ (wkᵣ η₁) (cong⬗Un⋆ η₂ υ , u)) , congaccUn η′ u) , u′)
                              ((cong⬗Un⋆ η′ (cong⬗Un⋆ η₂ (cong⬖Un⋆ η₁ υ)) , congaccUn η′ u) , u′))

renlift⟦_⟧Eq (M ∙ N) η₁ η₂ υ u =
  cong⟦∙⟧Eq idᵣ (renlift⟦ M ⟧Eq η₁ η₂ υ u) (⟦ ren (liftᵣ η₁) M ⟧Un (cong⬗Un⋆ η₂ υ , u)) (⟦ M ⟧Un (cong⬗Un⋆ η₂ (cong⬖Un⋆ η₁ υ) , u))
                (renlift⟦ N ⟧Eq η₁ η₂ υ u) (⟦ ren (liftᵣ η₁) N ⟧Un (cong⬗Un⋆ η₂ υ , u)) (⟦ N ⟧Un (cong⬗Un⋆ η₂ (cong⬖Un⋆ η₁ υ) , u))

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

renwk⟦_⟧Eq : ∀ {Γ Γ′ A C w} → {ρ : w ⊩⋆ Γ′} {a : w ⊩ A}
                            → (M : Γ ⊢ C) (η : Γ′ ∋⋆ Γ) → Un⋆ ρ → Un a
                            → Eq (⟦ ren (wkᵣ {A} η) M ⟧ (ρ , a))
                                  (⟦ M ⟧ (ρ ⬖ η))

renwk⟦_⟧Eq (𝓋 i) η υ u =
    get⬖Eq (wkᵣ η) (getᵣ (wkᵣ η) i) i (υ , u) ⁻¹
  ⦙ conggetEq i (zap⬖Eq⋆ (wkᵣ η) η υ)

renwk⟦_⟧Eq (ƛ M) η υ u =
  eq⊃ (λ η′ u′ → renlift⟦ M ⟧Eq (wkᵣ η) η′ (υ , u) u′
                ⦙ ⟦ M ⟧Eq (cong⬗Eq⋆ η′ (zap⬖Eq⋆ (wkᵣ η) η υ) , reflEq u′)
                          (cong⬗Un⋆ η′ (cong⬖Un⋆ (wkᵣ η) (υ , u)) , u′)
                          (cong⬗Un⋆ η′ (cong⬖Un⋆ η υ) , u′))

renwk⟦_⟧Eq (M ∙ N) η υ u =
  cong⟦∙⟧Eq idᵣ (renwk⟦ M ⟧Eq η υ u) (⟦ ren (wkᵣ η) M ⟧Un (υ , u)) (⟦ M ⟧Un (cong⬖Un⋆ η υ))
                (renwk⟦ N ⟧Eq η υ u) (⟦ ren (wkᵣ η) N ⟧Un (υ , u)) (⟦ N ⟧Un (cong⬖Un⋆ η υ))

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

wk⟦_⟧Eq : ∀ {Γ A C w} → {ρ : w ⊩⋆ Γ} {a : w ⊩ A}
                      → (M : Γ ⊢ C) → Un⋆ ρ → Un a
                      → Eq (⟦ wk {A} M ⟧ (ρ , a))
                            (⟦ M ⟧ ρ)
wk⟦_⟧Eq M υ u = renwk⟦ M ⟧Eq idᵣ υ u
              ⦙ ⟦ M ⟧Eq (rid⬖Eq⋆ υ) (cong⬖Un⋆ idᵣ υ) υ

wk⟦_⟧Eq⋆ : ∀ {Γ Ξ A w} → {ρ : w ⊩⋆ Γ} {a : w ⊩ A}
                       → (σ : Γ ⊢⋆ Ξ) → Un⋆ ρ → Un a
                       → Eq⋆ (⟦ wkₛ {A} σ ⟧⋆ (ρ , a))
                              (⟦ σ ⟧⋆ ρ)
wk⟦_⟧Eq⋆ ∅       υ u = ∅
wk⟦_⟧Eq⋆ (σ , M) υ u = wk⟦ σ ⟧Eq⋆ υ u , wk⟦ M ⟧Eq υ u

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

get⟦_⟧Eq : ∀ {Γ Ξ A w} → {ρ : w ⊩⋆ Γ}
                       → (σ : Γ ⊢⋆ Ξ) (i : Ξ ∋ A) → Un⋆ ρ
                       → Eq (⟦ getₛ σ i ⟧ ρ)
                             (getᵥ (⟦ σ ⟧⋆ ρ) i)
get⟦_⟧Eq (σ , M) zero    υ = reflEq (⟦ M ⟧Un υ)
get⟦_⟧Eq (σ , M) (suc i) υ = get⟦ σ ⟧Eq i υ

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

sublift⟦_⟧Eq : ∀ {Γ Ξ A B w} → {ρ : w ⊩⋆ Γ} {a : w ⊩ A}
                             → (M : Ξ , A ⊢ B) (σ : Γ ⊢⋆ Ξ) → Un⋆ ρ → Un a
                             → Eq (⟦ sub (liftₛ {A} σ) M ⟧ (ρ , a))
                                   (⟦ M ⟧ (⟦ σ ⟧⋆ ρ , a))

sublift⟦_⟧Eq (𝓋 zero) σ υ u = reflEq u

sublift⟦_⟧Eq {ρ = ρ} {a} (𝓋 (suc i)) σ υ u =
    ≡→Eq ((λ M′ → ⟦ M′ ⟧ (ρ , a)) & natgetₛ σ i)
          (⟦ getₛ (wkₛ σ) i ⟧Un (υ , u))
  ⦙ wk⟦ getₛ σ i ⟧Eq υ u
  ⦙ get⟦ σ ⟧Eq i υ

sublift⟦_⟧Eq (ƛ M) σ υ u =
  eq⊃ (λ η′ u′ → sublift⟦ M ⟧Eq (liftₛ σ) (cong⬗Un⋆ η′ υ , congaccUn η′ u) u′
                ⦙ ⟦ M ⟧Eq ((⟦ wkₛ σ ⟧⬗Eq⋆ η′ (υ , u) , reflEq (congaccUn η′ u)) , reflEq u′)
                          ((⟦ wkₛ σ ⟧Un⋆ (cong⬗Un⋆ η′ υ , congaccUn η′ u) , congaccUn η′ u) , u′)
                          ((cong⬗Un⋆ η′ (⟦ wkₛ σ ⟧Un⋆ (υ , u)) , congaccUn η′ u) , u′)
                ⦙ ⟦ M ⟧Eq ((cong⬗Eq⋆ η′ (wk⟦ σ ⟧Eq⋆ υ u) , reflEq (congaccUn η′ u)) , reflEq u′)
                          ((cong⬗Un⋆ η′ (⟦ wkₛ σ ⟧Un⋆ (υ , u)) , congaccUn η′ u) , u′)
                          ((cong⬗Un⋆ η′ (⟦ σ ⟧Un⋆ υ) , congaccUn η′ u) , u′))

sublift⟦_⟧Eq (M ∙ N) σ υ u =
  cong⟦∙⟧Eq idᵣ (sublift⟦ M ⟧Eq σ υ u) (⟦ sub (liftₛ σ) M ⟧Un (υ , u)) (⟦ M ⟧Un (⟦ σ ⟧Un⋆ υ , u))
                (sublift⟦ N ⟧Eq σ υ u) (⟦ sub (liftₛ σ) N ⟧Un (υ , u)) (⟦ N ⟧Un (⟦ σ ⟧Un⋆ υ , u))

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

subliftwk⟦_⟧Eq : ∀ {Γ Ξ A A′ B w w′} → {ρ : w ⊩⋆ Γ} {a : w ⊩ A} {a′ : w′ ⊩ A′}
                                     → (M : Ξ , A′ ⊢ B) (σ : Γ ⊢⋆ Ξ) (η : w′ ∋⋆ w) → Un⋆ ρ → Un a → Un a′
                                     → Eq (⟦ sub (liftₛ (wkₛ σ)) M ⟧ (η ⬗ ρ , acc η a , a′))
                                           (⟦ sub (liftₛ σ) M ⟧ (η ⬗ ρ , a′))
subliftwk⟦_⟧Eq M σ η υ u u′ = sublift⟦ M ⟧Eq (wkₛ σ) (cong⬗Un⋆ η υ , congaccUn η u) u′
                            ⦙ ⟦ M ⟧Eq (wk⟦ σ ⟧Eq⋆ (cong⬗Un⋆ η υ) (congaccUn η u) , reflEq u′)
                                      (⟦ wkₛ σ ⟧Un⋆ (cong⬗Un⋆ η υ , congaccUn η u) , u′)
                                      (⟦ σ ⟧Un⋆ (cong⬗Un⋆ η υ) , u′)
                            ⦙ sublift⟦ M ⟧Eq σ (cong⬗Un⋆ η υ) u′ ⁻¹

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

subwk⟦_⟧Eq : ∀ {Γ Ξ A C w} → {ρ : w ⊩⋆ Γ} {a : w ⊩ A}
                           → (M : Ξ ⊢ C) (σ : Γ ⊢⋆ Ξ) → Un⋆ ρ → Un a
                           → Eq (⟦ sub (wkₛ {A} σ) M ⟧ (ρ , a))
                                 (⟦ sub σ M ⟧ ρ)

subwk⟦_⟧Eq {ρ = ρ} {a} (𝓋 i) σ υ u =
    ≡→Eq ((λ M′ → ⟦ M′ ⟧ (ρ , a)) & (natgetₛ σ i))
          (⟦ getₛ (wkₛ σ) i ⟧Un (υ , u))
  ⦙ wk⟦ getₛ σ i ⟧Eq υ u

subwk⟦_⟧Eq (ƛ {A = A′} M) σ υ u =
  eq⊃ (λ η u′ → subliftwk⟦ M ⟧Eq σ η υ u u′)

subwk⟦_⟧Eq (M ∙ N) σ υ u =
  cong⟦∙⟧Eq idᵣ (subwk⟦ M ⟧Eq σ υ u) (⟦ sub (wkₛ σ) M ⟧Un (υ , u)) (⟦ sub σ M ⟧Un υ)
                (subwk⟦ N ⟧Eq σ υ u) (⟦ sub (wkₛ σ) N ⟧Un (υ , u)) (⟦ sub σ N ⟧Un υ)

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

sub⟦_⟧Eq : ∀ {Γ Ξ A w} → {ρ : w ⊩⋆ Γ}
                       → (M : Ξ ⊢ A) (σ : Γ ⊢⋆ Ξ) → Un⋆ ρ
                       → Eq (⟦ sub σ M ⟧ ρ)
                             (⟦ M ⟧ (⟦ σ ⟧⋆ ρ))

sub⟦_⟧Eq (𝓋 i) σ υ = get⟦ σ ⟧Eq i υ

sub⟦_⟧Eq (ƛ M) σ υ =
  eq⊃ (λ η u → sublift⟦ M ⟧Eq σ (cong⬗Un⋆ η υ) u
              ⦙ ⟦ M ⟧Eq (⟦ σ ⟧⬗Eq⋆ η υ , reflEq u)
                        (⟦ σ ⟧Un⋆ (cong⬗Un⋆ η υ) , u)
                        (cong⬗Un⋆ η (⟦ σ ⟧Un⋆ υ) , u))

sub⟦_⟧Eq (M ∙ N) σ υ =
  cong⟦∙⟧Eq idᵣ (sub⟦ M ⟧Eq σ υ) (⟦ sub σ M ⟧Un υ) (⟦ M ⟧Un (⟦ σ ⟧Un⋆ υ))
                (sub⟦ N ⟧Eq σ υ) (⟦ sub σ N ⟧Un υ) (⟦ N ⟧Un (⟦ σ ⟧Un⋆ υ))

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

-- TODO: Rename this
sublift⟦⟧Eq⁈ : ∀ {Γ Ξ A B w} → {ρ : w ⊩⋆ Γ}
                             → (σ : Γ ⊢⋆ Ξ) (M : Ξ , A ⊢ B) (N : Γ ⊢ A) → Un⋆ ρ
                             → Eq (⟦ sub (liftₛ {A} σ) M ⟧ (ρ , ⟦ N ⟧ ρ))
                                   (⟦ sub (σ , N) M ⟧ ρ)
sublift⟦⟧Eq⁈ {ρ = ρ} σ M N υ = sublift⟦ M ⟧Eq σ υ (⟦ N ⟧Un υ)
                             ⦙ sub⟦ M ⟧Eq (σ , N) υ ⁻¹

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

-- TODO: Generalise theorem 4 over models

module _ where
  open 𝔐 canon

  mutual
    lemƛ : ∀ {Γ A B w} → {ρ : w ⊩⋆ Γ} {M M′ : Γ , A ⊢ B}
                       → M ∼ M′ → Un⋆ ρ
                       → Eq (⟦ ƛ M ⟧ ρ) (⟦ ƛ M′ ⟧ ρ)
    lemƛ p υ = eq⊃ (λ xs u → cong⟦ p ⟧Eq (cong⬗Un⋆ xs υ , u))

    lem∙ : ∀ {Γ A B w} → {ρ : w ⊩⋆ Γ} {M M′ : Γ ⊢ A ⇒ B} {N N′ : Γ ⊢ A}
                       → M ∼ M′ → N ∼ N′ → Un⋆ ρ
                       → Eq (⟦ M ∙ N ⟧ ρ) (⟦ M′ ∙ N′ ⟧ ρ)
    lem∙ {M = M} {M′} {N} {N′} p q υ = cong⟦∙⟧Eq idᵣ (cong⟦ p ⟧Eq υ) (⟦ M ⟧Un υ) (⟦ M′ ⟧Un υ)
                                                     (cong⟦ q ⟧Eq υ) (⟦ N ⟧Un υ) (⟦ N′ ⟧Un υ)

    lemred⇒ : ∀ {Γ Ξ A B w} → {ρ : w ⊩⋆ Γ}
                             → (σ : Γ ⊢⋆ Ξ) (M : Ξ , A ⊢ B) (N : Γ ⊢ A) → Un⋆ ρ
                             → Eq (⟦ sub σ (ƛ M) ∙ N ⟧ ρ) (⟦ sub (σ , N) M ⟧ ρ)
    lemred⇒ {ρ = ρ} σ M N υ =
        ⟦ sub (liftₛ σ) M ⟧Eq (lid⬗Eq⋆ υ , reflEq (⟦ N ⟧Un υ))
                              (cong⬗Un⋆ idᵣ υ , ⟦ N ⟧Un υ)
                              (υ , ⟦ N ⟧Un υ)
      ⦙ sublift⟦⟧Eq⁈ σ M N υ

    lemexp⇒ : ∀ {Γ A B w} → {ρ : w ⊩⋆ Γ}
                           → (M : Γ ⊢ A ⇒ B) → Un⋆ ρ
                           → Eq (⟦ M ⟧ ρ) (⟦ ƛ (wk M ∙ 0) ⟧ ρ)
    lemexp⇒ {ρ = ρ} M υ =
      eq⊃ (λ η {a} u → acc⟦∙⟧idEq η (⟦ M ⟧Un υ) u ⁻¹
                      ⦙ cong⟦∙⟧Eq idᵣ (⟦ M ⟧⬗Eq η υ ⁻¹) (congaccUn η (⟦ M ⟧Un υ)) (⟦ M ⟧Un (cong⬗Un⋆ η υ))
                                      (reflEq u) u u
                      ⦙ cong⟦∙⟧Eq idᵣ (wk⟦ M ⟧Eq (cong⬗Un⋆ η υ) u ⁻¹) (⟦ M ⟧Un (cong⬗Un⋆ η υ)) (⟦ wk M ⟧Un (cong⬗Un⋆ η υ , u))
                                      (reflEq u) u u)

    -- Theorem 4.
    cong⟦_⟧Eq : ∀ {Γ A w} → {M M′ : Γ ⊢ A} {ρ : w ⊩⋆ Γ}
                          → M ∼ M′ → Un⋆ ρ
                          → Eq (⟦ M ⟧ ρ) (⟦ M′ ⟧ ρ)
    cong⟦ refl∼ {M = M} ⟧Eq υ = reflEq (⟦ M ⟧Un υ)
    cong⟦ p ⁻¹∼ ⟧Eq         υ = cong⟦ p ⟧Eq υ ⁻¹
    cong⟦ p ⦙∼ q ⟧Eq        υ = cong⟦ p ⟧Eq υ ⦙ cong⟦ q ⟧Eq υ
    cong⟦ ƛ∼ p ⟧Eq          υ = lemƛ p υ
    cong⟦ p ∙∼ q ⟧Eq        υ = lem∙ p q υ
    cong⟦ red⇒ σ M N ⟧Eq   υ = lemred⇒ σ M N υ
    cong⟦ exp⇒ M ⟧Eq       υ = lemexp⇒ M υ

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

-- Theorem 5.
thm₅ : ∀ {Γ A} → (M M′ : Γ ⊢ A) → nf M ≡ nf M′
               → M ∼ M′
thm₅ M M′ p = thm₂ M
            ⦙ ≡→∼ p
            ⦙ (thm₂ M′ ⁻¹)

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

-- proj⟨_⟩𝒰⋆
⌊_⌋ᵤ : ∀ {Γ Γ′} → (η : Γ′ ∋⋆ Γ)
                → Un⋆ ⌊ η ⌋ᵥ
⌊ ∅ ⌋ᵤ     = ∅
⌊ η , i ⌋ᵤ = ⌊ η ⌋ᵤ , ⟪𝓋 i ⟫ᵤ

-- refl𝒰⋆
idᵤ : ∀ {Γ} → Un⋆ (idᵥ {Γ})
idᵤ = ⌊ idᵣ ⌋ᵤ

-- Theorem 6.
thm₆ : ∀ {Γ A} → (M M′ : Γ ⊢ A) → M ∼ M′
               → nf M ≡ nf M′
thm₆ M M′ p = cor₁ M M′ (cong⟦ p ⟧Eq idᵤ)

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

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


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

open import Cubical.Algebra.Group.Base public
open import Cubical.Algebra.Group.Properties public
open import Cubical.Algebra.Group.GroupPath public
open import Cubical.Algebra.Group.DirProd public
open import Cubical.Algebra.Group.Morphisms public
open import Cubical.Algebra.Group.MorphismProperties public
open import Cubical.Algebra.Group.Subgroup public
open import Cubical.Algebra.Group.QuotientGroup public
open import Cubical.Algebra.Group.IsomorphismTheorems public
open import Cubical.Algebra.Group.Instances.Unit public
open import Cubical.Algebra.Group.Instances.Bool public
open import Cubical.Algebra.Group.Instances.Int public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
-- Andreas, 2020-04-15, issue #4586
-- Better error for invalid let pattern.

import Agda.Builtin.Nat

test : Set₁
test = let 13 = Set
       in  Set

-- WAS:
-- Set != x of type Set₁
-- when checking that the given dot pattern Set matches the inferred
-- value x

-- EXPECTED:
-- Not a valid let pattern
-- when scope checking let .Set = Set in Set

max_forks_repo_name: shlevy/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A binary representation of natural numbers
------------------------------------------------------------------------

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

module Data.Bin where

open import Data.Nat as Nat
  using (ℕ; zero; z≤n; s≤s) renaming (suc to 1+_)
open import Data.Digit  using (fromDigits; toDigits; Bit)
open import Data.Fin as Fin using (Fin; zero)
  renaming (suc to 1+_)
open import Data.Fin.Properties as FP using (_+′_)
open import Data.List.Base as List hiding (downFrom)
open import Function
open import Data.Product using (uncurry; _,_; _×_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
  using (_≡_; _≢_; refl; sym)
open import Relation.Nullary
open import Relation.Nullary.Decidable

------------------------------------------------------------------------
-- Bits

pattern 0b = zero
pattern 1b = 1+ zero
pattern ⊥b = 1+ 1+ ()

------------------------------------------------------------------------
-- The type

-- A representation of binary natural numbers in which there is
-- exactly one representative for every number. The function toℕ below
-- defines the meaning of Bin.

-- `bs 1#` stands for the binary number "1<reverse bs>" e.g.
-- `(0b ∷ [])           1#` represents "10"
-- `(0b ∷ 1b ∷ 1b ∷ []) 1#` represents "1110"

Bin⁺ : Set
Bin⁺ = List Bit

infix 8 _1#

data Bin : Set where
  0#  : Bin
  _1# : (bs : Bin⁺) → Bin

------------------------------------------------------------------------
-- Conversion functions

-- Converting to a list of bits starting with the _least_ significant
-- one.

toBits : Bin → List Bit
toBits 0#      = [ 0b ]
toBits (bs 1#) = bs ++ [ 1b ]

-- Converting to a natural number.

toℕ : Bin → ℕ
toℕ = fromDigits ∘ toBits

-- Converting from a list of bits, starting with the _least_
-- significant one.

fromBits : List Bit → Bin
fromBits []        = 0#
fromBits (b  ∷ bs) with fromBits bs
fromBits (b  ∷ bs) | bs′ 1# = (b ∷ bs′) 1#
fromBits (0b ∷ bs) | 0#     = 0#
fromBits (1b ∷ bs) | 0#     = [] 1#
fromBits (⊥b ∷ bs) | _

private
  pattern 2+_ n = 1+ 1+ n

  ntoBits′ : ℕ → ℕ → List Bit
  ntoBits′     0      _  = []
  ntoBits′     1      0  = 0b ∷ 1b ∷ []
  ntoBits′     1      1  = 1b ∷ []
  ntoBits′ (2+ k)     0  = 0b ∷ ntoBits′ (1+ k) k
  ntoBits′ (2+ k)     1  = 1b ∷ ntoBits′ (1+ k) (1+ k)
  ntoBits′ (1+ k) (2+ n) = ntoBits′ k n

  ntoBits : ℕ → List Bit
  ntoBits n = ntoBits′ n n

-- Converting from a natural number.

fromℕ : ℕ → Bin
fromℕ n = fromBits $ ntoBits n

------------------------------------------------------------------------
-- Order relation.

-- Wrapped so that the parameters can be inferred.

infix 4 _<_

data _<_ (b₁ b₂ : Bin) : Set where
  less : (lt : (Nat._<_ on toℕ) b₁ b₂) → b₁ < b₂

less-injective : ∀ {b₁ b₂} {lt₁ lt₂} → (b₁ < b₂ ∋ less lt₁) ≡ less lt₂ → lt₁ ≡ lt₂
less-injective refl = refl

------------------------------------------------------------------------
-- Arithmetic

-- Power of two.

infixr 8 2^_

2^_ : ℕ → Bin⁺
2^ 0      = []
2^ (1+ n) = 0b ∷ 2^ n

-- Base 2 logarithm (rounded downwards).

⌊log₂_⌋ : Bin⁺ → ℕ
⌊log₂ (b ∷ bs) ⌋ = 1+ ⌊log₂ bs ⌋
⌊log₂ []       ⌋ = 0

-- Multiplication by 2.

infix 7 _*2 _*2+1

_*2 : Bin → Bin
0#      *2 = 0#
(bs 1#) *2 = (0b ∷ bs) 1#

_*2+1 : Bin → Bin
0#      *2+1 = [] 1#
(bs 1#) *2+1 = (1b ∷ bs) 1#

-- Division by 2, rounded downwards.

⌊_/2⌋ : Bin → Bin
⌊ 0#          /2⌋ = 0#
⌊ [] 1#       /2⌋ = 0#
⌊ (b ∷ bs) 1# /2⌋ = bs 1#

-- Addition.

Carry : Set
Carry = Bit

addBits : Carry → Bit → Bit → Carry × Bit
addBits c b₁ b₂ with c +′ (b₁ +′ b₂)
... | zero           = (0b , 0b)
... | 1+ zero        = (0b , 1b)
... | 1+ 1+ zero     = (1b , 0b)
... | 1+ 1+ 1+ zero  = (1b , 1b)
... | 1+ 1+ 1+ 1+ ()

addCarryToBitList : Carry → List Bit → List Bit
addCarryToBitList 0b bs        = bs
addCarryToBitList 1b []        = 1b ∷ []
addCarryToBitList 1b (0b ∷ bs) = 1b ∷ bs
addCarryToBitList 1b (1b ∷ bs) = 0b ∷ addCarryToBitList 1b bs
addCarryToBitList ⊥b _
addCarryToBitList _  (⊥b ∷ _)

addBitLists : Carry → List Bit → List Bit → List Bit
addBitLists c []         bs₂        = addCarryToBitList c bs₂
addBitLists c bs₁        []         = addCarryToBitList c bs₁
addBitLists c (b₁ ∷ bs₁) (b₂ ∷ bs₂) with addBits c b₁ b₂
... | (c' , b') = b' ∷ addBitLists c' bs₁ bs₂

infixl 6 _+_

_+_ : Bin → Bin → Bin
m + n = fromBits (addBitLists 0b (toBits m) (toBits n))

-- Multiplication.

infixl 7 _*_

_*_ : Bin → Bin → Bin
0#                  * n = 0#
[]               1# * n = n
-- (b + 2 * bs 1#) * n = b * n + 2 * (bs 1# * n)
(b  ∷ bs) 1# * n with bs 1# * n
(b  ∷ bs) 1# * n | 0#     = 0#
(0b ∷ bs) 1# * n | bs' 1# = (0b ∷ bs') 1#
(1b ∷ bs) 1# * n | bs' 1# = n + (0b ∷ bs') 1#
(⊥b ∷ _)  1# * _ | _

-- Successor.

suc : Bin → Bin
suc n = [] 1# + n

-- Division by 2, rounded upwards.

⌈_/2⌉ : Bin → Bin
⌈ n /2⌉ = ⌊ suc n /2⌋

-- Predecessor.

pred : Bin⁺ → Bin
pred []        = 0#
pred (0b ∷ bs) = pred bs *2+1
pred (1b ∷ bs) = (zero ∷ bs) 1#
pred (⊥b ∷ bs)

-- downFrom n enumerates all numbers from n - 1 to 0. This function is
-- linear in n. Analysis: fromℕ takes linear time, and the preds used
-- take amortised constant time (to see this, let the cost of a pred
-- be 2, and put 1 debit on every bit which is 1).

downFrom : ℕ → List Bin
downFrom n = helper n (fromℕ n)
  where
  helper : ℕ → Bin → List Bin
  helper zero   0#      = []
  helper (1+ n) (bs 1#) = n′ ∷ helper n n′
    where n′ = pred bs
  -- Impossible cases:
  helper zero   (_ 1#)  = []
  helper (1+ _) 0#      = []

------------------------------------------------------------------------
-- Tests

-- The tests below are run when this module is type checked.

-- First some test helpers:

private

  testLimit : ℕ
  testLimit = 5

  nats : List ℕ
  nats = List.downFrom testLimit

  nats⁺ : List ℕ
  nats⁺ = filter (1 Nat.≤?_) nats

  natPairs : List (ℕ × ℕ)
  natPairs = List.zip nats (reverse nats)

  _=[_]_ : (ℕ → ℕ) → List ℕ → (Bin → Bin) → Set
  f =[ ns ] g = List.map f ns ≡ List.map (toℕ ∘ g ∘ fromℕ) ns

  _=[_]₂_ : (ℕ → ℕ → ℕ) → List (ℕ × ℕ) → (Bin → Bin → Bin) → Set
  f =[ ps ]₂ g =
    List.map (uncurry f) ps ≡ List.map (toℕ ∘ uncurry (g on fromℕ)) ps

-- And then the tests:

private

  test-*2+1 : (λ n → Nat._+_ (Nat._*_ n 2) 1) =[ nats ] _*2+1
  test-*2+1 = refl

  test-*2 : (λ n → Nat._*_ n 2) =[ nats ] _*2
  test-*2 = refl

  test-⌊_/2⌋ : Nat.⌊_/2⌋ =[ nats ] ⌊_/2⌋
  test-⌊_/2⌋ = refl

  test-+ : Nat._+_ =[ natPairs ]₂ _+_
  test-+ = refl

  test-* : Nat._*_ =[ natPairs ]₂ _*_
  test-* = refl

  test-suc : 1+_ =[ nats ] suc
  test-suc = refl

  test-⌈_/2⌉ : Nat.⌈_/2⌉ =[ nats ] ⌈_/2⌉
  test-⌈_/2⌉ = refl

  drop-1# : Bin → Bin⁺
  drop-1# 0#      = []
  drop-1# (bs 1#) = bs

  test-pred : Nat.pred =[ nats⁺ ] (pred ∘ drop-1#)
  test-pred = refl

  test-downFrom : List.map toℕ (downFrom testLimit) ≡
                  List.downFrom testLimit
  test-downFrom = refl


text:
------------------------------------------------------------------------
-- A compiler
------------------------------------------------------------------------

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

module Lambda.Simplified.Compiler where

open import Equality.Propositional.Cubical
open import Prelude

open import Vec.Function equality-with-J

open import Lambda.Simplified.Syntax
open import Lambda.Simplified.Virtual-machine

private
  module C = Closure Code
  module T = Closure Tm

-- The compiler (which takes a code continuation).

comp : ∀ {n} → Tm n → Code n → Code n
comp (var x)   c = var x ∷ c
comp (ƛ t)     c = clo (comp t (ret ∷ [])) ∷ c
comp (t₁ · t₂) c = comp t₁ (comp t₂ (app ∷ c))

-- Environments and values can also be compiled.

mutual

  comp-env : ∀ {n} → T.Env n → C.Env n
  comp-env ρ n = comp-val (ρ n)

  comp-val : T.Value → C.Value
  comp-val (T.ƛ t ρ) = C.ƛ (comp t (ret ∷ [])) (comp-env ρ)

-- Compilation takes empty environments to empty environments.

comp-nil : comp-env nil ≡ nil
comp-nil = empty≡nil ext

-- Compilation commutes with cons.

comp-cons : ∀ {n} {ρ : T.Env n} {v} →
            comp-env (cons v ρ) ≡ cons (comp-val v) (comp-env ρ)
comp-cons = non-empty≡cons-head-tail ext _

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


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

open import LogicalFormulae
open import Groups.Groups
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Numbers.Naturals.Definition
open import Numbers.Naturals.Order
open import Setoids.Orders
open import Setoids.Setoids
open import Functions
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Rings.Homomorphisms.Definition
open import Groups.Homomorphisms.Lemmas
open import Rings.IntegralDomains.Definition
open import Rings.IntegralDomains.Examples
open import Rings.EuclideanDomains.Definition
open import Fields.Fields
open import WellFoundedInduction

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

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

open import Rings.PrincipalIdealDomains.Definition (EuclideanDomain.isIntegralDomain E)
open import Rings.Ideals.Principal.Definition R
open import Rings.Divisible.Definition R
open Setoid S
open Ring R
open Equivalence eq

euclideanDomainIsPid : {c : _} → PrincipalIdealDomain {c}
euclideanDomainIsPid {pred = pred} ideal = {!!}
-- We definitely need to be able to decide equality in order to deduce this; otherwise we can't tell the difference
-- between "everything is 0" and "something is nonzero", and the proofs are genuinely different in the two cases.
  where
    r : A
    r = {!!}
    r!=0 : (r ∼ 0R) → False
    r!=0 = {!!}
    predR : pred r
    predR = {!!}
    sr : (s : A) → r ∣ s
    sr = EuclideanDomain.divisionAlg r!=0 s!=0 ?


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

module StructurallySmaller where

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero   + n = n
succ m + n = succ (m + n)

-- Foo is not structurally recursive even though zero + n normalises
-- to n.
{-# TERMINATING #-}
foo : ℕ → ℕ
foo zero     = zero
foo (succ n) = foo (zero + n)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{- In some cases you may want to block certain terms from being
  evaluated by Agda at compile time.  I found I needed to do this
  when generating large terms intended for evaluation at run-time only.
  You can use the runtime-only function for this.  If its first
  argument is tt, then we will use a postulate runtime-identity
  to block Agda's compile-time evaluation.  Otherwise, we will
  not block compile-time evaluation. -}
module runtime-only where

open import bool

postulate
  runtime-identity : ∀{A : Set} → A → A

{-# COMPILED runtime-identity (\ _ x -> x )   #-}

runtime-only : ∀{A : Set} → 𝔹 → A → A
runtime-only ff = λ x → x
runtime-only tt = runtime-identity

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Example showing how to define an indexed container
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe --guardedness #-}

module README.Data.Container.Indexed where

open import Data.Unit
open import Data.Empty
open import Data.Nat.Base
open import Data.Product
open import Function
open import Data.W.Indexed
open import Data.Container.Indexed
open import Data.Container.Indexed.WithK

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

------------------------------------------------------------------------
-- Vector as an indexed container

-- An indexed container is defined by three things:
-- 1. Commands the user can emit
-- 2. Responses the indexed container returns to these commands
-- 3. Update of the index based on the command and the response issued.

-- For a vector, commands are constructors, responses are the number of subvectors
-- (0 if the vector is empty, 1 otherwise) and the update corresponds to setting the
-- size of the tail (if it exists). We can formalize these ideas like so:

-- Depending on the size of the vector, we may have reached the end already (nil)
-- or we may specify what the head should be (cons). This is the type of commands.

  data VecC : ℕ → Set a where
    nil  :           VecC zero
    cons : ∀ n → A → VecC (suc n)

  Vec : Container ℕ ℕ a _
  Command Vec = VecC

-- We then treat each command independently, specifying both the response and the
-- next index based on that response.

-- In the nil case, the response is the empty type: there won't be any tail. As
-- a consequence, the next index won't be needed (and we can rely on the fact the
-- user will never be able to call it).

  Response Vec nil = ⊥
  next     Vec nil = λ ()

-- In the cons case, the response is the unit type: there is exactly one tail. The
-- next index is the predecessor of the current one. It is handily handed over to
-- use by `cons`.

  -- cons
  Response Vec (cons n a) = ⊤
  next     Vec (cons n a) = λ _ → n

-- Finally we can define the type of Vector as the least fixed point of Vec.

  Vector : ℕ → Set a
  Vector = μ Vec

module _ {a} {A : Set a} where

-- We can recover the usual constructors by using `sup` to enter the fixpoint
-- and then using the appropriate pairing of a command & a handler for the
-- response.

-- For [], the response is ⊥ which makes it easy to conclude.

  [] : Vector A 0
  [] = sup (nil , λ ())

-- For _∷_, the response is ⊤ so we need to pass a tail. We give the one we took
-- as an argument.

  infixr 3 _∷_
  _∷_ : ∀ {n} → A → Vector A n → Vector A (suc n)
  x ∷ xs = sup (cons _ x , λ _ → xs)

-- We can now use these constructors to build up vectors:

1⋯3 : Vector ℕ 3
1⋯3 = 1 ∷ 2 ∷ 3 ∷ []

-- Horrible thing to check the definition of _∈_ is not buggy.
-- Not sure whether we can say anything interesting about it in the case of Vector...

open import Relation.Binary.HeterogeneousEquality

_ : _∈_ {C = Vec ℕ} {X = Vector ℕ} 1⋯3 (⟦ Vec ℕ ⟧ (Vector ℕ) 4 ∋ cons _ 0 , λ _ → 1⋯3)
_ = _ , refl


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

module Level where

open import Agda.Primitive
  using (Level)
  renaming ( _⊔_ to _ℓ⊔_
           ; lzero to ℓzero
           ; lsuc  to ℓsuc )
  public

Type : (ℓ : Level) → Set (ℓsuc ℓ)
Type ℓ = Set ℓ

Type₀ = Type ℓzero
Type₁ = Type (ℓsuc ℓzero)
Type₂ = Type (ℓsuc (ℓsuc ℓzero))
Type₃ = Type (ℓsuc (ℓsuc (ℓsuc ℓzero)))

variable
  a b c : Level
  A : Type a
  B : Type b
  C : Type c

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.DirProd where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Semigroup

open GroupStr
open IsGroup hiding (rid ; lid ; invr ; invl)
open IsMonoid hiding (rid ; lid)
open IsSemigroup

DirProd : ∀ {ℓ ℓ'} → Group ℓ → Group ℓ' → Group (ℓ-max ℓ ℓ')
fst (DirProd G H) = fst G × fst H
1g (snd (DirProd G H)) = (1g (snd G)) , (1g (snd H))
_·_ (snd (DirProd G H)) x y = _·_ (snd G) (fst x) (fst y)
                            , _·_ (snd H) (snd x) (snd y)
(inv (snd (DirProd G H))) x = (inv (snd G) (fst x)) , (inv (snd H) (snd x))
is-set (isSemigroup (isMonoid (isGroup (snd (DirProd G H))))) =
  isSet× (is-set (snd G)) (is-set (snd H))
assoc (isSemigroup (isMonoid (isGroup (snd (DirProd G H))))) x y z i =
  assoc (snd G) (fst x) (fst y) (fst z) i , assoc (snd H) (snd x) (snd y) (snd z) i
fst (identity (isMonoid (isGroup (snd (DirProd G H)))) x) i =
  rid (snd G) (fst x) i , rid (snd H) (snd x) i
snd (identity (isMonoid (isGroup (snd (DirProd G H)))) x) i =
  lid (snd G) (fst x) i , lid (snd H) (snd x) i
fst (inverse (isGroup (snd (DirProd G H))) x) i =
  (invr (snd G) (fst x) i) , invr (snd H) (snd x) i
snd (inverse (isGroup (snd (DirProd G H))) x) i =
  (invl (snd G) (fst x) i) , invl (snd H) (snd x) i


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Bisimilarity for Conats
------------------------------------------------------------------------

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

module Codata.Conat.Bisimilarity where

open import Size
open import Codata.Thunk
open import Codata.Conat
open import Relation.Binary

infix 1 _⊢_≈_
data _⊢_≈_ i : (m n : Conat ∞) → Set where
  zero : i ⊢ zero ≈ zero
  suc  : ∀ {m n} → Thunk^R _⊢_≈_ i m n → i ⊢ suc m ≈ suc n

refl : ∀ {i m} → i ⊢ m ≈ m
refl {m = zero}  = zero
refl {m = suc m} = suc λ where .force → refl

sym : ∀ {i m n} → i ⊢ m ≈ n → i ⊢ n ≈ m
sym zero     = zero
sym (suc eq) = suc λ where .force → sym (eq .force)

trans : ∀ {i m n p} → i ⊢ m ≈ n → i ⊢ n ≈ p → i ⊢ m ≈ p
trans zero      zero      = zero
trans (suc eq₁) (suc eq₂) = suc λ where .force → trans (eq₁ .force) (eq₂ .force)

infix 1 _⊢_≲_
data _⊢_≲_ i : (m n : Conat ∞) → Set where
  z≲n : ∀ {n} → i ⊢ zero ≲ n
  s≲s : ∀ {m n} → Thunk^R _⊢_≲_ i m n → i ⊢ suc m ≲ suc n

≈⇒≲ : ∀ {i m n} → i ⊢ m ≈ n → i ⊢ m ≲ n
≈⇒≲ zero     = z≲n
≈⇒≲ (suc eq) = s≲s λ where .force → ≈⇒≲ (eq .force)

≲-refl : ∀ {i m} → i ⊢ m ≲ m
≲-refl = ≈⇒≲ refl

≲-antisym : ∀ {i m n} → i ⊢ m ≲ n → i ⊢ n ≲ m → i ⊢ m ≈ n
≲-antisym z≲n      z≲n      = zero
≲-antisym (s≲s le) (s≲s ge) = suc λ where .force → ≲-antisym (le .force) (ge .force)

≲-trans : ∀ {i m n p} → i ⊢ m ≲ n → i ⊢ n ≲ p → i ⊢ m ≲ p
≲-trans z≲n       _         = z≲n
≲-trans (s≲s le₁) (s≲s le₂) = s≲s λ where .force → ≲-trans (le₁ .force) (le₂ .force)


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

open import Base

module Homotopy.Pushout where

open import Homotopy.PushoutDef public

pushout-diag-flip : ∀ {i} → pushout-diag i → pushout-diag i
pushout-diag-flip (diag A , B , C , f , g) = diag B , A , C , g , f

pushout-flip : ∀ {i} {d : pushout-diag i} → pushout d → pushout (pushout-diag-flip d)
pushout-flip {d = d} = pushout-rec-nondep
  (pushout $ pushout-diag-flip d)
  right left (! ◯ glue)

pushout-flip-flip : ∀ {i} {d : pushout-diag i} (p : pushout d)
                    → pushout-flip (pushout-flip p) ≡ p
pushout-flip-flip {d = d} = pushout-rec
  (λ p → pushout-flip (pushout-flip p) ≡ p)
  (λ _ → refl)
  (λ _ → refl)
  (λ c →
    transport (λ p → pushout-flip (pushout-flip p) ≡ p) (glue c) refl
      ≡⟨ trans-app≡id (pushout-flip ◯ pushout-flip) (glue c) refl ⟩
    ! (ap (pushout-flip ◯ pushout-flip) (glue c)) ∘ glue c
      ≡⟨ ap (λ x → ! x ∘ glue c)
            $ ap-compose pushout-flip pushout-flip (glue c) ⟩
    ! (ap pushout-flip (ap pushout-flip (glue c))) ∘ glue c
      ≡⟨ ap (λ x → ! (ap pushout-flip x) ∘ glue c)
            $ pushout-β-glue-nondep (pushout $ pushout-diag-flip d) right left (! ◯ glue) c ⟩
    ! (ap pushout-flip (! (glue c))) ∘ glue c
      ≡⟨ ap (λ x → ! x ∘ glue c) $ ap-opposite pushout-flip (glue c) ⟩
    ! (! (ap pushout-flip (glue c))) ∘ glue c
      ≡⟨ ap (λ x → ! (! x) ∘ glue c)
            $ pushout-β-glue-nondep (pushout d) right left (! ◯ glue) c ⟩
    ! (! (! (glue c))) ∘ glue c
      ≡⟨ ap (λ x → ! x ∘ glue c) $ opposite-opposite $ glue c ⟩
    ! (glue c) ∘ glue c
      ≡⟨ opposite-left-inverse (glue c) ⟩∎
    refl
      ∎)

pushout-β-!glue-nondep : ∀ {i} {d : pushout-diag i} {l} (D : Set l) →
  let open pushout-diag d in
  (left* : A → D) (right* : B → D)
  (glue* : (c : C) → left* (f c) ≡ right* (g c)) (c : C)
  → ap (pushout-rec-nondep D left* right* glue*) (! (glue c)) ≡ ! (glue* c)
pushout-β-!glue-nondep D left* right* glue* c =
  ap (pushout-rec-nondep D left* right* glue*) (! (glue c))
    ≡⟨ ap-opposite (pushout-rec-nondep D left* right* glue*) $ glue c ⟩
  ! (ap (pushout-rec-nondep D left* right* glue*) $ glue c)
    ≡⟨ ap ! $ pushout-β-glue-nondep D left* right* glue* c ⟩∎
  ! (glue* c)
    ∎


text:
module Negative1 where

data D : Set where
    lam : (D -> D) -> D

max_forks_repo_name: Agda-zh/agda


text:
module FFI.Data.Text.Encoding where

open import Agda.Builtin.String using (String)

open import FFI.Data.ByteString using (ByteString)

{-# FOREIGN GHC import qualified Data.Text.Encoding #-}

postulate encodeUtf8 : String → ByteString
{-# COMPILE GHC encodeUtf8 = Data.Text.Encoding.encodeUtf8 #-}

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
{-| A custom prelude -}
module Eth.Prelude where

import Prelude
import Prelude.Bool -- using (bool)
import Prelude.List -- using (intercalate)
import Prelude.Monad -- using ((>=>))
import Control.Monad.Identity -- using
import Control.Monad.Writer -- using
--  (MonadWriter, WriterT, Writer, execWriterT, execWriter, tell)
import Control.Monad.Reader -- using
--  (MonadReader, ReaderT, Reader, runReaderT, runReader, ask, local)

infixl 6 <>

export
isNullStr : String -> Bool
isNullStr = (== neutral)

-- export
-- (<>) : Monoid m => m -> m -> m
-- (<>) = (<+>)

export
bool : a -> a -> Bool -> a
bool x y b = case b of
  True => x
  False => y

export
execWriterT : Functor m => WriterT w m a -> m w
execWriterT = map snd . runWriterT

-- works : WriterT w (ReaderT r Identity) _ -> ReaderT r Identity w
-- works = execWriterT @{ }

-- doesnt : WriterT w (Reader r) _ -> Reader r w
-- doesnt = execWriterT @{ FunctorReaderT }
  -- using ReaderTFunctor

export
execWriter : Writer w a -> w
execWriter = runIdentity . execWriterT

export
runReader : Reader r a -> r -> a
runReader m = runIdentity . runReaderT m

-- M : Type -> Type -> Type -> Type
-- M w r a = WriterT w (Reader r) a

-- unM : M w r a -> w -> r -> a
-- unM = ?foo

max_stars_repo_name: fredefox/ethambda-agda

max_issues_repo_name: fredefox/ethambda-agda

max_forks_repo_name: fredefox/ethambda-agda


text:
-- 2014-07-30 Andreas, issue reported by toporoskyy.y

data Nat : Set where
   Zero : Nat
   Succ : Nat -> Nat

boom : Nat -> Nat
boom n@(Succ _) = Zero

-- EXPECTED:
-- Not supported: @-patterns
-- when scope checking the left-hand side boom n@(Succ _) in the
-- definition of boom

max_forks_repo_name: cruhland/agda


text: A : Set