text:
module Yoneda where

open import Level
open import Data.Product
open import Relation.Binary
import Relation.Binary.SetoidReasoning as SetR
open Setoid renaming (_≈_ to eqSetoid)

open import Basic
open import Category
import Functor
import Nat

open Category.Category
open Functor.Functor
open Nat.Nat
open Nat.Export

yoneda : ∀{C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) → Functor.Functor C PSh[ C ]
yoneda C = record {
  fobj = λ x → Hom[ C ][-, x ] ;
  fmapsetoid = λ {A} {B} → record { mapping = λ f → HomNat[ C ][-, f ] ; preserveEq = λ {x} {y} x₁ x₂ → begin⟨ C ⟩
    Map.mapping (component HomNat[ C ][-, x ] _) x₂ ≈⟨ refl-hom C ⟩
    C [ x ∘ x₂ ] ≈⟨ ≈-composite C x₁ (refl-hom C) ⟩
    C [ y ∘ x₂ ] ≈⟨ refl-hom C ⟩
    Map.mapping (component HomNat[ C ][-, y ] _) x₂
  ∎ } ;
  preserveId = λ x → leftId C ;
  preserveComp = λ x → assoc C
  }

YonedaLemma : ∀{C₀ C₁ ℓ} {C : Category C₀ C₁ ℓ} {F : Obj PSh[ C ]} {X : Obj C} → Setoids [ Homsetoid [ op C , Setoids ] (fobj (yoneda C) X) F ≅ LiftSetoid {C₁} {suc (suc ℓ) ⊔ (suc (suc C₁) ⊔ suc C₀)} {ℓ} {C₀ ⊔ C₁ ⊔ ℓ} (fobj F X) ]
YonedaLemma {C₀} {C₁} {ℓ} {C} {F} {X} = record {
  map-→ = nat→obj ;
  map-← = obj→nat ;
  proof = obj→obj≈id , nat→nat≈id }
  where
    nat→obj : Map.Map (Homsetoid [ op C , Setoids ] (fobj (yoneda C) X) F) (LiftSetoid (fobj F X))
    nat→obj = record {
      mapping = λ α → lift (Map.mapping (component α X) (id C)) ;
      preserveEq = λ x≈y → lift (x≈y (id C)) }

    obj→nat : Map.Map (LiftSetoid (fobj F X)) (Homsetoid [ op C , Setoids ] (fobj (yoneda C) X) F)
    obj→nat = record {
      mapping = λ a → record {
        component = component-map a ;
        naturality = λ {c} {d} {f} x → SetR.begin⟨ fobj F d ⟩
          Map.mapping (Setoids [ component-map a d ∘ fmap (fobj (yoneda C) X) f ]) x SetR.≈⟨ refl (fobj F d) ⟩
          Map.mapping (Map.mapping (fmapsetoid F) (C [ x ∘ f ])) (lower a) SetR.≈⟨ (preserveComp F) (lower a) ⟩
          Map.mapping (Map.mapping (fmapsetoid F) f) (Map.mapping (Map.mapping (fmapsetoid F) x) (lower a)) SetR.≈⟨ refl (fobj F d) ⟩
          Map.mapping (Setoids [ fmap F f ∘ component-map a c ]) x
        SetR.∎} ;
      preserveEq = λ {x} {y} x≈y f → SetR.begin⟨ fobj F _ ⟩
        Map.mapping (component-map x _) f SetR.≈⟨ refl (fobj F _) ⟩
        Map.mapping (Map.mapping (fmapsetoid F) f) (lower x) SetR.≈⟨ Map.preserveEq (fmap F f) (lower x≈y) ⟩
        Map.mapping (Map.mapping (fmapsetoid F) f) (lower y) SetR.≈⟨ refl (fobj F _) ⟩
        Map.mapping (component-map y _) f
        SetR.∎}
      where
        component-map = λ a b → record {
          mapping = λ u → Map.mapping (fmap F u) (lower a) ;
          preserveEq = λ {x} {y} x≈y → SetR.begin⟨ fobj F b ⟩
            Map.mapping (fmap F x) (lower a) SetR.≈⟨ (Functor.preserveEq F x≈y) (lower a) ⟩
            Map.mapping (fmap F y) (lower a)
          SetR.∎
          }

    obj→obj≈id : Setoids [ Setoids [ nat→obj ∘ obj→nat ] ≈ id Setoids ]
    obj→obj≈id = λ x → lift (SetR.begin⟨ fobj F X ⟩
      lower (Map.mapping (Setoids [ nat→obj ∘ obj→nat ]) x) SetR.≈⟨ refl (fobj F X) ⟩
      Map.mapping (Map.mapping (fmapsetoid F) (id C)) (lower x) SetR.≈⟨ (preserveId F) (lower x) ⟩
      lower x SetR.≈⟨ refl (fobj F X) ⟩
      lower (Map.mapping {A = LiftSetoid {ℓ′ = ℓ} (fobj F X)} (id Setoids) x)
      SetR.∎)

    nat→nat≈id : Setoids [ Setoids [ obj→nat ∘ nat→obj ] ≈ id Setoids ]
    nat→nat≈id α f = SetR.begin⟨ fobj F _ ⟩
      Map.mapping (component (Map.mapping (Setoids [ obj→nat ∘ nat→obj ]) α) _) f SetR.≈⟨ refl (fobj F _) ⟩
      Map.mapping (Setoids [ fmap F f ∘ component α X ]) (id C) SetR.≈⟨ lemma (id C) ⟩
      Map.mapping (Setoids [ component α (dom C f) ∘ fmap (fobj (yoneda C) X) f ]) (id C) SetR.≈⟨ Map.preserveEq (component α (dom C f)) (leftId C) ⟩
      Map.mapping (component α (dom C f)) f SetR.≈⟨ refl (fobj F _) ⟩
      Map.mapping (component (Map.mapping (id Setoids {Homsetoid [ (op C) , Setoids ] _ _}) α) (dom C f)) f
      SetR.∎
      where
        lemma : Setoids [ Setoids [ fmap F f ∘ component α X ] ≈ Setoids [ component α (dom C f) ∘ fmap (fobj (yoneda C) X) f ] ]
        lemma = sym-hom Setoids {f = Setoids [ component α (dom C f) ∘ fmap (fobj (yoneda C) X) f ]} {g = Setoids [ fmap F f ∘ component α X ]} (naturality α)

max_stars_repo_name: myuon/agda-cate

max_issues_repo_name: myuon/agda-cate

max_forks_repo_name: myuon/agda-cate


text:
------------------------------------------------------------------------
-- "Equational" reasoning combinator setup
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Prelude

open import Labelled-transition-system

module Similarity.Weak.Equational-reasoning-instances
         {ℓ} {lts : LTS ℓ} where

open import Bisimilarity lts
open import Bisimilarity.Weak lts
import Bisimilarity.Weak.Equational-reasoning-instances
open import Equational-reasoning
open import Expansion lts
import Expansion.Equational-reasoning-instances
open import Similarity lts
open import Similarity.Weak lts

instance

  reflexive≼ : ∀ {i} → Reflexive [ i ]_≼_
  reflexive≼ = is-reflexive reflexive-≼

  reflexive≼′ : ∀ {i} → Reflexive [ i ]_≼′_
  reflexive≼′ = is-reflexive reflexive-≼′

  convert≼≼ : ∀ {i} → Convertible [ i ]_≼_ [ i ]_≼_
  convert≼≼ = is-convertible id

  convert≼′≼ : ∀ {i} → Convertible _≼′_ [ i ]_≼_
  convert≼′≼ = is-convertible λ p≼′q → force p≼′q

  convert≼≼′ : ∀ {i} → Convertible [ i ]_≼_ [ i ]_≼′_
  convert≼≼′ {i} = is-convertible lemma
    where
    lemma : ∀ {p q} → [ i ] p ≼ q → [ i ] p ≼′ q
    force (lemma p≼q) = p≼q

  convert≼′≼′ : ∀ {i} → Convertible [ i ]_≼′_ [ i ]_≼′_
  convert≼′≼′ = is-convertible id

  convert≤≼ : ∀ {i} → Convertible [ i ]_≤_ [ i ]_≼_
  convert≤≼ = is-convertible ≤⇒≼

  convert≤′≼ : ∀ {i} → Convertible _≤′_ [ i ]_≼_
  convert≤′≼ = is-convertible (convert ∘ ≤⇒≼′)

  convert≤≼′ : ∀ {i} → Convertible [ i ]_≤_ [ i ]_≼′_
  convert≤≼′ {i} = is-convertible lemma
    where
    lemma : ∀ {p q} → [ i ] p ≤ q → [ i ] p ≼′ q
    force (lemma p≤q) = convert p≤q

  convert≤′≼′ : ∀ {i} → Convertible [ i ]_≤′_ [ i ]_≼′_
  convert≤′≼′ = is-convertible ≤⇒≼′

  convert≈≼ : ∀ {i} → Convertible [ i ]_≈_ [ i ]_≼_
  convert≈≼ = is-convertible ≈⇒≼

  convert≈′≼ : ∀ {i} → Convertible _≈′_ [ i ]_≼_
  convert≈′≼ = is-convertible (convert ∘ ≈⇒≼′)

  convert≈≼′ : ∀ {i} → Convertible [ i ]_≈_ [ i ]_≼′_
  convert≈≼′ {i} = is-convertible lemma
    where
    lemma : ∀ {p q} → [ i ] p ≈ q → [ i ] p ≼′ q
    force (lemma p≈q) = convert p≈q

  convert≈′≼′ : ∀ {i} → Convertible [ i ]_≈′_ [ i ]_≼′_
  convert≈′≼′ = is-convertible ≈⇒≼′

  convert∼≼ : ∀ {i} → Convertible [ i ]_∼_ [ i ]_≼_
  convert∼≼ = is-convertible (≈⇒≼ ∘ convert {a = ℓ})

  convert∼′≼ : ∀ {i} → Convertible _∼′_ [ i ]_≼_
  convert∼′≼ = is-convertible (convert ∘ ≈⇒≼′ ∘ convert {a = ℓ})

  convert∼≼′ : ∀ {i} → Convertible [ i ]_∼_ [ i ]_≼′_
  convert∼≼′ {i} = is-convertible lemma
    where
    lemma : ∀ {p q} → [ i ] p ∼ q → [ i ] p ≼′ q
    force (lemma p∼q) = ≈⇒≼ (convert {a = ℓ} p∼q)

  convert∼′≼′ : ∀ {i} → Convertible [ i ]_∼′_ [ i ]_≼′_
  convert∼′≼′ = is-convertible (≈⇒≼′ ∘ convert {a = ℓ})

  trans≼≼ : ∀ {i} → Transitive′ [ i ]_≼_ _≼_
  trans≼≼ = is-transitive transitive-≼

  trans≼′≼ : Transitive′ _≼′_ _≼_
  trans≼′≼ = is-transitive transitive-≼′

  trans≼′≼′ : ∀ {i} → Transitive′ [ i ]_≼′_ _≼′_
  trans≼′≼′ = is-transitive (λ p≼q → transitive-≼′ p≼q ∘ convert)

  trans≼≼′ : ∀ {i} → Transitive′ [ i ]_≼_ _≼′_
  trans≼≼′ = is-transitive (λ p≼q → transitive-≼ p≼q ∘ convert)

  trans≳≼ : ∀ {i} → Transitive [ i ]_≳_ [ i ]_≼_
  trans≳≼ = is-transitive transitive-≳≼

  trans≳′≼ : ∀ {i} → Transitive _≳′_ [ i ]_≼_
  trans≳′≼ = is-transitive (transitive-≳≼ ∘ convert {a = ℓ})

  trans≳′≼′ : ∀ {i} → Transitive [ i ]_≳′_ [ i ]_≼′_
  trans≳′≼′ = is-transitive transitive-≳≼′

  trans≳≼′ : ∀ {i} → Transitive [ i ]_≳_ [ i ]_≼′_
  trans≳≼′ = is-transitive (transitive-≳≼′ ∘ convert {a = ℓ})

ext: agda

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


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

open import Numbers.Naturals.Semiring
open import Functions
open import LogicalFormulae
open import Groups.Definition
open import Rings.Definition
open import Rings.IntegralDomains.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Definition
open import Groups.Orders.Archimedean

module Fields.FieldOfFractions.Archimedean {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) {c : _} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) where

open import Groups.Cyclic.Definition
open import Fields.FieldOfFractions.Setoid I
open import Fields.FieldOfFractions.Group I
open import Fields.FieldOfFractions.Addition I
open import Fields.FieldOfFractions.Ring I
open import Fields.FieldOfFractions.Order I order
open import Fields.FieldOfFractions.Field I
open import Fields.Orders.Partial.Archimedean {F = fieldOfFractions} record { oRing = fieldOfFractionsPOrderedRing }
open import Rings.Orders.Partial.Lemmas pRing
open import Rings.Orders.Total.Lemmas

open Setoid S
open Equivalence eq
open Ring R
open Group additiveGroup
open TotallyOrderedRing order
open SetoidTotalOrder total

private

  denomPower : (n : ℕ) → fieldOfFractionsSet.denom (positiveEltPower fieldOfFractionsGroup record { num = 1R ; denom = 1R ; denomNonzero = IntegralDomain.nontrivial I } n) ∼ 1R
  denomPower zero = reflexive
  denomPower (succ n) = transitive identIsIdent (denomPower n)

  denomPlus : {a : A} .(a!=0 : a ∼ 0R → False) (n1 n2 : A) → Setoid._∼_ fieldOfFractionsSetoid (fieldOfFractionsPlus record { num = n1 ; denom = a ; denomNonzero = a!=0 } record { num = n2 ; denom = a ; denomNonzero = a!=0 }) (record { num = n1 + n2 ; denom = a ; denomNonzero = a!=0 })
  denomPlus {a} a!=0 n1 n2 = transitive *Commutative (transitive (*WellDefined reflexive (transitive (+WellDefined *Commutative reflexive) (symmetric *DistributesOver+))) *Associative)

  d : (a : fieldOfFractionsSet) → fieldOfFractionsSet.denom a ∼ 0R → False
  d record { num = num ; denom = denom ; denomNonzero = denomNonzero } bad = exFalso (denomNonzero bad)

  simpPower : (n : ℕ) → Setoid._∼_ fieldOfFractionsSetoid (positiveEltPower fieldOfFractionsGroup record { num = Ring.1R R ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I} n) record { num = positiveEltPower (Ring.additiveGroup R) (Ring.1R R) n ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I }
  simpPower zero = Equivalence.reflexive (Setoid.eq fieldOfFractionsSetoid) {Group.0G fieldOfFractionsGroup}
  simpPower (succ n) = Equivalence.transitive (Setoid.eq fieldOfFractionsSetoid) {record { denomNonzero = d (fieldOfFractionsPlus (record { num = 1R ; denom = 1R ; denomNonzero = λ t → IntegralDomain.nontrivial I t }) (positiveEltPower fieldOfFractionsGroup _ n)) }} {record { denomNonzero = λ t → IntegralDomain.nontrivial I (transitive (symmetric identIsIdent) t) }} {record { denomNonzero = IntegralDomain.nontrivial I }} (Group.+WellDefined fieldOfFractionsGroup {record { num = Ring.1R R ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I }} {positiveEltPower fieldOfFractionsGroup record { num = Ring.1R R ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I } n} {record { num = Ring.1R R ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I }} {record { num = positiveEltPower (Ring.additiveGroup R) (Ring.1R R) n ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I }} (Equivalence.reflexive (Setoid.eq fieldOfFractionsSetoid) {record { num = Ring.1R R ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I}}) (simpPower n)) (transitive (transitive (transitive *Commutative (transitive identIsIdent (+WellDefined identIsIdent identIsIdent))) (symmetric identIsIdent)) (*WellDefined (symmetric identIsIdent) reflexive))

  lemma : (n : ℕ) {num denom : A} .(d!=0 : denom ∼ 0G → False) → (num * denom) < positiveEltPower additiveGroup 1R n → fieldOfFractionsComparison (record { num = num ; denom = denom ; denomNonzero = d!=0}) record { num = positiveEltPower additiveGroup (Ring.1R R) n ; denom = 1R ; denomNonzero = IntegralDomain.nontrivial I }
  lemma n {num} {denom} d!=0 numdenom<n with totality 0G denom
  ... | inl (inl 0<denom) with totality 0G 1R
  ... | inl (inl 0<1) = {!!}
  ... | inl (inr x) = exFalso (1<0False order x)
  ... | inr x = exFalso (IntegralDomain.nontrivial I (symmetric x))
  lemma n {num} {denom} d!=0 numdenom<n | inl (inr denom<0) with totality 0G 1R
  ... | inl (inl 0<1) = {!!}
  ... | inl (inr 1<0) = exFalso (1<0False order 1<0)
  ... | inr 0=1 = exFalso (IntegralDomain.nontrivial I (symmetric 0=1))
  lemma n {num} {denom} d!=0 numdenom<n | inr 0=denom = exFalso (d!=0 (symmetric 0=denom))

fieldOfFractionsArchimedean : Archimedean (toGroup R pRing) → ArchimedeanField
fieldOfFractionsArchimedean arch (record { num = num ; denom = denom ; denomNonzero = denom!=0 }) 0<q with totality 0G denom ,, totality 0G 1R
... | inl (inl 0<denom) ,, inl (inl 0<1) rewrite refl { x = 0} = {!!}
... | inl (inl 0<denom) ,, inl (inr x) = exFalso {!!}
... | inl (inl 0<denom) ,, inr x = exFalso {!!}
... | inl (inr denom<0) ,, inl (inl 0<1) = 0 , {!!}
  where
    t : {!!}
    t = {!!}
... | inl (inr denom<0) ,, inl (inr x) = exFalso {!!}
... | inl (inr denom<0) ,, inr x = exFalso {!!}
... | inr x ,, snd = exFalso (denom!=0 (symmetric x))
--... | N , pr = N , SetoidPartialOrder.<WellDefined fieldOfFractionsOrder {record { denomNonzero = denom!=0 }} {record { denomNonzero = denom!=0 }} {record { denomNonzero = λ t → nonempty (symmetric t) }} {record { denomNonzero = d (positiveEltPower fieldOfFractionsGroup record { num = 1R ; denom = 1R ; denomNonzero = λ t → nonempty (symmetric t) } N) }} (Equivalence.reflexive (Setoid.eq fieldOfFractionsSetoid) { record { denomNonzero = denom!=0 } }) (Equivalence.symmetric (Setoid.eq fieldOfFractionsSetoid) {record { denomNonzero = λ t → d (positiveEltPower fieldOfFractionsGroup record { num = 1R ; denom = 1R ; denomNonzero = λ t → nonempty (symmetric t) } N) t }} {record { denomNonzero = λ t → nonempty (symmetric t) }} (simpPower N)) (lemma N denom!=0 pr)

fieldOfFractionsArchimedean' : Archimedean (toGroup R pRing) → Archimedean (toGroup fieldOfFractionsRing fieldOfFractionsPOrderedRing)
fieldOfFractionsArchimedean' arch = archFieldToGrp (reciprocalPositive fieldOfFractionsOrderedRing) (fieldOfFractionsArchimedean arch)


text:
------------------------------------------------------------------------
-- Vectors parameterised on types in Set₁
------------------------------------------------------------------------

-- I want universe polymorphism.

module Data.Vec1 where

infixr 5 _∷_

open import Data.Nat
open import Data.Vec using (Vec; []; _∷_)
open import Data.Fin

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

data Vec₁ (a : Set₁) : ℕ → Set₁ where
  []  : Vec₁ a zero
  _∷_ : ∀ {n} (x : a) (xs : Vec₁ a n) → Vec₁ a (suc n)

------------------------------------------------------------------------
-- Some operations

map : ∀ {a b n} → (a → b) → Vec₁ a n → Vec₁ b n
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

map₀₁ : ∀ {a b n} → (a → b) → Vec a n → Vec₁ b n
map₀₁ f []       = []
map₀₁ f (x ∷ xs) = f x ∷ map₀₁ f xs

map₁₀ : ∀ {a b n} → (a → b) → Vec₁ a n → Vec b n
map₁₀ f []       = []
map₁₀ f (x ∷ xs) = f x ∷ map₁₀ f xs

lookup : ∀ {a n} → Fin n → Vec₁ a n → a
lookup zero    (x ∷ xs) = x
lookup (suc i) (x ∷ xs) = lookup i xs

max_issues_repo_name: larrytheliquid/Lemmachine


text:
open import Common.Prelude
open import Common.Reflection
open import Common.Equality

postulate
  trustme : ∀ {a} {A : Set a} {x y : A} → x ≡ y

magic : List (Arg Type) → Term → Tactic
magic _ _ = give (def (quote trustme) [])

id : ∀ {a} {A : Set a} → A → A
id x = x

science : List (Arg Type) → Term → Tactic
science _ _ = give (def (quote id) [])

by-magic : ∀ n → n + 4 ≡ 3
by-magic n = tactic magic

by-science : ∀ n → 0 + n ≡ n
by-science n = tactic science | refl

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
module Issue274 where

-- data ⊥ : Set where

record U : Set where
  constructor roll
  field ap : U → U

-- lemma : U → ⊥
-- lemma (roll u) = lemma (u (roll u))

-- bottom : ⊥
-- bottom = lemma (roll λ x → x)

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import HoTT

module cohomology.Choice where

unchoose : ∀ {i j} {n : ℕ₋₂} {A : Type i} {B : A → Type j}
  → Trunc n (Π A B) → Π A (Trunc n ∘ B)
unchoose = Trunc-rec (Π-level (λ _ → Trunc-level)) (λ f → [_] ∘ f)

has-choice : ∀ {i j} (n : ℕ₋₂) (A : Type i) (B : A → Type j) → Type (lmax i j)
has-choice {i} {j} n A B = is-equiv (unchoose {n = n} {A} {B})

{- Binary Choice -}
module _ {k} where

  pick-Bool : ∀ {j} {C : Lift {j = k} Bool → Type j}
    → (C (lift true)) → (C (lift false)) → Π (Lift Bool) C
  pick-Bool x y (lift true) = x
  pick-Bool x y (lift false) = y

  pick-Bool-η : ∀ {j} {C : Lift Bool → Type j} (f : Π (Lift Bool) C)
    → pick-Bool (f (lift true)) (f (lift false)) == f
  pick-Bool-η {C = C} f = λ= lemma
    where
    lemma : (b : Lift Bool) →
      pick-Bool {C = C} (f (lift true)) (f (lift false)) b == f b
    lemma (lift true) = idp
    lemma (lift false) = idp

  module _ {i} {n : ℕ₋₂} {A : Lift {j = k} Bool → Type i} where
    choose-Bool : Π (Lift Bool) (Trunc n ∘ A) → Trunc n (Π (Lift Bool) A)
    choose-Bool f = Trunc-rec Trunc-level
      (λ ft → Trunc-rec Trunc-level
        (λ ff → [ pick-Bool ft ff ] )
        (f (lift false)))
      (f (lift true))

    choose-Bool-squash : (f : Π (Lift Bool) A)
      → choose-Bool (λ b → [ f b ]) == [ f ]
    choose-Bool-squash f = ap [_] (pick-Bool-η f)

    private
      unc-c : ∀ f → unchoose (choose-Bool f) == f
      unc-c f = transport
        (λ h → unchoose (choose-Bool h) == h)
        (pick-Bool-η f)
        (Trunc-elim
           {P = λ tft →
             unchoose (choose-Bool (pick-Bool tft (f (lift false))))
             == pick-Bool tft (f (lift false))}
           (λ _ → =-preserves-level _ (Π-level (λ _ → Trunc-level)))
           (λ ft → Trunc-elim
             {P = λ tff →
               unchoose (choose-Bool (pick-Bool [ ft ] tff ))
               == pick-Bool [ ft ] tff}
             (λ _ → =-preserves-level _ (Π-level (λ _ → Trunc-level)))
             (λ ff → ! (pick-Bool-η _))
             (f (lift false)))
           (f (lift true)))

      c-unc : ∀ tg → choose-Bool (unchoose tg) == tg
      c-unc = Trunc-elim
        {P = λ tg → choose-Bool (unchoose tg) == tg}
        (λ _ → =-preserves-level _ Trunc-level)
        (λ g → ap [_] (pick-Bool-η g))

    Bool-has-choice : has-choice n (Lift Bool) A
    Bool-has-choice = is-eq unchoose choose-Bool unc-c c-unc

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

module Data.Tuple where

open import Data.Tuple.Base public
import Data.Product as P

Pair→× : ∀ {a b A B} → Pair {a} {b} A B → A P.× B
Pair→× (fst , snd) = fst P., snd

×→Pair : ∀ {a b A B} → P._×_ {a} {b} A B → Pair A B
×→Pair (fst P., snd) = fst , snd

max_stars_repo_name: semenov-vladyslav/bytes-agda

max_issues_repo_name: semenov-vladyslav/bytes-agda

max_forks_repo_name: semenov-vladyslav/bytes-agda


text:
module Type.NbE where

open import Context
open import Type.Core

open import Function
open import Data.Empty
open import Data.Sum.Base

infix  3 _⊢ᵗⁿᵉ_ _⊢ᵗⁿᶠ_ _⊨ᵗ_
infixl 9 _[_]ᵗ

mutual
  Starⁿᵉ : Conᵏ -> Set
  Starⁿᵉ Θ = Θ ⊢ᵗⁿᵉ ⋆

  Starⁿᶠ : Conᵏ -> Set
  Starⁿᶠ Θ = Θ ⊢ᵗⁿᶠ ⋆

  data _⊢ᵗⁿᵉ_ Θ : Kind -> Set where
    Varⁿᵉ : ∀ {σ} -> σ ∈ Θ -> Θ ⊢ᵗⁿᵉ σ
    _∙ⁿᵉ_ : ∀ {σ τ} -> Θ ⊢ᵗⁿᵉ σ ⇒ᵏ τ -> Θ ⊢ᵗⁿᶠ σ -> Θ ⊢ᵗⁿᵉ τ
    _⇒ⁿᵉ_ : Starⁿᵉ Θ -> Starⁿᵉ Θ -> Starⁿᵉ Θ
    πⁿᵉ   : ∀ σ -> Starⁿᵉ (Θ ▻ σ) -> Starⁿᵉ Θ
    μⁿᵉ   : ∀ {κ} -> Θ ⊢ᵗⁿᶠ (κ ⇒ᵏ ⋆) ⇒ᵏ κ ⇒ᵏ ⋆ -> Θ ⊢ᵗⁿᶠ κ -> Starⁿᵉ Θ

  data _⊢ᵗⁿᶠ_ Θ : Kind -> Set where
    Neⁿᶠ   : ∀ {σ} -> Θ ⊢ᵗⁿᵉ σ -> Θ ⊢ᵗⁿᶠ σ
    Lamⁿᶠ_ : ∀ {σ τ} -> Θ ▻ σ ⊢ᵗⁿᶠ τ -> Θ ⊢ᵗⁿᶠ σ ⇒ᵏ τ

mutual
  embᵗⁿᵉ : ∀ {Θ σ} -> Θ ⊢ᵗⁿᵉ σ -> Θ ⊢ᵗ σ
  embᵗⁿᵉ (Varⁿᵉ v) = Var v
  embᵗⁿᵉ (φ ∙ⁿᵉ α) = embᵗⁿᵉ φ ∙ embᵗⁿᶠ α
  embᵗⁿᵉ (α ⇒ⁿᵉ β) = embᵗⁿᵉ α ⇒ embᵗⁿᵉ β
  embᵗⁿᵉ (πⁿᵉ σ α) = π σ (embᵗⁿᵉ α)
  embᵗⁿᵉ (μⁿᵉ ψ α) = μ (embᵗⁿᶠ ψ) (embᵗⁿᶠ α)

  embᵗⁿᶠ : ∀ {Θ σ} -> Θ ⊢ᵗⁿᶠ σ -> Θ ⊢ᵗ σ
  embᵗⁿᶠ (Neⁿᶠ α)  = embᵗⁿᵉ α
  embᵗⁿᶠ (Lamⁿᶠ β) = Lam (embᵗⁿᶠ β)

mutual
  renᵗⁿᵉ : ∀ {Θ Ξ σ} -> Θ ⊆ Ξ -> Θ ⊢ᵗⁿᵉ σ -> Ξ ⊢ᵗⁿᵉ σ
  renᵗⁿᵉ ι (Varⁿᵉ v) = Varⁿᵉ (renᵛ ι v)
  renᵗⁿᵉ ι (φ ∙ⁿᵉ α) = renᵗⁿᵉ ι φ ∙ⁿᵉ renᵗⁿᶠ ι α
  renᵗⁿᵉ ι (α ⇒ⁿᵉ β) = renᵗⁿᵉ ι α ⇒ⁿᵉ renᵗⁿᵉ ι β
  renᵗⁿᵉ ι (πⁿᵉ σ α) = πⁿᵉ σ (renᵗⁿᵉ (keep ι) α)
  renᵗⁿᵉ ι (μⁿᵉ ψ α) = μⁿᵉ (renᵗⁿᶠ ι ψ) (renᵗⁿᶠ ι α)

  renᵗⁿᶠ : ∀ {Θ Ξ σ} -> Θ ⊆ Ξ -> Θ ⊢ᵗⁿᶠ σ -> Ξ ⊢ᵗⁿᶠ σ
  renᵗⁿᶠ ι (Neⁿᶠ α)  = Neⁿᶠ (renᵗⁿᵉ ι α)
  renᵗⁿᶠ ι (Lamⁿᶠ β) = Lamⁿᶠ (renᵗⁿᶠ (keep ι) β)

mutual
  _⊨ᵗ_ : Conᵏ -> Kind -> Set
  Θ ⊨ᵗ σ = Θ ⊢ᵗⁿᵉ σ ⊎ Kripke Θ σ

  Kripke : Conᵏ -> Kind -> Set
  Kripke Θ  ⋆       = ⊥
  Kripke Θ (σ ⇒ᵏ τ) = ∀ {Ξ} -> Θ ⊆ Ξ -> Ξ ⊨ᵗ σ -> Ξ ⊨ᵗ τ

Neˢ : ∀ {σ Θ} -> Θ ⊢ᵗⁿᵉ σ -> Θ ⊨ᵗ σ
Neˢ = inj₁

Varˢ : ∀ {σ Θ} -> σ ∈ Θ -> Θ ⊨ᵗ σ
Varˢ = Neˢ ∘ Varⁿᵉ

renᵗˢ : ∀ {σ Θ Δ} -> Θ ⊆ Δ -> Θ ⊨ᵗ σ -> Δ ⊨ᵗ σ
renᵗˢ          ι (inj₁ α)  = inj₁ (renᵗⁿᵉ ι α)
renᵗˢ {⋆}      ι (inj₂ ())
renᵗˢ {σ ⇒ᵏ τ} ι (inj₂ k)  = inj₂ λ κ -> k (κ ∘ ι)

readbackᵗ : ∀ {σ Θ} -> Θ ⊨ᵗ σ -> Θ ⊢ᵗⁿᶠ σ
readbackᵗ          (inj₁ α)  = Neⁿᶠ α
readbackᵗ {⋆}      (inj₂ ())
readbackᵗ {σ ⇒ᵏ τ} (inj₂ k)  = Lamⁿᶠ (readbackᵗ (k topᵒ (Varˢ vz)))

_∙ˢ_ : ∀ {Θ σ τ} -> Θ ⊨ᵗ σ ⇒ᵏ τ -> Θ ⊨ᵗ σ -> Θ ⊨ᵗ τ
inj₁ f ∙ˢ x = Neˢ (f ∙ⁿᵉ readbackᵗ x)
inj₂ k ∙ˢ x = k idᵒ x

groundⁿᵉ : ∀ {Θ} -> Θ ⊨ᵗ ⋆ -> Θ ⊢ᵗⁿᵉ ⋆
groundⁿᵉ (inj₁ α)  = α
groundⁿᵉ (inj₂ ())

environmentᵗˢ : Environment _⊨ᵗ_
environmentᵗˢ = record
  { varᵈ = Varˢ
  ; renᵈ = renᵗˢ
  }

module _ where
  open Environment environmentᵗˢ

  mutual
    evalᵗ : ∀ {Θ Ξ σ} -> Ξ ⊢ᵉ Θ -> Θ ⊢ᵗ σ -> Ξ ⊨ᵗ σ
    evalᵗ ρ (Var v) = lookupᵉ v ρ
    evalᵗ ρ (Lam β) = inj₂ λ ι α -> evalᵗ (renᵉ ι ρ ▷ α) β
    evalᵗ ρ (φ ∙ α) = evalᵗ ρ φ ∙ˢ evalᵗ ρ α
    evalᵗ ρ (α ⇒ β) = inj₁ $ groundⁿᵉ (evalᵗ ρ α) ⇒ⁿᵉ groundⁿᵉ (evalᵗ ρ β)
    evalᵗ ρ (π σ α) = inj₁ $ πⁿᵉ σ ∘ groundⁿᵉ $ evalᵗ (keepᵉ ρ) α
    evalᵗ ρ (μ ψ α) = inj₁ $ μⁿᵉ (nfᵗ ρ ψ) (nfᵗ ρ α)

    nfᵗ : ∀ {Θ Ξ σ} -> Ξ ⊢ᵉ Θ -> Θ ⊢ᵗ σ -> Ξ ⊢ᵗⁿᶠ σ
    nfᵗ ρ = readbackᵗ ∘ evalᵗ ρ

  normalize : ∀ {Θ σ} -> Θ ⊢ᵗ σ -> Θ ⊢ᵗ σ
  normalize = embᵗⁿᶠ ∘ nfᵗ idᵉ

_[_]ᵗ : ∀ {Θ σ τ} -> Θ ▻ σ ⊢ᵗ τ -> Θ ⊢ᵗ σ -> Θ ⊢ᵗ τ
β [ α ]ᵗ = normalize $ Lam β ∙ α
{-# DISPLAY normalize (Lam β ∙ α) = β [ α ]ᵗ #-}

max_stars_repo_name: AriFordsham/plutus

max_issues_repo_name: AriFordsham/plutus

max_forks_repo_name: AriFordsham/plutus


text:
postulate
  _→_ : Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe --no-termination-check #-}

module Issue2442-conflicting where


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

open import lib.Basics
open import lib.NType2
open import lib.Function2
open import lib.types.Group
open import lib.types.Sigma
open import lib.types.Truncation
open import lib.groups.Homomorphism
open import lib.groups.Isomorphism
open import lib.groups.SubgroupProp

module lib.groups.Subgroup where

module _ {i j} {G : Group i} (P : SubgroupProp G j) where
  private
    module G = Group G
    module P = SubgroupProp P

  subgroup-struct : GroupStructure P.SubEl
  subgroup-struct = record {M} where
    module M where
      ident : P.SubEl
      ident = G.ident , P.ident

      inv : P.SubEl → P.SubEl
      inv (g , p) = G.inv g , P.inv p

      comp : P.SubEl → P.SubEl → P.SubEl
      comp (g₁ , p₁) (g₂ , p₂) = G.comp g₁ g₂ , P.comp p₁ p₂

      abstract
        unit-l : ∀ g → comp ident g == g
        unit-l (g , _) = Subtype=-out P.subEl-prop (G.unit-l g)

        assoc : ∀ g₁ g₂ g₃ → comp (comp g₁ g₂) g₃ == comp g₁ (comp g₂ g₃)
        assoc (g₁ , _) (g₂ , _) (g₃ , _) = Subtype=-out P.subEl-prop (G.assoc g₁ g₂ g₃)

        inv-l : ∀ g → comp (inv g) g == ident
        inv-l (g , _) = Subtype=-out P.subEl-prop (G.inv-l g)

  Subgroup : Group (lmax i j)
  Subgroup = group _ SubEl-level subgroup-struct
    where abstract SubEl-level = Subtype-level P.subEl-prop G.El-level

module Subgroup {i j} {G : Group i} (P : SubgroupProp G j) where
  private
    module P = SubgroupProp P
    module G = Group G

  grp = Subgroup P
  open Group grp public

  El=-out : ∀ {s₁ s₂ : El} → fst s₁ == fst s₂ → s₁ == s₂
  El=-out = Subtype=-out P.subEl-prop

  inject : Subgroup P →ᴳ G
  inject = record {f = fst; pres-comp = λ _ _ → idp}

  inject-lift : ∀ {j} {H : Group j} (φ : H →ᴳ G)
    → Π (Group.El H) (P.prop ∘ GroupHom.f φ)
    → (H →ᴳ Subgroup P)
  inject-lift {H = H} φ P-all = record {M} where
    module H = Group H
    module φ = GroupHom φ
    module M where
      f : H.El → P.SubEl
      f h = φ.f h , P-all h

      abstract
        pres-comp : ∀ h₁ h₂ → f (H.comp h₁ h₂) == Group.comp (Subgroup P) (f h₁) (f h₂)
        pres-comp h₁ h₂ = Subtype=-out P.subEl-prop (φ.pres-comp h₁ h₂)

full-subgroup : ∀ {i j} {G : Group i} {P : SubgroupProp G j}
  → is-fullᴳ P → Subgroup P ≃ᴳ G
full-subgroup {G = G} {P} full = Subgroup.inject P , is-eq _ from to-from from-to where
  from : Group.El G → Subgroup.El P
  from g = g , full g

  abstract
    from-to : ∀ p → from (fst p) == p
    from-to p = Subtype=-out (SubgroupProp.subEl-prop P) idp

    to-from : ∀ g → fst (from g) == g
    to-from g = idp

module _ {i} {j} {G : Group i} {H : Group j} (φ : G →ᴳ H) where

  private
    module G = Group G
    module H = Group H
    module φ = GroupHom φ

  module Ker = Subgroup (ker-propᴳ φ)
  Ker = Ker.grp

  module Im = Subgroup (im-propᴳ φ)
  Im = Im.grp

  im-lift : G →ᴳ Im
  im-lift = Im.inject-lift φ (λ g → [ g , idp ])

  im-lift-is-surj : is-surjᴳ im-lift
  im-lift-is-surj (_ , s) = Trunc-fmap
    (λ {(g , p) → (g , Subtype=-out (_ , λ _ → Trunc-level) p)}) s

module _ {i j k} {G : Group i} (P : SubgroupProp G j)
  (Q : SubgroupProp G k) where

  -- FIXME looks like a bad name
  Subgroup-fmap-r : P ⊆ᴳ Q → Subgroup P →ᴳ Subgroup Q
  Subgroup-fmap-r P⊆Q = group-hom (Σ-fmap-r P⊆Q)
    (λ _ _ → Subtype=-out (SubgroupProp.subEl-prop Q) idp)

  Subgroup-emap-r : P ⊆ᴳ Q → Q ⊆ᴳ P → Subgroup P ≃ᴳ Subgroup Q
  Subgroup-emap-r P⊆Q Q⊆P = Subgroup-fmap-r P⊆Q ,
    is-eq _ (Σ-fmap-r Q⊆P)
      (λ _ → Subtype=-out (SubgroupProp.subEl-prop Q) idp)
      (λ _ → Subtype=-out (SubgroupProp.subEl-prop P) idp)

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module Lemmachine.Resource.Configure where
open import Lemmachine.Request
open import Lemmachine.Response
open import Lemmachine.Resource
open import Lemmachine.Resource.Universe
open import Data.Bool
open import Data.Maybe
open import Data.Product
open import Data.List
open import Data.Function using (const)

private

 update : (code : Code) → El code → Resource → Resource

 update resourceExists f c = record {
     resourceExists = f
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update serviceAvailable f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = f
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update isAuthorized f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = f
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update forbidden f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = f
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update allowMissingPost f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = f
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update malformedRequest f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = f
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update uriTooLong f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = f
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update knownContentType f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = f
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update validContentHeaders f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = f
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update validEntityLength f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = f
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update options f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = f
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update allowedMethods f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = f
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update knownMethods f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = f
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update deleteResource f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = f
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update deleteCompleted f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = f
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update postIsCreate f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = f
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update createPath f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = f
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update processPost f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = f
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update contentTypesProvided f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = f
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update languageAvailable f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = f
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update contentTypesAccepted f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = f
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update charsetsProvided f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = f
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update encodingsProvided f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = f
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update variances f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = f
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update isConflict f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = f
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update multipleChoices f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = f
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update previouslyExisted f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = f
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update movedPermanently f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = f
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update movedTemporarily f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = f
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update lastModified f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = f
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update expires f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = f
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update generateETag f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = f
   ; finishRequest = Resource.finishRequest c
   ; body = Resource.body c
   }

 update finishRequest f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = f
   ; body = Resource.body c
   }

 update body f c = record {
     resourceExists = Resource.resourceExists c
   ; serviceAvailable = Resource.serviceAvailable c
   ; isAuthorized = Resource.isAuthorized c
   ; forbidden = Resource.forbidden c
   ; allowMissingPost = Resource.allowMissingPost c
   ; malformedRequest = Resource.malformedRequest c
   ; uriTooLong = Resource.uriTooLong c
   ; knownContentType = Resource.knownContentType c
   ; validContentHeaders = Resource.validContentHeaders c
   ; validEntityLength = Resource.validEntityLength c
   ; options = Resource.options c
   ; allowedMethods = Resource.allowedMethods c
   ; knownMethods = Resource.knownMethods c
   ; deleteResource = Resource.deleteResource c
   ; deleteCompleted = Resource.deleteCompleted c
   ; postIsCreate = Resource.postIsCreate c
   ; createPath = Resource.createPath c
   ; processPost = Resource.processPost c
   ; contentTypesProvided = Resource.contentTypesProvided c
   ; languageAvailable = Resource.languageAvailable c
   ; contentTypesAccepted = Resource.contentTypesAccepted c
   ; charsetsProvided = Resource.charsetsProvided c
   ; encodingsProvided = Resource.encodingsProvided c
   ; variances = Resource.variances c
   ; isConflict = Resource.isConflict c
   ; multipleChoices = Resource.multipleChoices c
   ; previouslyExisted = Resource.previouslyExisted c
   ; movedPermanently = Resource.movedPermanently c
   ; movedTemporarily = Resource.movedTemporarily c
   ; lastModified = Resource.lastModified c
   ; expires = Resource.expires c
   ; generateETag = Resource.generateETag c
   ; finishRequest = Resource.finishRequest c
   ; body = f
   }

 default : Resource
 default = record {
     resourceExists = const true
   ; serviceAvailable = const true
   ; isAuthorized = const true
   ; forbidden = const false
   ; allowMissingPost = const false
   ; malformedRequest = const false
   ; uriTooLong = const false
   ; knownContentType = const true
   ; validContentHeaders = const true
   ; validEntityLength = const true
   ; options = const []
   ; allowedMethods = const (HEAD ∷ GET ∷ [])
   ; knownMethods = const (HEAD ∷ GET ∷ PUT ∷ DELETE ∷ POST ∷ TRACE ∷ CONNECT ∷ OPTIONS ∷ [])
   ; deleteResource = const false
   ; deleteCompleted = const true
   ; postIsCreate = const false
   ; createPath = const nothing
   ; processPost = const false
   ; contentTypesProvided = const [ "text/html" ]
   ; languageAvailable = const true
   ; contentTypesAccepted = const []
   ; charsetsProvided = const []
   ; encodingsProvided = const [ "identity" , "defaultEncoder" ]
   ; variances = const []
   ; isConflict = const false
   ; multipleChoices = const false
   ; previouslyExisted = const false
   ; movedPermanently = const nothing
   ; movedTemporarily = const nothing
   ; lastModified = const nothing
   ; expires = const nothing
   ; generateETag = const nothing
   ; finishRequest = const true
   ; body = defaultHtml
   }

configure : Resource → Hooks → Resource
configure base [] = base
configure base ((code , f) ∷ cfs) = update code f (configure base cfs)

toResource : Hooks → Resource
toResource props = configure default props


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Finite sets, based on AVL trees
------------------------------------------------------------------------

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

module Data.AVL.Sets
  {k ℓ} {Key : Set k} {_<_ : Rel Key ℓ}
  (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_)
  where

import Data.AVL as AVL
open import Data.Bool
open import Data.List as List using (List)
open import Data.Maybe as Maybe
open import Data.Product as Prod using (_×_; _,_; proj₁)
open import Data.Unit
open import Function
open import Level

-- The set type. (Note that Set is a reserved word.)

private
  open module S = AVL (const ⊤) isStrictTotalOrder
    public using () renaming (Tree to ⟨Set⟩)

-- Repackaged functions.

empty : ⟨Set⟩
empty = S.empty

singleton : Key → ⟨Set⟩
singleton k = S.singleton k _

insert : Key → ⟨Set⟩ → ⟨Set⟩
insert k = S.insert k _

delete : Key → ⟨Set⟩ → ⟨Set⟩
delete = S.delete

_∈?_ : Key → ⟨Set⟩ → Bool
_∈?_ = S._∈?_

headTail : ⟨Set⟩ → Maybe (Key × ⟨Set⟩)
headTail s = Maybe.map (Prod.map proj₁ id) (S.headTail s)

initLast : ⟨Set⟩ → Maybe (⟨Set⟩ × Key)
initLast s = Maybe.map (Prod.map id proj₁) (S.initLast s)

fromList : List Key → ⟨Set⟩
fromList = S.fromList ∘ List.map (λ k → (k , _))

toList : ⟨Set⟩ → List Key
toList = List.map proj₁ ∘ S.toList


text:
module VecAppend where

open import Prelude

add : Nat -> Nat -> Nat
add zero y = y
add (suc x) y = suc (add x y)

append : forall {A m n} -> Vec A m -> Vec A n -> Vec A (add m n)
append xs ys = {!!}

max_stars_repo_name: carlostome/martin

max_issues_repo_name: carlostome/martin

max_forks_repo_name: carlostome/martin


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

open import lib.Basics
open import lib.types.Coproduct
open import lib.types.Truncation
open import lib.types.Sigma
open import lib.types.Empty
open import lib.types.Bool
open import lib.NConnected
open import lib.NType2

module Util.Misc where

transp-↓' : ∀ {k j} {A : Type k} (P : A → Type j) {a₁ a₂ : A}
  (p : a₁ == a₂) (y : P a₁) → y == transport P p y [ P ↓ p ]
transp-↓' P p y = from-transp P p idp

Σ-transp : ∀ {i j} {A : Type i} (B : A → Type j) {a a' : A} (p : a == a') (b : B a) →
           (a , b) == (a' , transport B p b)

Σ-transp B p b = pair= p (transp-↓' B p b)

equiv-prop : {i j : ULevel} {P : Type i} ⦃ P-prop : is-prop P ⦄ {Q : Type j} ⦃ Q-prop : is-prop Q ⦄ → (P → Q) →
             (Q → P) → (P ≃ Q)

equiv-prop f g = f , (record { g = g ; f-g = λ q → prop-has-all-paths (f (g q)) q
                             ; g-f = λ p → prop-has-all-paths (g (f p)) p
                             ; adj = λ p → prop-has-all-paths _ _ })

_↔_ : {i j : ULevel} (A : Type i) (B : Type j) → Type (lmax i j)
A ↔ B = (A → B) × (B → A)

prop-extensionality : {i : ULevel} {P Q : Type i} ⦃ P-prop : is-prop P ⦄ ⦃ Q-prop : is-prop Q ⦄ → (P ↔ Q) → (P == Q)
prop-extensionality e = ua (equiv-prop (fst e) (snd e))

{- Notation for propositional truncation. -}
∥_∥ : {j : ULevel} → (A : Type j) → Type j
∥_∥ = Trunc (-1)

{- This enables do notation for propositional truncation. It works well for any modality, but we will
   only need this special case. -}
_>>=_ : {i j : ULevel} {X : Type i} {Y : Type j} → (Trunc (-1) X) → (X → Trunc (-1) Y) → (Trunc (-1) Y)
x >>= f = Trunc-rec f x

{- We also add notation for 0 and 1 truncation -}
∥_∥₀ : {j : ULevel} → (A : Type j) → Type j
∥_∥₀ = Trunc 0

∥_∥₁ : {j : ULevel} → (A : Type j) → Type j
∥_∥₁ = Trunc 1

conn-to-path : {i : ULevel} {A : Type i} ⦃ conn : is-connected 0 A ⦄ → (a b : A) → ∥ a == b ∥
conn-to-path ⦃ conn ⦄ _ _ = contr-center (path-conn conn)

conn-to-inh : {i : ULevel} {A : Type i} ⦃ conn : is-connected 0 A ⦄ → ∥ A ∥
conn-to-inh ⦃ conn ⦄ = Trunc-rec ⦃ raise-level _ ⟨⟩ ⦄ [_] (contr-center conn)

inj-to-embed-allpaths : {i j : ULevel} {A : Type i} {B : Type j} ⦃ Bset : is-set B ⦄ (inc : A → B) (inc-inj : is-inj inc) → (b : B) → has-all-paths (hfiber inc b)
inj-to-embed-allpaths inc inc-inj b (a , p) (a' , q) = pair= (inc-inj _ _ (p ∙ ! q)) prop-has-all-paths-↓

inj-to-embed : {i j : ULevel} {A : Type i} {B : Type j} ⦃ Bset : is-set B ⦄ (inc : A → B) (inc-inj : is-inj inc) → (b : B) → is-prop (hfiber inc b)
inj-to-embed inc inc-inj b = all-paths-is-prop (inj-to-embed-allpaths inc inc-inj b)

dec-img-to-⊔ : {i j : ULevel} {A : Type i} {B : Type j} (inc : A → B) (inc-inj : is-inj inc) (dec-img : (b : B) → Dec (hfiber inc b)) → A ⊔ Σ B (λ b → ¬ (hfiber inc b)) ≃ B
dec-img-to-⊔ {A = A} {B = B} inc inc-inj dec-img = equiv f g f-g g-f
  where
    g-aux : (b : B) → (Dec (hfiber inc b)) → A ⊔ Σ B (λ b → ¬ (hfiber inc b))
    g-aux b (inl x) = inl (fst x)
    g-aux b (inr x) = inr (b , x)

    g : (b : B) → A ⊔ Σ B (λ b → ¬ (hfiber inc b))
    g b = g-aux b (dec-img b)

    f : A ⊔ Σ B (λ b → ¬ (hfiber inc b)) → B
    f (inl a) = inc a
    f (inr (b , p)) = b

    g-f-aux : (z : A ⊔ Σ B (λ b → ¬ (hfiber inc b))) (x : Dec (hfiber inc (f z))) → (g-aux (f z) x == z)
    g-f-aux (inl a) (inl x) = ap inl (inc-inj _ _ (snd x))
    g-f-aux (inl a) (inr x) = ⊥-rec (x (a , idp))
    g-f-aux (inr p) (inl x) = ⊥-rec (snd p x)
    g-f-aux (inr p) (inr x) = ap inr (pair= idp (λ= λ w → prop-has-all-paths _ _))

    g-f : (z : A ⊔ Σ B (λ b → ¬ (hfiber inc b))) → (g (f z) == z)
    g-f z = g-f-aux z (dec-img (f z))

    f-g-aux : (b : B) → (x : Dec (hfiber inc b)) → (f (g-aux b x) == b)
    f-g-aux b (inl x) = snd x
    f-g-aux b (inr x) = idp

    f-g : (b : B) → (f (g b) == b)
    f-g b = f-g-aux b (dec-img b)

max_stars_repo_name: awswan/nielsenschreier-hott

max_issues_repo_name: awswan/nielsenschreier-hott

max_forks_repo_name: awswan/nielsenschreier-hott


text:
------------------------------------------------------------------------
-- An alternative but equivalent definition of the partiality monad
-- (but only for sets), based on the lifting construction in Lifting
------------------------------------------------------------------------

-- The code in this module is based on a suggestion from Paolo
-- Capriotti.

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

open import Prelude hiding (T; ⊥)

module Lifting.Partiality-monad {a : Level} where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)

open import Bijection equality-with-J using (_↔_)
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J hiding (⊥↔⊥)
open import H-level equality-with-J

import Lifting
open import Omega-cpo
import Partiality-monad.Inductive as I
import Partiality-monad.Inductive.Eliminators as IE

private
  module L {A : Set a} = Lifting (Set→ω-cpo A)

-- The partiality monad as an ω-cppo.

partiality-monad : Set a → ω-cppo a a
partiality-monad A = L.cppo {A = A}

-- The partiality monad.

infix 10 _⊥
infix  4 _⊑_

_⊥ : Set a → Type a
A ⊥ = ω-cppo.Carrier (partiality-monad A)

_⊑_ : ∀ {A} → A ⊥ → A ⊥ → Type a
_⊑_ {A = A} = ω-cppo._⊑_ (partiality-monad A)

-- This definition of the partiality monad is isomorphic to the
-- definition in Partiality-monad.Inductive.

private

  argsL :
    ∀ {A} →
    L.Rec-args (λ (_ : A ⊥) → ⌞ A ⌟ I.⊥) (λ x y _ → x I.⊑ y)
  argsL = record
    { pe = I.never
    ; po = I.now
    ; pl = λ _ → I.⨆
    ; pa = λ x⊑y y⊑x p-x p-y p-x⊑p-y p-y⊑p-x →
             subst (const _) (L.antisymmetry x⊑y y⊑x) p-x  ≡⟨ subst-const (L.antisymmetry x⊑y y⊑x) ⟩
             p-x                                           ≡⟨ I.antisymmetry p-x⊑p-y p-y⊑p-x ⟩∎
             p-y                                           ∎
    ; pp = I.⊥-is-set
    ; qr = λ _ → I.⊑-refl
    ; qt = λ _ _ _ _ _ → I.⊑-trans
    ; qe = λ _ → I.never⊑
    ; qu = λ _ → I.upper-bound
    ; ql = λ _ _ _ → I.least-upper-bound
    ; qm = λ { refl → I.⊑-refl _ }
    ; q⨆ = λ s →
             I.now (proj₁ s 0)                    I.⊑⟨ I.upper-bound _ 0 ⟩■
             I.⨆ ((λ n → I.now (proj₁ s n)) , _)  ■
    ; qp = λ _ _ _ → I.⊑-propositional
    }

  argsI : ∀ {A} → IE.Arguments-nd a a ⌞ A ⌟
  argsI {A} = record
    { P  = A ⊥
    ; Q  = _⊑_
    ; pe = L.never
    ; po = L.now
    ; pl = λ _ → L.⨆
    ; pa = λ _ _ → L.antisymmetry
    ; ps = L.Carrier-is-set
    ; qr = λ _ → L.⊑-refl
    ; qt = λ _ _ → L.⊑-trans
    ; qe = λ _ → L.never⊑
    ; qu = λ _ → L.upper-bound
    ; ql = λ _ _ _ → L.least-upper-bound
    ; qp = λ _ _ → L.⊑-propositional
    }

⊥↔⊥ : ∀ {A} → A ⊥ ↔ ⌞ A ⌟ I.⊥
⊥↔⊥ = record
  { surjection = record
    { logical-equivalence = record
      { to   = L.⊥-rec argsL
      ; from = IE.⊥-rec-nd argsI
      }
    ; right-inverse-of = IE.⊥-rec-⊥ (record
        { pe = L.⊥-rec argsL (IE.⊥-rec-nd argsI I.never)  ≡⟨ cong (L.⊥-rec argsL) (IE.⊥-rec-nd-never argsI) ⟩
               L.⊥-rec argsL L.never                      ≡⟨ L.⊥-rec-never _ ⟩∎
               I.never                                    ∎
        ; po = λ x →
                 L.⊥-rec argsL (IE.⊥-rec-nd argsI (I.now x))  ≡⟨ cong (L.⊥-rec argsL) (IE.⊥-rec-nd-now argsI _) ⟩
                 L.⊥-rec argsL (L.now x)                      ≡⟨ L.⊥-rec-now _ _ ⟩∎
                 I.now x ∎
        ; pl = λ s ih →
                 L.⊥-rec argsL (IE.⊥-rec-nd argsI (I.⨆ s))      ≡⟨ cong (L.⊥-rec argsL) (IE.⊥-rec-nd-⨆ argsI _) ⟩
                 L.⊥-rec argsL (L.⨆ (IE.inc-rec-nd argsI s))    ≡⟨ L.⊥-rec-⨆ _ _ ⟩
                 I.⨆ (L.inc-rec argsL (IE.inc-rec-nd argsI s))  ≡⟨ cong I.⨆ $ _↔_.to I.equality-characterisation-increasing ih ⟩∎
                 I.⨆ s                                          ∎
        ; pp = λ _ → I.⊥-is-set
        })
    }
  ; left-inverse-of = L.⊥-rec {Q = λ _ _ _ → ⊤} (record
      { pe = IE.⊥-rec-nd argsI (L.⊥-rec argsL L.never)  ≡⟨ cong (IE.⊥-rec-nd argsI) (L.⊥-rec-never _) ⟩
             IE.⊥-rec-nd argsI I.never                  ≡⟨ IE.⊥-rec-nd-never argsI ⟩∎
             L.never                                    ∎
      ; po = λ x →
               IE.⊥-rec-nd argsI (L.⊥-rec argsL (L.now x))  ≡⟨ cong (IE.⊥-rec-nd argsI) (L.⊥-rec-now _ _) ⟩
               IE.⊥-rec-nd argsI (I.now x)                  ≡⟨ IE.⊥-rec-nd-now argsI _ ⟩∎
               L.now x                                      ∎
      ; pl = λ s ih →
                 IE.⊥-rec-nd argsI (L.⊥-rec argsL (L.⨆ s))      ≡⟨ cong (IE.⊥-rec-nd argsI) (L.⊥-rec-⨆ _ _) ⟩
                 IE.⊥-rec-nd argsI (I.⨆ (L.inc-rec argsL s))    ≡⟨ IE.⊥-rec-nd-⨆ argsI _ ⟩
                 L.⨆ (IE.inc-rec-nd argsI (L.inc-rec argsL s))  ≡⟨ cong L.⨆ $ _↔_.to L.equality-characterisation-increasing (proj₁ ih) ⟩∎
                 L.⨆ s                                          ∎
      ; pa = λ _ _ _ _ _ _ → L.Carrier-is-set _ _
      ; pp = mono₁ 1 L.Carrier-is-set
      ; qp = λ _ _ _ _ _ → refl
      })
  }

⊑≃⊑ : ∀ {A} {x y : A ⊥} →
      (x ⊑ y) ≃ (_↔_.to ⊥↔⊥ x I.⊑ _↔_.to ⊥↔⊥ y)
⊑≃⊑ {x = x} {y} =
  _↔_.to (Eq.⇔↔≃ ext L.⊑-propositional I.⊑-propositional)
    (record
       { to   = L.⊑-rec argsL
       ; from =
                _↔_.to ⊥↔⊥ x I.⊑ _↔_.to ⊥↔⊥ y  ↝⟨ IE.⊑-rec-nd argsI ⟩

                _↔_.from ⊥↔⊥ (_↔_.to ⊥↔⊥ x) ⊑
                _↔_.from ⊥↔⊥ (_↔_.to ⊥↔⊥ y)    ↝⟨ ≡⇒↝ _ (cong₂ _⊑_ (_↔_.left-inverse-of ⊥↔⊥ _)
                                                                   (_↔_.left-inverse-of ⊥↔⊥ _)) ⟩□
                x ⊑ y                          □
       })

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module container.w where

open import container.w.core public
open import container.w.algebra public
open import container.w.fibration public

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
module Preduploid where

open import Relation.Unary using (Pred)
open import Relation.Binary using (REL)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)

open import Level

data Polarity : Set where
  + : Polarity
  ⊝ : Polarity

private
  variable p q r s : Polarity

record Preduploid o ℓ : Set (suc (o ⊔ ℓ)) where
  infix 4 _⇒_
  infix 9 _∙_ _∘_ _⊙_

  field
    Ob : Polarity -> Set o
    _⇒_ : REL (Ob p) (Ob q) ℓ

    id : forall {A : Ob p} -> A ⇒ A
    _∙_ : forall {A : Ob p} {B : Ob +} {C : Ob q} -> B ⇒ C -> A ⇒ B -> A ⇒ C
    _∘_ : forall {A : Ob p} {B : Ob ⊝} {C : Ob q} -> B ⇒ C -> A ⇒ B -> A ⇒ C

    identity∙ˡ : forall {A : Ob p} {B : Ob +} {f : A ⇒ B} -> id ∙ f ≡ f
    identity∙ʳ : forall {A : Ob +} {B : Ob p} {f : A ⇒ B} -> f ∙ id ≡ f

    identity∘ˡ : forall {A : Ob p} {B : Ob ⊝} {f : A ⇒ B} -> id ∘ f ≡ f
    identity∘ʳ : forall {A : Ob ⊝} {B : Ob p} {f : A ⇒ B} -> f ∘ id ≡ f

    assoc∙∙ : forall {A : Ob p} {B : Ob +} {C : Ob +} {D : Ob q}
      {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} -> (h ∙ g) ∙ f ≡ h ∙ (g ∙ f)
    assoc∘∘ : forall {A : Ob p} {B : Ob ⊝} {C : Ob ⊝} {D : Ob q}
      {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} -> (h ∘ g) ∘ f ≡ h ∘ (g ∘ f)
    assoc∙∘ : forall {A : Ob p} {B : Ob ⊝} {C : Ob +} {D : Ob q}
      {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} -> (h ∙ g) ∘ f ≡ h ∙ (g ∘ f)

  π : Ob p -> Polarity
  π {p = p} _ = p

  _⊙_ : forall {A : Ob p} {B : Ob q} {C : Ob r} -> B ⇒ C -> A ⇒ B -> A ⇒ C
  _⊙_ {q = +} = _∙_
  _⊙_ {q = ⊝} = _∘_

  identityˡ : forall {A : Ob p} {B : Ob q} {f : A ⇒ B} -> id ⊙ f ≡ f
  identityˡ {q = +} = identity∙ˡ
  identityˡ {q = ⊝} = identity∘ˡ

  identityʳ : forall {A : Ob p} {B : Ob q} {f : A ⇒ B} -> f ⊙ id ≡ f
  identityʳ {p = +} = identity∙ʳ
  identityʳ {p = ⊝} = identity∘ʳ

  Linear : forall {C : Ob r} {D : Ob s} -> Pred (C ⇒ D) (o ⊔ ℓ)
  Linear {C = C} {D = D} f = forall {p q} {A : Ob p} {B : Ob q} {g : B ⇒ C} {h : A ⇒ B} -> f ⊙ (g ⊙ h) ≡ (f ⊙ g) ⊙ h

  Thunkable : forall {A : Ob p} {B : Ob q} -> Pred (A ⇒ B) (o ⊔ ℓ)
  Thunkable {A = A} {B = B} f = forall {r s} {C : Ob r} {D : Ob s} {g : B ⇒ C} {h : C ⇒ D} -> h ⊙ (g ⊙ f) ≡ (h ⊙ g) ⊙ f

  P-Linear : forall {P : Ob +} {A : Ob p} -> (f : P ⇒ A) -> Linear f
  P-Linear f {q = +} = sym assoc∙∙
  P-Linear f {q = ⊝} = sym assoc∙∘

  N-Thunkable : forall {A : Ob p} {N : Ob ⊝} -> (f : A ⇒ N) -> Thunkable f
  N-Thunkable f {r = +} = sym assoc∙∘
  N-Thunkable f {r = ⊝} = sym assoc∘∘

max_stars_repo_name: elpinal/duploids

max_issues_repo_name: elpinal/duploids

max_forks_repo_name: elpinal/duploids